Theorem: Tutorial.GroupHom.ker_eq_bot (Solution/Advanced/Algebra/Lecture2.lean)

State before:
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ ker f = ⊥ ↔ Function.Injective ⇑f
Tactic:
rw [injective_iff_map_eq_one]
State after:
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ ker f = ⊥ ↔ ∀ (a : G₁), f a = 1 → a = 1

State before:
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ ker f = ⊥ ↔ ∀ (a : G₁), f a = 1 → a = 1
Tactic:
constructor
State after:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ ker f = ⊥ → ∀ (a : G₁), f a = 1 → a = 1

case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ (∀ (a : G₁), f a = 1 → a = 1) → ker f = ⊥

State before:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ ker f = ⊥ → ∀ (a : G₁), f a = 1 → a = 1
Tactic:
intro h a (hf : a ∈ f.ker)
State after:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ker f = ⊥
a : G₁
hf : a ∈ ker f
⊢ a = 1

State before:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ker f = ⊥
a : G₁
hf : a ∈ ker f
⊢ a = 1
Tactic:
simpa [h] using hf
State after:
no goals

State before:
case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ (∀ (a : G₁), f a = 1 → a = 1) → ker f = ⊥
Tactic:
intro h
State after:
case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
⊢ ker f = ⊥

State before:
case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
⊢ ker f = ⊥
Tactic:
ext a
State after:
case mpr.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
⊢ a ∈ ker f ↔ a ∈ ⊥

State before:
case mpr.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
⊢ a ∈ ker f ↔ a ∈ ⊥
Tactic:
simp only [mem_ker, mem_bot]
State after:
case mpr.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
⊢ f a = 1 ↔ a = 1

State before:
case mpr.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
⊢ f a = 1 ↔ a = 1
Tactic:
constructor
State after:
case mpr.a.mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
⊢ f a = 1 → a = 1

case mpr.a.mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
⊢ a = 1 → f a = 1

State before:
case mpr.a.mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
⊢ f a = 1 → a = 1
Tactic:
intro ha
State after:
case mpr.a.mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
ha : f a = 1
⊢ a = 1

State before:
case mpr.a.mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
ha : f a = 1
⊢ a = 1
Tactic:
apply h
State after:
case mpr.a.mp.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
ha : f a = 1
⊢ f a = 1

State before:
case mpr.a.mp.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
ha : f a = 1
⊢ f a = 1
Tactic:
apply ha
State after:
no goals

State before:
case mpr.a.mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
⊢ a = 1 → f a = 1
Tactic:
intro ha
State after:
case mpr.a.mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
ha : a = 1
⊢ f a = 1

State before:
case mpr.a.mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
h : ∀ (a : G₁), f a = 1 → a = 1
a : G₁
ha : a = 1
⊢ f a = 1
Tactic:
rw [ha, map_one]
State after:
no goals