-- 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
r : R
refine_5 :
  ∀ (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)
      ((↑(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 : ((Functor.const J).obj ((forget (AlgCat R)).mapCone s).pt).obj j) →
                      (F ⋙ forget (AlgCat R)).obj j)
                  ((algebraMap R (↑s.1 : Type w) : (a : R) → (↑s.1 : Type w)) r : (↑s.1 : Type w)))
              ⋯) :
          (j : J) → (F ⋙ forget (AlgCat R)).obj j)
        j)
      ((↑((algebraMap R ↥(sectionsSubalgebra F) : (a : R) → ↥(sectionsSubalgebra F)) r) :
          (j : J) → (F ⋙ forget (AlgCat R)).obj j)
        j)
⊢ Eq (α :=
    (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)
    (↑(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 : ((Functor.const J).obj ((forget (AlgCat R)).mapCone s).pt).obj j) → (F ⋙ forget (AlgCat R)).obj j)
              ((algebraMap R (↑s.1 : Type w) : (a : R) → (↑s.1 : Type w)) r : (↑s.1 : Type w)))
          ⋯) :
      (j : J) → (F ⋙ forget (AlgCat R)).obj j)
    (↑((algebraMap R ↥(sectionsSubalgebra F) : (a : R) → ↥(sectionsSubalgebra F)) r) :
      (j : J) → (F ⋙ forget (AlgCat R)).obj j)

Tactic:
ext j