no goals
G : Type u_1
G' : Type ?u.10728
F : Type ?u.10731
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
⊢ ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆
simp_rw [commutatorElement_def, mul_inv_rev, inv_inv, mul_assoc]