rw [h2]
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a * a⁻¹ * a⁻¹⁻¹ = 1 * a⁻¹⁻¹
no goals