Theorem: Tutorial.GroupHom.ker_eq_bot (Tutorial/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:
sorry
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:
sorry
State after:
no goals