-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f : M ⟶ N
r : R
⊢ Eq (α :=
    Functor.obj
        (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
          (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
          (CD := AddCommGrpCat.carrier))
        M ⟶
      Functor.obj
        (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
          (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
          (CD := AddCommGrpCat.carrier))
        N)
    (CategoryTheory.Functor.map
        (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
          (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
          (CD := AddCommGrpCat.carrier))
        f ≫
      (N.smul : (a : R) → End ((forget₂ (ModuleCat R) AddCommGrpCat).obj N)) r)
    ((M.smul : (a : R) → End ((forget₂ (ModuleCat R) AddCommGrpCat).obj M)) r ≫
      CategoryTheory.Functor.map
        (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
          (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
          (CD := AddCommGrpCat.carrier))
        f)
have hf : ∀
  (x :
    (↑(Functor.obj
          (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
            (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
            (CD := AddCommGrpCat.carrier))
          M) :
      Type v)),
  Eq (α :=
    (↑(Functor.obj
          (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
            (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
            (CD := AddCommGrpCat.carrier))
          N) :
      Type v))
    ((AddCommGrpCat.Hom.hom
            (CategoryTheory.Functor.map
                (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦
                  (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommGrpCat (FD :=
                  fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
                f ≫
              (N.smul : (a : R) → End ((forget₂ (ModuleCat R) AddCommGrpCat).obj N)) r) :
          (a : (↑((forget₂ (ModuleCat R) AddCommGrpCat).obj M) : Type v)) →
            (↑((forget₂ (ModuleCat R) AddCommGrpCat).obj N) : Type v))
        x :
      (↑(Functor.obj
            (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
              (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
              (CD := AddCommGrpCat.carrier))
            N) :
        Type v))
    ((AddCommGrpCat.Hom.hom
            ((M.smul : (a : R) → End ((forget₂ (ModuleCat R) AddCommGrpCat).obj M)) r ≫
              CategoryTheory.Functor.map
                (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦
                  (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommGrpCat (FD :=
                  fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
                f) :
          (a : (↑((forget₂ (ModuleCat R) AddCommGrpCat).obj M) : Type v)) →
            (↑((forget₂ (ModuleCat R) AddCommGrpCat).obj N) : Type v))
        x :
      (↑(Functor.obj
            (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
              (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
              (CD := AddCommGrpCat.carrier))
            N) :
        Type v))
Tactic: ext x