∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_3} [inst_1 : CommSemiring P] (I : Ideal R) [hI : I.IsPrime]
  (J : Ideal P) [inst_2 : J.IsPrime] (f f_1 : R →+* P) (e_f : f = f_1) (hIJ : I = Ideal.comap f J),
  Localization.localRingHom I J f hIJ = Localization.localRingHom I J f_1 ⋯