∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (I : Ideal R) [inst_2 : I.IsPrime]
  (J : Ideal S) [inst_3 : J.IsPrime] (f : R →+* S) (hf : I = Ideal.comap f J),
  IsLocalHom (Localization.localRingHom I J f hf)