refactor(group_theory/commutator): Generalize map_commutator_element (

#12555)

This PR generalizes `map_commutator_element` from `monoid_hom_class F G G` to `monoid_hom_class F G G'`.

src/group_theory/commutator.lean

@@ -21,12 +21,12 @@ is the subgroup of `G` generated by the commutators `h₁ * h₂ * h₁⁻¹ * h
 * `⁅H₁, H₂⁆` : the commutator of the subgroups `H₁` and `H₂`.
 -/
 
-variables {G G' F : Type*} [group G] [group G'] [monoid_hom_class F G G] (f : F) (g₁ g₂ g₃ : G)
+variables {G G' F : Type*} [group G] [group G'] [monoid_hom_class F G G'] (f : F) (g₁ g₂ g₃ : G)
 
 @[simp] lemma commutator_element_inv : ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆ :=
 by simp_rw [commutator_element_def, mul_inv_rev, inv_inv, mul_assoc]
 
-lemma map_commutator_element : f ⁅g₁, g₂⁆ = ⁅f g₁, f g₂⁆ :=
+lemma map_commutator_element : (f ⁅g₁, g₂⁆ : G') = ⁅f g₁, f g₂⁆ :=
 by simp_rw [commutator_element_def, map_mul f, map_inv f]
 
 lemma conjugate_commutator_element : g₃ * ⁅g₁, g₂⁆ * g₃⁻¹ = ⁅g₃ * g₁ * g₃⁻¹, g₃ * g₂ * g₃⁻¹⁆ :=