Theorem: RingHom.ker_eq_ideal_iff (DividedPowers/DPAlgebra/RobyLemma9.lean)

State before:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
⊢ ker f = I ↔ ∃ (h : I ≤ ker f), Function.Injective ⇑(Ideal.Quotient.lift I f h)
Tactic:
constructor
State after:
case mp
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
⊢ ker f = I → ∃ (h : I ≤ ker f), Function.Injective ⇑(Ideal.Quotient.lift I f h)

case mpr
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
⊢ (∃ (h : I ≤ ker f), Function.Injective ⇑(Ideal.Quotient.lift I f h)) → ker f = I

State before:
case mp
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
⊢ ker f = I → ∃ (h : I ≤ ker f), Function.Injective ⇑(Ideal.Quotient.lift I f h)
Tactic:
intro hI
State after:
case mp
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
hI : ker f = I
⊢ ∃ (h : I ≤ ker f), Function.Injective ⇑(Ideal.Quotient.lift I f h)

State before:
case mp
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
hI : ker f = I
⊢ ∃ (h : I ≤ ker f), Function.Injective ⇑(Ideal.Quotient.lift I f h)
Tactic:
use le_of_eq hI.symm
State after:
case h
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
hI : ker f = I
⊢ Function.Injective ⇑(Ideal.Quotient.lift I f ⋯)

State before:
case h
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
hI : ker f = I
⊢ Function.Injective ⇑(Ideal.Quotient.lift I f ⋯)
Tactic:
apply RingHom.lift_injective_of_ker_le_ideal
State after:
case h.hI
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
hI : ker f = I
⊢ ker f ≤ I

State before:
case h.hI
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
hI : ker f = I
⊢ ker f ≤ I
Tactic:
simp only [hI, le_refl]
State after:
no goals

State before:
case mpr
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
⊢ (∃ (h : I ≤ ker f), Function.Injective ⇑(Ideal.Quotient.lift I f h)) → ker f = I
Tactic:
rintro ⟨hI, h⟩
State after:
case mpr.intro
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
hI : I ≤ ker f
h : Function.Injective ⇑(Ideal.Quotient.lift I f hI)
⊢ ker f = I

State before:
case mpr.intro
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
hI : I ≤ ker f
h : Function.Injective ⇑(Ideal.Quotient.lift I f hI)
⊢ ker f = I
Tactic:
simp only [RingHom.injective_iff_ker_eq_bot, Ideal.ker_quotient_lift f hI,
  Ideal.map_eq_bot_iff_le_ker, Ideal.mk_ker] at h
State after:
case mpr.intro
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
hI : I ≤ ker f
h : ker f ≤ I
⊢ ker f = I

State before:
case mpr.intro
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
hI : I ≤ ker f
h : ker f ≤ I
⊢ ker f = I
Tactic:
exact le_antisymm h hI
State after:
no goals