no goals
R : Type u_1
S : Type u_2
F : Type ?u.1967635
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
⊢ map f I = map f J ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f
rw [← (comap_injective_of_surjective f hf).eq_iff, comap_map_of_surjective f hf,
  comap_map_of_surjective f hf, RingHom.ker_eq_comap_bot]