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]
G : Type u_1
inst✝ : Group G
g : G
⊢ g⁻¹⁻¹ = g
no goals