-- Lean 4 proof step from Mathlib.Algebra.Category.AlgCat.Limits (goal)
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
⊢ 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 : ((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)))
        ⋯) =
    (equivShrink ↥(sectionsSubalgebra F) :
        (a : ↥(sectionsSubalgebra F)) → (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt)
      ((algebraMap R ↥(sectionsSubalgebra F) : (a : R) → ↥(sectionsSubalgebra F)) r)
have refine_5 : Eq (α :=
  { 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 })
  (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)))
    sorry)
  ((algebraMap R ↥(sectionsSubalgebra F) : (a : R) → ↥(sectionsSubalgebra F)) r)
Tactic: apply congrArg