-- 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))
s : Cone F
x y : (↑s.1 : Type w)
refine_1 :
  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) ↦
        HAdd.hAdd (α := (↑(F.obj j) : Type w)) (β := (↑(F.obj j) : Type w))
          ((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))
          ((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))
              y :
            (↑(F.obj j) : Type w)))
      ⋯ =
    HAdd.hAdd (α :=
      (↑(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)))
      (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)
        ⋯)
      (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))
            y)
        ⋯)
⊢ (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)

Tactic:
simp [← equivShrink_add]

Premises used: equivShrink_add