-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Limits (goal)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
              (CC := carrier)).sections :
      Type (max v w))
j : J
x : R
x_1 :
  (Types.Small.limitCone
      (F ⋙
        forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
          (CC := carrier))).pt
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((Types.Small.limitCone
                  (F ⋙
                    forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                      (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier))).π.app
            j) :
        (a :
            (fun (X : Type w) ↦ X)
              (((Functor.const J).obj (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt).obj j)) →
          (fun (X : Type w) ↦ X) ((F ⋙ forget (ModuleCat R)).obj j))
      (x • x_1) =
    HSMul.hSMul (α := R) (β :=
      (F ⋙
            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
              (CC := carrier)).obj
        j)
      ((RingHom.id R : (a : R) → R) x : R)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((Types.Small.limitCone
                      (F ⋙
                        forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                          (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier))).π.app
                j) :
            (a :
                (fun (X : Type w) ↦ X)
                  (((Functor.const J).obj (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt).obj j)) →
              (fun (X : Type w) ↦ X) ((F ⋙ forget (ModuleCat R)).obj j))
          x_1 :
        (fun (X : Type w) ↦ X)
          ((F ⋙
                forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                  (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier)).obj
            j))
have simp : (↑(HSMul.hSMul (β :=
          (↑(F ⋙
                  forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                    (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier)).sections :
            Type (max w v)))
          x
          ((Equiv.symm
                  (equivShrink
                    (↑(F ⋙
                            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                              (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier)).sections :
                      Type (max w v))) :
                (a : Shrink.{w, max v w} (↑(F ⋙ forget (ModuleCat R)).sections : Type (max w v))) →
                  (↑(F ⋙ forget (ModuleCat R)).sections : Type (max w v)))
              x_1 :
            (↑(F ⋙
                    forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                      (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier)).sections :
              Type (max w v)))) :
      (j : J) → ToType (F.obj j))
    j =
  HSMul.hSMul (β :=
    ToType (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier) (F.obj j)) x
    ((↑((Equiv.symm
                (equivShrink
                  (↑(F ⋙
                          forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                            (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier)).sections :
                    Type (max w v))) :
              (a : Shrink.{w, max w v} (↑(F ⋙ forget (ModuleCat R)).sections : Type (max w v))) →
                (↑(F ⋙ forget (ModuleCat R)).sections : Type (max w v)))
            x_1) :
        (j : J) → ToType (F.obj j))
      j)
Tactic: simp