-- 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) :
        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))
have 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))
Tactic: apply Finsupp.liftAddHom.symm.injective