∀ {R : Type u} {S : Type v} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S} {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} {inst_3 : CommRing R'} {inst_4 : CommRing S'} {inst_5 : Algebra R' S'}
  {P' : Algebra.Extension R' S'} {inst_6 : Algebra R R'} {inst_7 : Algebra S S'} {toRingHom : P.Ring →+* P'.Ring}
  {toRingHom_algebraMap :
    ∀ (x : R), toRingHom ((algebraMap R P.Ring) x) = (algebraMap R' P'.Ring) ((algebraMap R R') x)}
  {algebraMap_toRingHom :
    ∀ (x : P.Ring), (algebraMap P'.Ring S') (toRingHom x) = (algebraMap S S') ((algebraMap P.Ring S) x)}
  {toRingHom_1 : P.Ring →+* P'.Ring}
  {toRingHom_algebraMap_1 :
    ∀ (x : R), toRingHom_1 ((algebraMap R P.Ring) x) = (algebraMap R' P'.Ring) ((algebraMap R R') x)}
  {algebraMap_toRingHom_1 :
    ∀ (x : P.Ring), (algebraMap P'.Ring S') (toRingHom_1 x) = (algebraMap S S') ((algebraMap P.Ring S) x)},
  { toRingHom := toRingHom, toRingHom_algebraMap := toRingHom_algebraMap,
        algebraMap_toRingHom := algebraMap_toRingHom } =
      { toRingHom := toRingHom_1, toRingHom_algebraMap := toRingHom_algebraMap_1,
        algebraMap_toRingHom := algebraMap_toRingHom_1 } →
    toRingHom = toRingHom_1