Theorem: MyGroup.mul_right_inv (LeanInRome/S2_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean)

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

State before:
G : Type u_1
inst✝ : Group G
a : G
h : (a * a⁻¹)⁻¹ * (a * a⁻¹ * (a * a⁻¹)) = 1
⊢ a * a⁻¹ = 1
Tactic:
rw [← h, ← mul_assoc, mul_left_inv, one_mul]
State after:
no goals

State before:
G : Type u_1
inst✝ : Group G
a : G
⊢ (a * a⁻¹)⁻¹ * (a * a⁻¹ * (a * a⁻¹)) = 1
Tactic:
rw [mul_assoc, ← mul_assoc a⁻¹ a, mul_left_inv, one_mul, mul_left_inv]
State after:
no goals