Theorem: Ideal.ker_mk (GlimpseOfLean/Library/Basic.lean)

State before:
R : Type u_1
S : Type ?u.14649
inst✝¹ : CommRing R
ι : Type ?u.14646
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ ker (Quotient.mk I) = I
Tactic:
ext x
State after:
case h
R : Type u_1
S : Type ?u.14649
inst✝¹ : CommRing R
ι : Type ?u.14646
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
x : R
⊢ x ∈ ker (Quotient.mk I) ↔ x ∈ I

State before:
case h
R : Type u_1
S : Type ?u.14649
inst✝¹ : CommRing R
ι : Type ?u.14646
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
x : R
⊢ x ∈ ker (Quotient.mk I) ↔ x ∈ I
Tactic:
rw [mem_ker, Quotient.eq_zero_iff_mem]
State after:
no goals