Theorem: inverse_involution' (PowerCalc/Examples/Groups.lean)

State before:
G : Type u_1
inst✝ : Group G
g : G
⊢ g⁻¹⁻¹ = g
Tactic:
rw [←  mul_one g⁻¹⁻¹, ←  inv_mul_self g,
    ← mul_assoc, inv_mul_self g⁻¹,  one_mul]
State after:
no goals