Theorem: MyGroup.mul_inv_revαα (MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean)

State before:
G : Type u_1
inst✝ : Group G
a b : G
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
Tactic:
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]
State after:
no goals