no goals
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I✝ : Ideal R
hf : Function.Surjective ↑f
I : Ideal R
r : R
h : ↑f r ∈ map f I
s : R
hsi : s ∈ ↑I
hfsr : ↑f s = ↑f r
⊢ ↑f (r - s) = 0
rw [map_sub, hfsr, sub_self]