-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f : M ⟶ N
r : R
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))
⊢ 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)

Tactic:
ext x