Theorem: Tutorial.GroupHom.rangeKerLift_injective (Solution/Advanced/Algebra/Lecture5.lean)

State before:
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
⊢ Function.Injective ⇑(rangeKerLift f)
Tactic:
rw [injective_iff_map_eq_one]
State after:
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
⊢ ∀ (a : G ⧸ ker f), (rangeKerLift f) a = 1 → a = 1

State before:
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
⊢ ∀ (a : G ⧸ ker f), (rangeKerLift f) a = 1 → a = 1
Tactic:
rintro ⟨_⟩
State after:
case mk
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
a✝¹ : G ⧸ ker f
a✝ : G
⊢ (rangeKerLift f) (Quot.mk Setoid.r a✝) = 1 → Quot.mk Setoid.r a✝ = 1

State before:
case mk
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
a✝¹ : G ⧸ ker f
a✝ : G
⊢ (rangeKerLift f) (Quot.mk Setoid.r a✝) = 1 → Quot.mk Setoid.r a✝ = 1
Tactic:
simp_all
State after:
no goals