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

State before:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ Injective ⇑(Quotient.lift I f H) ↔ ker f = I
Tactic:
have : I ≤ ker f := H
State after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : I ≤ ker f
⊢ Injective ⇑(Quotient.lift I f H) ↔ ker f = I

State before:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : I ≤ ker f
⊢ Injective ⇑(Quotient.lift I f H) ↔ ker f = I
Tactic:
rw [injective_iff_ker_eq_bot, ker_lift, map_eq_bot_iff_le_ker, ker_mk]
State after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : I ≤ ker f
⊢ ker f ≤ I ↔ ker f = I

State before:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : I ≤ ker f
⊢ ker f ≤ I ↔ ker f = I
Tactic:
constructor
State after:
case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : I ≤ ker f
⊢ ker f ≤ I → ker f = I

case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : I ≤ ker f
⊢ ker f = I → ker f ≤ I

State before:
case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : I ≤ ker f
⊢ ker f ≤ I → ker f = I
Tactic:
exact fun h ↦ le_antisymm h this
State after:
no goals

State before:
case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : I ≤ ker f
⊢ ker f = I → ker f ≤ I
Tactic:
rintro rfl
State after:
case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
f : R →+* S
H : ∀ a ∈ ker f, f a = 0
this : ker f ≤ ker f
⊢ ker f ≤ ker f

State before:
case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
f : R →+* S
H : ∀ a ∈ ker f, f a = 0
this : ker f ≤ ker f
⊢ ker f ≤ ker f
Tactic:
rfl
State after:
no goals