-- 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)
refine_4 :
  ∀ (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)
⊢ 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))
        ⋯) =
    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)
          ⋯)

Tactic:
ext j