∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  [inst_3 : NeZero (p.ramificationIdx P)] (x : R),
  (algebraMap (R ⧸ p) (S ⧸ P)) ((Ideal.Quotient.mk p) x) = (Ideal.Quotient.mk P) ((algebraMap R S) x)