no goals
G : Type u_1
G' : Type ?u.665
F : Type ?u.668
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
⊢ ⁅g₁, g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁
rw [commutatorElement_def, mul_inv_eq_one, mul_inv_eq_iff_eq_mul]