-- 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))
        M →
      ℕ →+ (↑(Functor.obj (𝟭 AddCommMonCat) N) : Type u))
    ((AddEquiv.symm Finsupp.liftAddHom :
          (a : ((forget AddCommMonCat).obj M →₀ ℕ) →+ (↑((𝟭 AddCommMonCat).obj N) : Type u)) →
            (forget AddCommMonCat).obj M → ℕ →+ (↑((𝟭 AddCommMonCat).obj 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)) :
      Functor.obj
          (forget AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            carrier))
          M →
        ℕ →+ (↑(Functor.obj (𝟭 AddCommMonCat) N) : Type u))
    ((AddEquiv.symm Finsupp.liftAddHom :
          (a : ((forget AddCommMonCat).obj M →₀ ℕ) →+ (↑((𝟭 AddCommMonCat).obj N) : Type u)) →
            (forget AddCommMonCat).obj M → ℕ →+ (↑((𝟭 AddCommMonCat).obj 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))
          M →
        ℕ →+ (↑(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) :
        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:
apply Finsupp.liftAddHom.symm.injective

Premises used: AddEquiv.injective, Finsupp.liftAddHom, AddEquiv.symm