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

State before:
G₁ G₂ : Type
inst✝¹ : Group G₁
inst✝ : Group G₂
f : G₁ →* G₂
a : G₁
⊢ f a⁻¹ = (f a)⁻¹
Tactic:
apply eq_inv_of_mul_eq_one_left
State after:
case a
G₁ G₂ : Type
inst✝¹ : Group G₁
inst✝ : Group G₂
f : G₁ →* G₂
a : G₁
⊢ f a⁻¹ * f a = 1

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