no goals
R : Type u
S : Type v
F : Type ?u.1386892
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f✝ : F
I✝ I : Ideal R
f : R ≃+* S
⊢ map (↑(RingEquiv.symm f)) (map (↑f) I) = I
simp [← RingEquiv.toRingHom_eq_coe, map_map]