How can I use the definition to prove this quetion?

Stream: maths

[Move fast]

I meet a question

Let $G$ be any group. Prove that the map from $G$ to itself defined
by $g \mapsto g^{2}$ is a homomorphism if and only if $G$ is abelian.

And I solved it like the following:

import Mathlib
open Subgroup
variable (G : Type*) [Group G]
/-- f: G → G，x→ x\^2   -/
def f : G → G := fun (x : G) ↦ x^2
/-- f is a homomorphism ↔ G is abelian -/
theorem f_homo_iff_G_abelian: (∀ a b : G, f G a * f G b = f G (a * b))
↔ (∀ a b : G, a * b = b * a) := by
  constructor
  /-If f is a homomorphism，then G is abelian。 -/
  · -- Suppose ∀ a b : G，f(a) * f(b) = f(a * b)
    intro eq a b
    /- f(a * b) = f(a) * f(b)。 -/
    have key: f G (a * b) = f G a * f G b := by simp [eq]
    simp [f] at key
    rw [pow_two, pow_two, pow_two, mul_assoc, mul_assoc] at key
    simp [inv_mul_cancel_left] at key
    rw [← mul_assoc, ← mul_assoc] at key
    simp [inv_mul_cancel_right] at key
    simp [key]
  /- If G is abelian, then f is a homomorphism-/
  · --  ∀ a b : G，a * b = b * a
    intro eq a b
    have h1: f G a * f G b = a^2 * b^2 := rfl

    have h2: f G (a * b) = (a * b)^2 := rfl
    rw [h1, h2]
    rw [pow_two, pow_two, pow_two, mul_assoc, mul_assoc]
    simp [inv_mul_cancel_left]
    rw [← mul_assoc, ← mul_assoc]
    simp [inv_mul_cancel_right]
    simp [eq]

I want to use the definition "CommGroup" and "MonoidHom" instead of the theorem conditions. But I don't know how to express it in the theorem line, and the code always be wrong . Is there anyone who can help me?

[Aaron Liu]

I don't think that will be easy, because both CommGroup and MonoidHom are both bundled

[Alex Meiburg]

Here are two both kind of terrible ways to write it:

import Mathlib

instance setFunFunlike {α β : Type*} (S : Set (α → β)) : FunLike S α β where
  coe f := f
  coe_injective' := Subtype.val_injective

open Subgroup

variable (G : Type*) [inst : Group G]

/-- f: G → G，x→ x\^2   -/
def f : G → G := fun (x : G) ↦ x^2

/-- f is a homomorphism ↔ G is abelian -/
theorem f_homo_iff_G_abelian: (MonoidHomClass ({f G} : Set (G → G)) G G)
    ↔ (Std.Commutative (fun (x y : G) ↦ x * y)) := by
  sorry

/-- f is a homomorphism ↔ G is abelian -/
theorem f_homo_iff_G_abelian_alt: (∃ (f' : MonoidHom G G), ⇑f' = f G)
    ↔ (∃ (CG : CommGroup G), CG.toGroup = inst) := by
  sorry

[Aaron Liu]

We have docs#IsMulCommutative