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