-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X' X : GrpCat
Y : CommGrpCat
f : X' ⟶ X
g :
  X ⟶
    Functor.obj
      (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
        CommGrpCat.carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := carrier))
      Y
hf :
  ∀ (x : (↑(abelianize.obj X') : Type u)),
    Eq (α := (↑Y : Type u))
      ((CommGrpCat.Hom.hom
              ((Equiv.symm
                    (Equiv.trans (β :=
                      ToHom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) X'
                        (Functor.obj
                          (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                            (CC := CommGrpCat.carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{u}) ↦
                            (↑x1 : Type u) →* (↑x2 : Type u)) (CD := carrier))
                          Y))
                      (Equiv.trans (β :=
                        ToHom (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                          CommGrpCat.carrier) (abelianize.obj X') Y)
                        (ConcreteCategory.homEquiv (FC := fun (x1 x2 : CommGrpCat.{u}) ↦
                          (↑x1 : Type u) →* (↑x2 : Type u)) (CC := CommGrpCat.carrier))
                        (Equiv.symm Abelianization.lift))
                      (Equiv.symm
                        (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                          (CC := carrier)))) :
                  (a : X' ⟶ (forget₂ CommGrpCat GrpCat).obj Y) → abelianize.obj X' ⟶ Y)
                (f ≫ g)) :
            (a : (↑(abelianize.obj X') : Type u)) → (↑Y : Type u))
          x :
        (↑Y : Type u))
      ((CommGrpCat.Hom.hom
              (abelianize.map f ≫
                (Equiv.symm
                      (Equiv.trans (β :=
                        ToHom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) X
                          (Functor.obj
                            (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                              (CC := CommGrpCat.carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{u}) ↦
                              (↑x1 : Type u) →* (↑x2 : Type u)) (CD := carrier))
                            Y))
                        (Equiv.trans (β :=
                          ToHom (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                            CommGrpCat.carrier) (abelianize.obj X) Y)
                          (ConcreteCategory.homEquiv (FC := fun (x1 x2 : CommGrpCat.{u}) ↦
                            (↑x1 : Type u) →* (↑x2 : Type u)) (CC := CommGrpCat.carrier))
                          (Equiv.symm Abelianization.lift))
                        (Equiv.symm
                          (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                            (CC := carrier)))) :
                    (a : X ⟶ (forget₂ CommGrpCat GrpCat).obj Y) → abelianize.obj X ⟶ Y)
                  g) :
            (a : (↑(abelianize.obj X') : Type u)) → (↑Y : Type u))
          x :
        (↑Y : Type u))
⊢ Eq (α := abelianize.obj X' ⟶ Y)
    ((Equiv.symm
            (Equiv.trans (β :=
              ToHom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) X'
                (Functor.obj
                  (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                    CommGrpCat.carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                    (CD := carrier))
                  Y))
              (Equiv.trans (β :=
                ToHom (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := CommGrpCat.carrier)
                  (abelianize.obj X') Y)
                (ConcreteCategory.homEquiv (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                  (CC := CommGrpCat.carrier))
                (Equiv.symm Abelianization.lift))
              (Equiv.symm
                (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                  carrier)))) :
          (a : X' ⟶ (forget₂ CommGrpCat GrpCat).obj Y) → abelianize.obj X' ⟶ Y)
        (f ≫ g) :
      abelianize.obj X' ⟶ Y)
    (abelianize.map f ≫
        (Equiv.symm
              (Equiv.trans (β :=
                ToHom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) X
                  (Functor.obj
                    (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                      CommGrpCat.carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                      (CD := carrier))
                    Y))
                (Equiv.trans (β :=
                  ToHom (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                    CommGrpCat.carrier) (abelianize.obj X) Y)
                  (ConcreteCategory.homEquiv (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                    (CC := CommGrpCat.carrier))
                  (Equiv.symm Abelianization.lift))
                (Equiv.symm
                  (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                    carrier)))) :
            (a : X ⟶ (forget₂ CommGrpCat GrpCat).obj Y) → abelianize.obj X ⟶ Y)
          g :
      abelianize.obj X' ⟶ Y)

Tactic:
ext