Theorem: inverse_of_a_commutator (LeanCourse/Lectures/Lecture2.lean)

State before:
G : Type u_1
inst✝ : Group G
g h : G
⊢ ⁅g, h⁆⁻¹ = ⁅h, g⁆
Tactic:
rw [commutatorElement_def, commutatorElement_def]
State after:
G : Type u_1
inst✝ : Group G
g h : G
⊢ (g * h * g⁻¹ * h⁻¹)⁻¹ = h * g * h⁻¹ * g⁻¹

State before:
G : Type u_1
inst✝ : Group G
g h : G
⊢ (g * h * g⁻¹ * h⁻¹)⁻¹ = h * g * h⁻¹ * g⁻¹
Tactic:
rw [mul_inv_rev (g * h * g⁻¹) h⁻¹]
State after:
G : Type u_1
inst✝ : Group G
g h : G
⊢ h⁻¹⁻¹ * (g * h * g⁻¹)⁻¹ = h * g * h⁻¹ * g⁻¹

State before:
G : Type u_1
inst✝ : Group G
g h : G
⊢ h⁻¹⁻¹ * (g * h * g⁻¹)⁻¹ = h * g * h⁻¹ * g⁻¹
Tactic:
rw [mul_inv_rev]
State after:
G : Type u_1
inst✝ : Group G
g h : G
⊢ h⁻¹⁻¹ * (g⁻¹⁻¹ * (g * h)⁻¹) = h * g * h⁻¹ * g⁻¹

State before:
G : Type u_1
inst✝ : Group G
g h : G
⊢ h⁻¹⁻¹ * (g⁻¹⁻¹ * (g * h)⁻¹) = h * g * h⁻¹ * g⁻¹
Tactic:
rw [mul_inv_rev]
State after:
G : Type u_1
inst✝ : Group G
g h : G
⊢ h⁻¹⁻¹ * (g⁻¹⁻¹ * (h⁻¹ * g⁻¹)) = h * g * h⁻¹ * g⁻¹

State before:
G : Type u_1
inst✝ : Group G
g h : G
⊢ h⁻¹⁻¹ * (g⁻¹⁻¹ * (h⁻¹ * g⁻¹)) = h * g * h⁻¹ * g⁻¹
Tactic:
rw [inv_inv, inv_inv]
State after:
G : Type u_1
inst✝ : Group G
g h : G
⊢ h * (g * (h⁻¹ * g⁻¹)) = h * g * h⁻¹ * g⁻¹

State before:
G : Type u_1
inst✝ : Group G
g h : G
⊢ h * (g * (h⁻¹ * g⁻¹)) = h * g * h⁻¹ * g⁻¹
Tactic:
rw [mul_assoc]
State after:
G : Type u_1
inst✝ : Group G
g h : G
⊢ h * (g * (h⁻¹ * g⁻¹)) = h * g * (h⁻¹ * g⁻¹)

State before:
G : Type u_1
inst✝ : Group G
g h : G
⊢ h * (g * (h⁻¹ * g⁻¹)) = h * g * (h⁻¹ * g⁻¹)
Tactic:
rw [mul_assoc]
State after:
no goals