no goals
R : Type u_2
S : Type u_3
F : Type ?u.1964564
inst✝³ : Ring R
inst✝² : Ring S
rc : RingHomClass F R S
F' : Type u_1
inst✝¹ : RingEquivClass F' R S
f : F'
I : Ideal R
inst✝ : IsPrime I
⊢ RingHom.ker f ≤ I
simp only [RingHom.ker_equiv, bot_le]