case h
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
x✝ : R
⊢ x✝ ∈ RingHom.ker (Quotient.mk I) ↔ x✝ ∈ I
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
⊢ RingHom.ker (Quotient.mk I) = I
ext
no goals
case h
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
x✝ : R
⊢ x✝ ∈ RingHom.ker (Quotient.mk I) ↔ x✝ ∈ I
rw [RingHom.ker, mem_comap, @Submodule.mem_bot _ _ _ _ Semiring.toModule _,
  Quotient.eq_zero_iff_mem]