no goals
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
I : Ideal R
f : F
hf : Function.Injective ↑f
⊢ map f I = ⊥ ↔ I = ⊥
rw [map_eq_bot_iff_le_ker, (RingHom.injective_iff_ker_eq_bot f).mp hf, le_bot_iff]