no goals
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Semiring R
inst✝ : Semiring S
rc : RingHomClass F R S
I : Ideal R
f : F
⊢ map f I = ⊥ ↔ I ≤ RingHom.ker f
rw [RingHom.ker, eq_bot_iff, map_le_iff_le_comap]