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

State before:
G₁ G₂ : Type
inst✝¹ : Group G₁
inst✝ : Group G₂
f : G₁ →* G₂
⊢ f 1 = 1
Tactic:
have h : f 1 * f 1 = f 1 * 1 := by
  rw [← map_mul, mul_one, mul_one]
State after:
G₁ G₂ : Type
inst✝¹ : Group G₁
inst✝ : Group G₂
f : G₁ →* G₂
h : f 1 * f 1 = f 1 * 1
⊢ f 1 = 1

State before:
G₁ G₂ : Type
inst✝¹ : Group G₁
inst✝ : Group G₂
f : G₁ →* G₂
h : f 1 * f 1 = f 1 * 1
⊢ f 1 = 1
Tactic:
exact mul_left_cancel _ h
State after:
no goals

State before:
G₁ G₂ : Type
inst✝¹ : Group G₁
inst✝ : Group G₂
f : G₁ →* G₂
⊢ f 1 * f 1 = f 1 * 1
Tactic:
rw [← map_mul, mul_one, mul_one]
State after:
no goals