case h
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
⊢ ∀ (x : R ⧸ I), x ∈ RingHom.ker (Quotient.lift I f H) ↔ x ∈ map (Quotient.mk I) (RingHom.ker f)
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
⊢ RingHom.ker (Quotient.lift I f H) = map (Quotient.mk I) (RingHom.ker f)
apply Ideal.ext
case h
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
⊢ x ∈ RingHom.ker (Quotient.lift I f H) ↔ x ∈ map (Quotient.mk I) (RingHom.ker f)
case h
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
⊢ ∀ (x : R ⧸ I), x ∈ RingHom.ker (Quotient.lift I f H) ↔ x ∈ map (Quotient.mk I) (RingHom.ker f)
intro x
case h.mp
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
⊢ x ∈ RingHom.ker (Quotient.lift I f H) → x ∈ map (Quotient.mk I) (RingHom.ker f)

case h.mpr
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
⊢ x ∈ map (Quotient.mk I) (RingHom.ker f) → x ∈ RingHom.ker (Quotient.lift I f H)
case h
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
⊢ x ∈ RingHom.ker (Quotient.lift I f H) ↔ x ∈ map (Quotient.mk I) (RingHom.ker f)
constructor
case h.mp
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
hx : x ∈ RingHom.ker (Quotient.lift I f H)
⊢ x ∈ map (Quotient.mk I) (RingHom.ker f)
case h.mp
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
⊢ x ∈ RingHom.ker (Quotient.lift I f H) → x ∈ map (Quotient.mk I) (RingHom.ker f)
intro hx
case h.mp.intro
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
hx : x ∈ RingHom.ker (Quotient.lift I f H)
y : R
hy : ↑(Quotient.mk I) y = x
⊢ x ∈ map (Quotient.mk I) (RingHom.ker f)
case h.mp
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
hx : x ∈ RingHom.ker (Quotient.lift I f H)
⊢ x ∈ map (Quotient.mk I) (RingHom.ker f)
obtain ⟨y, hy⟩ := Quotient.mk_surjective x
case h.mp.intro
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
y : R
hx : y ∈ RingHom.ker f
hy : ↑(Quotient.mk I) y = x
⊢ x ∈ map (Quotient.mk I) (RingHom.ker f)
case h.mp.intro
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
hx : x ∈ RingHom.ker (Quotient.lift I f H)
y : R
hy : ↑(Quotient.mk I) y = x
⊢ x ∈ map (Quotient.mk I) (RingHom.ker f)
rw [RingHom.mem_ker, ← hy, Ideal.Quotient.lift_mk, ← RingHom.mem_ker] at hx
case h.mp.intro
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
y : R
hx : y ∈ RingHom.ker f
hy : ↑(Quotient.mk I) y = x
⊢ ∃ x, x ∈ RingHom.ker f ∧ ↑(Quotient.mk I) x = ↑(Quotient.mk I) y
case h.mp.intro
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
y : R
hx : y ∈ RingHom.ker f
hy : ↑(Quotient.mk I) y = x
⊢ x ∈ map (Quotient.mk I) (RingHom.ker f)
rw [← hy, mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective]
no goals
case h.mp.intro
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
y : R
hx : y ∈ RingHom.ker f
hy : ↑(Quotient.mk I) y = x
⊢ ∃ x, x ∈ RingHom.ker f ∧ ↑(Quotient.mk I) x = ↑(Quotient.mk I) y
exact ⟨y, hx, rfl⟩
case h.mpr
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
hx : x ∈ map (Quotient.mk I) (RingHom.ker f)
⊢ x ∈ RingHom.ker (Quotient.lift I f H)
case h.mpr
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
⊢ x ∈ map (Quotient.mk I) (RingHom.ker f) → x ∈ RingHom.ker (Quotient.lift I f H)
intro hx
case h.mpr
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
hx : ∃ x_1, x_1 ∈ RingHom.ker f ∧ ↑(Quotient.mk I) x_1 = x
⊢ x ∈ RingHom.ker (Quotient.lift I f H)
case h.mpr
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
hx : x ∈ map (Quotient.mk I) (RingHom.ker f)
⊢ x ∈ RingHom.ker (Quotient.lift I f H)
rw [mem_map_iff_of_surjective (Quotient.mk I)  Quotient.mk_surjective] at hx
case h.mpr.intro
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
y : R
hy : y ∈ RingHom.ker f ∧ ↑(Quotient.mk I) y = x
⊢ x ∈ RingHom.ker (Quotient.lift I f H)
case h.mpr
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
hx : ∃ x_1, x_1 ∈ RingHom.ker f ∧ ↑(Quotient.mk I) x_1 = x
⊢ x ∈ RingHom.ker (Quotient.lift I f H)
obtain ⟨y, hy⟩ := hx
case h.mpr.intro
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
y : R
hy : y ∈ RingHom.ker f ∧ ↑(Quotient.mk I) y = x
⊢ ↑f y = 0
case h.mpr.intro
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
y : R
hy : y ∈ RingHom.ker f ∧ ↑(Quotient.mk I) y = x
⊢ x ∈ RingHom.ker (Quotient.lift I f H)
rw [RingHom.mem_ker, ← hy.right, Ideal.Quotient.lift_mk]
no goals
case h.mpr.intro
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
y : R
hy : y ∈ RingHom.ker f ∧ ↑(Quotient.mk I) y = x
⊢ ↑f y = 0
exact hy.left