-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Adjunctions (goal)
Goal:
M N : AddCommMonCat
f : M ⟶ N
⊢ Eq (α :=
    Functor.obj
        (forget AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            carrier) ⋙
          free)
        M ⟶
      Functor.obj (𝟭 AddCommMonCat) N)
    (CategoryTheory.Functor.map
          (forget AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              carrier) ⋙
            free)
          f ≫
        ofHom
          ((Finsupp.liftAddHom :
              (a : (forget AddCommMonCat).obj N → ℕ →+ (↑N : Type u)) →
                ((forget AddCommMonCat).obj N →₀ ℕ) →+ (↑N : Type u))
            (⇑(multiplesHom (↑N : Type u)) : (a : (↑N : Type u)) → ℕ →+ (↑N : Type u))) :
      Functor.obj
          (forget AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              carrier) ⋙
            free)
          M ⟶
        Functor.obj (𝟭 AddCommMonCat) N)
    (ofHom
          ((Finsupp.liftAddHom :
              (a : (forget AddCommMonCat).obj M → ℕ →+ (↑M : Type u)) →
                ((forget AddCommMonCat).obj M →₀ ℕ) →+ (↑M : Type u))
            (⇑(multiplesHom (↑M : Type u)) : (a : (↑M : Type u)) → ℕ →+ (↑M : Type u))) ≫
        CategoryTheory.Functor.map (𝟭 AddCommMonCat) f :
      Functor.obj
          (forget AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              carrier) ⋙
            free)
          M ⟶
        Functor.obj (𝟭 AddCommMonCat) N)
have hf : Eq (α :=
  (↑(Functor.obj
          (forget AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              carrier) ⋙
            free)
          M) :
      Type u) →+
    (↑(Functor.obj (𝟭 AddCommMonCat) N) : Type u))
  (Hom.hom
      (CategoryTheory.Functor.map
          (forget AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              carrier) ⋙
            free)
          f ≫
        ofHom
          ((Finsupp.liftAddHom :
              (a : (forget AddCommMonCat).obj N → ℕ →+ (↑N : Type u)) →
                ((forget AddCommMonCat).obj N →₀ ℕ) →+ (↑N : Type u))
            (⇑(multiplesHom (↑N : Type u)) : (a : (↑N : Type u)) → ℕ →+ (↑N : Type u)))) :
    (↑(Functor.obj
            (forget AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                carrier) ⋙
              free)
            M) :
        Type u) →+
      (↑(Functor.obj (𝟭 AddCommMonCat) N) : Type u))
  (Hom.hom
      (ofHom
          ((Finsupp.liftAddHom :
              (a : (forget AddCommMonCat).obj M → ℕ →+ (↑M : Type u)) →
                ((forget AddCommMonCat).obj M →₀ ℕ) →+ (↑M : Type u))
            (⇑(multiplesHom (↑M : Type u)) : (a : (↑M : Type u)) → ℕ →+ (↑M : Type u))) ≫
        CategoryTheory.Functor.map (𝟭 AddCommMonCat) f) :
    (↑(Functor.obj
            (forget AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                carrier) ⋙
              free)
            M) :
        Type u) →+
      (↑(Functor.obj (𝟭 AddCommMonCat) N) : Type u))
Tactic: ext1