-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Adjunctions (goal)
Goal:
X' X : Semigrp
Y : MonCat
f : X' ⟶ X
g :
  X ⟶
    Functor.obj
      (forget₂ MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) Semigrp (FD :=
        fun (x1 x2 : Semigrp.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CD := Semigrp.carrier))
      Y
hf :
  Eq (α := (↑Y : Type u))
    ((Hom.hom
            ((Equiv.symm
                  (Equiv.trans (β :=
                    ToHom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                      (adjoinOne.obj X') Y)
                    (ConcreteCategory.homEquiv (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                      (CC := carrier))
                    (Equiv.trans (Equiv.symm WithOne.lift)
                      (Equiv.symm
                        (ConcreteCategory.homEquiv (FC := fun (x1 x2 : Semigrp.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u))
                          (CC := Semigrp.carrier))))) :
                (a : X' ⟶ (forget₂ MonCat Semigrp).obj Y) → adjoinOne.obj X' ⟶ Y)
              (f ≫ g)) :
          (a : (↑(adjoinOne.obj X') : Type u)) → (↑Y : Type u))
        none :
      (↑Y : Type u))
    ((Hom.hom
            (adjoinOne.map f ≫
              (Equiv.symm
                    (Equiv.trans (β :=
                      ToHom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                        (adjoinOne.obj X) Y)
                      (ConcreteCategory.homEquiv (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                        (CC := carrier))
                      (Equiv.trans (Equiv.symm WithOne.lift)
                        (Equiv.symm
                          (ConcreteCategory.homEquiv (FC := fun (x1 x2 : Semigrp.{u}) ↦
                            (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := Semigrp.carrier))))) :
                  (a : X ⟶ (forget₂ MonCat Semigrp).obj Y) → adjoinOne.obj X ⟶ Y)
                g) :
          (a : (↑(adjoinOne.obj X') : Type u)) → (↑Y : Type u))
        none :
      (↑Y : Type u))
⊢ Eq (α := adjoinOne.obj X' ⟶ Y)
    ((Equiv.symm
            (Equiv.trans (β :=
              ToHom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                (adjoinOne.obj X') Y)
              (ConcreteCategory.homEquiv (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier))
              (Equiv.trans (Equiv.symm WithOne.lift)
                (Equiv.symm
                  (ConcreteCategory.homEquiv (FC := fun (x1 x2 : Semigrp.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u))
                    (CC := Semigrp.carrier))))) :
          (a : X' ⟶ (forget₂ MonCat Semigrp).obj Y) → adjoinOne.obj X' ⟶ Y)
        (f ≫ g) :
      adjoinOne.obj X' ⟶ Y)
    (adjoinOne.map f ≫
        (Equiv.symm
              (Equiv.trans (β :=
                ToHom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                  (adjoinOne.obj X) Y)
                (ConcreteCategory.homEquiv (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                  carrier))
                (Equiv.trans (Equiv.symm WithOne.lift)
                  (Equiv.symm
                    (ConcreteCategory.homEquiv (FC := fun (x1 x2 : Semigrp.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u))
                      (CC := Semigrp.carrier))))) :
            (a : X ⟶ (forget₂ MonCat Semigrp).obj Y) → adjoinOne.obj X ⟶ Y)
          g :
      adjoinOne.obj X' ⟶ Y)
have hf₁ : ∀ (val : (↑X' : Type u)),
  Eq (α := (↑Y : Type u))
    ((Hom.hom
            ((Equiv.symm
                  (Equiv.trans (β :=
                    ToHom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                      (adjoinOne.obj X') Y)
                    (ConcreteCategory.homEquiv (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                      (CC := carrier))
                    (Equiv.trans (Equiv.symm WithOne.lift)
                      (Equiv.symm
                        (ConcreteCategory.homEquiv (FC := fun (x1 x2 : Semigrp.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u))
                          (CC := Semigrp.carrier))))) :
                (a : X' ⟶ (forget₂ MonCat Semigrp).obj Y) → adjoinOne.obj X' ⟶ Y)
              (f ≫ g)) :
          (a : (↑(adjoinOne.obj X') : Type u)) → (↑Y : Type u))
        (some val) :
      (↑Y : Type u))
    ((Hom.hom
            (adjoinOne.map f ≫
              (Equiv.symm
                    (Equiv.trans (β :=
                      ToHom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                        (adjoinOne.obj X) Y)
                      (ConcreteCategory.homEquiv (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                        (CC := carrier))
                      (Equiv.trans (Equiv.symm WithOne.lift)
                        (Equiv.symm
                          (ConcreteCategory.homEquiv (FC := fun (x1 x2 : Semigrp.{u}) ↦
                            (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := Semigrp.carrier))))) :
                  (a : X ⟶ (forget₂ MonCat Semigrp).obj Y) → adjoinOne.obj X ⟶ Y)
                g) :
          (a : (↑(adjoinOne.obj X') : Type u)) → (↑Y : Type u))
        (some val) :
      (↑Y : Type u))
Tactic: ext ⟨_ | _⟩