rw [← one_mul (b⁻¹ * a⁻¹), ← mul_left_inv (a * b), mul_assoc, mul_assoc, ← mul_assoc b b⁻¹,
  mul_right_inv, one_mul, mul_right_inv, mul_one]
G : Type u_1
inst✝ : Group G
a b : G
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
no goals