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

State before:
G : Type u_1
inst✝ : Group G
g : G
⊢ g⁻¹⁻¹ = g
Tactic:
calc
  g⁻¹⁻¹ = g⁻¹⁻¹ * 1 := by rw [mul_one]
      _ = g⁻¹⁻¹ * (g⁻¹ * g) := by rw [inv_mul_self]
      _ = (g⁻¹⁻¹ * g⁻¹) * g := by rw [mul_assoc]
      _ = 1 * g := by rw [inv_mul_self]
      _ = g := by rw [one_mul]
State after:
no goals

State before:
G : Type u_1
inst✝ : Group G
g : G
⊢ g⁻¹⁻¹ = g⁻¹⁻¹ * 1
Tactic:
rw [mul_one]
State after:
no goals

State before:
G : Type u_1
inst✝ : Group G
g : G
⊢ g⁻¹⁻¹ * 1 = g⁻¹⁻¹ * (g⁻¹ * g)
Tactic:
rw [inv_mul_self]
State after:
no goals

State before:
G : Type u_1
inst✝ : Group G
g : G
⊢ g⁻¹⁻¹ * (g⁻¹ * g) = g⁻¹⁻¹ * g⁻¹ * g
Tactic:
rw [mul_assoc]
State after:
no goals

State before:
G : Type u_1
inst✝ : Group G
g : G
⊢ g⁻¹⁻¹ * g⁻¹ * g = 1 * g
Tactic:
rw [inv_mul_self]
State after:
no goals

State before:
G : Type u_1
inst✝ : Group G
g : G
⊢ 1 * g = g
Tactic:
rw [one_mul]
State after:
no goals