-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Adjunctions (goal)
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
x : (↑(abelianize.obj X') : Type u)
⊢ Eq (α := (↑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))
    ((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))
have hf : ∀ (x : (↑X' : Type u)),
  Eq (α := (↑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 : Abelianization (↑X' : Type u)) → (↑Y : Type u))
        ((Abelianization.of : (a : (↑X' : Type u)) → Abelianization (↑X' : Type u)) x : Abelianization (↑X' : Type u)) :
      (↑Y : Type u))
    ((((Equiv.symm
                  (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) → ToHom X' ((forget₂ CommGrpCat GrpCat).obj Y))
              (f ≫ g) :
            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)) :
          (a : (↑X' : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
Tactic: apply Abelianization.lift_unique