have h : (a * a⁻¹)⁻¹ * (a * a⁻¹ * (a * a⁻¹)) = 1 := by
  rw [mul_assoc, ← mul_assoc a⁻¹ a, mul_left_inv, one_mul, mul_left_inv]
G : Type u_1
inst✝ : Group G
a : G
⊢ a * a⁻¹ = 1
G : Type u_1
inst✝ : Group G
a : G
h : (a * a⁻¹)⁻¹ * (a * a⁻¹ * (a * a⁻¹)) = 1
⊢ a * a⁻¹ = 1