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

State before:
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ Function.Injective ⇑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₂
⊢ Function.Injective ⇑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) → Function.Injective ⇑f

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

State before:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hf : Function.Injective ⇑f
a : G₁
ha : f a = 1
⊢ a = 1
Tactic:
apply hf
State after:
case mp.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hf : Function.Injective ⇑f
a : G₁
ha : f a = 1
⊢ f a = f 1

State before:
case mp.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hf : Function.Injective ⇑f
a : G₁
ha : f a = 1
⊢ f a = f 1
Tactic:
rw [ha, map_one]
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) → Function.Injective ⇑f
Tactic:
intro h a b hab
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
a b : G₁
hab : f a = f b
⊢ a = b

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
a b : G₁
hab : f a = f b
⊢ a = b
Tactic:
rw [← mul_inv_eq_one] at *
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
a b : G₁
hab : f a * (f b)⁻¹ = 1
⊢ a * b⁻¹ = 1

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
a b : G₁
hab : f a * (f b)⁻¹ = 1
⊢ a * b⁻¹ = 1
Tactic:
apply h
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 b : G₁
hab : f a * (f b)⁻¹ = 1
⊢ f (a * b⁻¹) = 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 b : G₁
hab : f a * (f b)⁻¹ = 1
⊢ f (a * b⁻¹) = 1
Tactic:
rw [map_mul, map_inv, hab]
State after:
no goals