-- 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))
refine_1 :
  ∀ (s : Cone F),
    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))
              1)
          ⋯) =
      1
refine_2 :
  ∀ (s : Cone F) (x y : (↑s.1 : Type w)),
    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)
            ⋯)
refine_3 :
  ∀ (s : Cone F),
    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))
              0)
          ⋯) =
      0
refine_4 :
  ∀ (s : Cone F) (x y : (↑s.1 : Type w)),
    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)
            ⋯)
refine_5 :
  ∀ (s : Cone F) (r : R),
    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))
              ((algebraMap R (↑s.1 : Type w) : (a : R) → (↑s.1 : Type w)) r : (↑s.1 : Type w)))
          ⋯) =
      (algebraMap R
            (Types.Small.limitCone
                (F ⋙
                  forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                    (CC := carrier))).pt :
          (a : R) → (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt)
        r
⊢ IsLimit (limitCone F)

Tactic:
refine
    IsLimit.ofFaithful (forget (AlgCat R)) (Types.Small.limitConeIsLimit.{v, w} _)
      (fun s => ofHom
        { toFun := _, map_one' := ?_, map_mul' := ?_, map_zero' := ?_, map_add' := ?_,
          commutes' := ?_ })
      (fun s => rfl)