-- Module: Mathlib.Algebra.Category.MonCat.Adjunctions
Goal:
M N : AddCommMonCat
f : M ⟶ N
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))
⊢ 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)

Tactic:
ext1