no goals
G : Type u_2
G' : Type u_1
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
⊢ ↑f ⁅g₁, g₂⁆ = ⁅↑f g₁, ↑f g₂⁆
simp_rw [commutatorElement_def, map_mul f, map_inv f]