-- Module: Mathlib.Algebra.Category.AlgCat.Limits
Goal:
R : Type u
inst : CommRing R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ AlgCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{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)
j : J
refine_4 :
  HAdd.hAdd (α := (↑(F.obj j) : Type w)) (β := (↑(F.obj j) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{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 : AlgCat.{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 (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{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 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)
                      (F.obj j)) ↦
              x ∈
                (F ⋙
                    forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                      (CC := carrier)).sections)
              (fun (j : J) ↦
                (ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{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 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)
                      (F.obj j)) ↦
              x ∈
                (F ⋙
                    forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                      (CC := carrier)).sections)
              (fun (j : J) ↦
                (ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{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)
              ⋯)) :
        (j : J) → ToType (F.obj j))
      j
⊢ Eq.{w + 1} (α :=
    (F ⋙
          forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
            carrier)).obj
      j)
    ((↑((Equiv.symm
                (equivShrink
                  (↑(F ⋙
                          forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{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 (AlgCat R)).sections : Type (max w v))) →
                (↑(F ⋙ forget (AlgCat R)).sections : Type (max w v)))
            (EquivLike.coe (E :=
              (↑(F ⋙
                        forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                          (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)).sections :
                  Type (max w v)) ≃
                Shrink.{w, max w v}
                  (↑(F ⋙
                          forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                            (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)).sections :
                    Type (max w v)))
              (equivShrink
                (↑(F ⋙
                        forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                          (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)).sections :
                  Type (max w v)))
              (Subtype.mk (p :=
                fun
                  (x :
                    (j : J) →
                      (F ⋙
                            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                              (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)).obj
                        j) ↦
                x ∈
                  (F ⋙
                      forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                        (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)).sections)
                (fun (j : J) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun)
                        (NatTrans.app
                          (Cone.π
                            (Functor.mapCone
                              (forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                                (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier))
                              s))
                          j) :
                      (a : (fun (X : Type w) ↦ X) (((Functor.const J).obj ((forget (AlgCat R)).mapCone s).pt).obj j)) →
                        (fun (X : Type w) ↦ X) ((F ⋙ forget (AlgCat R)).obj j))
                    (x + y))
                ⋯))) :
        (j : J) → (F ⋙ forget (AlgCat R)).obj j)
      j)
    ((↑((Equiv.symm
                (equivShrink
                  (↑(F ⋙
                          forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{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 (AlgCat R)).sections : Type (max w v))) →
                (↑(F ⋙ forget (AlgCat R)).sections : Type (max w v)))
            (EquivLike.coe (E :=
                (↑(F ⋙
                          forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                            (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)).sections :
                    Type (max w v)) ≃
                  Shrink.{w, max w v}
                    (↑(F ⋙
                            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                              (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)).sections :
                      Type (max w v)))
                (equivShrink
                  (↑(F ⋙
                          forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                            (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)).sections :
                    Type (max w v)))
                (Subtype.mk (p :=
                  fun
                    (x :
                      (j : J) →
                        (F ⋙
                              forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                                (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)).obj
                          j) ↦
                  x ∈
                    (F ⋙
                        forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                          (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)).sections)
                  (fun (j : J) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun)
                          (NatTrans.app
                            (Cone.π
                              (Functor.mapCone
                                (forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                                  (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier))
                                s))
                            j) :
                        (a :
                            (fun (X : Type w) ↦ X) (((Functor.const J).obj ((forget (AlgCat R)).mapCone s).pt).obj j)) →
                          (fun (X : Type w) ↦ X) ((F ⋙ forget (AlgCat R)).obj j))
                      x)
                  ⋯) +
              EquivLike.coe (E :=
                (↑(F ⋙
                          forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                            (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)).sections :
                    Type (max w v)) ≃
                  Shrink.{w, max w v}
                    (↑(F ⋙
                            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                              (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)).sections :
                      Type (max w v)))
                (equivShrink
                  (↑(F ⋙
                          forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                            (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)).sections :
                    Type (max w v)))
                (Subtype.mk (p :=
                  fun
                    (x :
                      (j : J) →
                        (F ⋙
                              forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                                (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)).obj
                          j) ↦
                  x ∈
                    (F ⋙
                        forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                          (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)).sections)
                  (fun (j : J) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun)
                          (NatTrans.app
                            (Cone.π
                              (Functor.mapCone
                                (forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                                  (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier))
                                s))
                            j) :
                        (a :
                            (fun (X : Type w) ↦ X) (((Functor.const J).obj ((forget (AlgCat R)).mapCone s).pt).obj j)) →
                          (fun (X : Type w) ↦ X) ((F ⋙ forget (AlgCat R)).obj j))
                      y)
                  ⋯))) :
        (j : J) → (F ⋙ forget (AlgCat R)).obj j)
      j)

Tactic:
simp