-- Module: Mathlib.Algebra.Category.ModuleCat.Limits
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))
refine_1 :
  ∀ (s : Cone F) (x y : (↑s.1 : Type w)),
    (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)
        (x + y) =
      HAdd.hAdd (α :=
        (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)
        (β :=
        (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)
                (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)
            x :
          (fun (X : Type w) ↦ X)
            (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)
                (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)
            y :
          (fun (X : Type w) ↦ X)
            (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)
refine_2 :
  ∀ (s : Cone F) (m : 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' := ⋯ }
        (m • 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) m : 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)
⊢ IsLimit (limitCone F)

Tactic:
refine IsLimit.ofFaithful (forget (ModuleCat R)) (Types.Small.limitConeIsLimit.{v, w} _)
    (fun s => ofHom ⟨⟨(Types.Small.limitConeIsLimit.{v, w} _).lift
                ((forget (ModuleCat R)).mapCone s), ?_⟩, ?_⟩)
    (fun s => rfl)