-- 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))
s : Cone F
r : R
x : (↑s.1 : Type w)
⊢ AddHom.toFun
      {
        toFun :=
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                (IsLimit.lift
                  (Types.Small.limitConeIsLimit
                    (F ⋙
                      forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                        (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier)))
                  (Functor.mapCone
                    (forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                      (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier))
                    s))) :
            (a : (fun (X : Type w) ↦ X) ((forget (ModuleCat R)).mapCone s).pt) →
              (fun (X : Type w) ↦ X) (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt),
        map_add' := ⋯ }
      (r • x) =
    HSMul.hSMul (α := R) (β :=
      (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)
      ((RingHom.id R : (a : R) → R) r : R)
      (AddHom.toFun
        {
          toFun :=
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                  (IsLimit.lift
                    (Types.Small.limitConeIsLimit
                      (F ⋙
                        forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                          (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier)))
                    (Functor.mapCone
                      (forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                        (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier))
                      s))) :
              (a : (fun (X : Type w) ↦ X) ((forget (ModuleCat R)).mapCone s).pt) →
                (fun (X : Type w) ↦ X) (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt),
          map_add' := ⋯ :
          (↑s.1 : Type w) →ₙ+
            (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 }
        x)
have refine_2 : Subtype.mk (p :=
    fun
      (x :
        (j : J) →
          ToType (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier)
            (F.obj j)) ↦
    x ∈
      (F ⋙
          forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
            (CC := carrier)).sections)
    (fun (j : J) ↦
      HSMul.hSMul (β := (↑(F.obj j) : Type w)) r
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC :=
                carrier) (s.π.app j) :
              (a : (↑s.pt : Type w)) → (↑(F.obj j) : Type w))
            x :
          (↑(F.obj j) : Type w)))
    sorry =
  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)))
    r
    (Subtype.mk (p :=
      fun
        (x :
          (j : J) →
            ToType (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier)
              (F.obj j)) ↦
      x ∈
        (F ⋙
            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
              (CC := carrier)).sections)
      (fun (j : J) ↦
        (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC :=
              carrier) (s.π.app j) :
            (a : (↑s.pt : Type w)) → (↑(F.obj j) : Type w))
          x)
      sorry)
Tactic: simp [← equivShrink_smul]