∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {p : Ideal R} [inst_2 : Algebra R S] (x : R),
  (algebraMap (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) ((Ideal.Quotient.mk p) x) =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) ((algebraMap R S) x)