-- 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))
j : J
this : 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) RingCat (FD := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CD :=
                RingCat.carrier) ⋙
              forget₂ RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC := RingCat.carrier)
                SemiRingCat (FD := fun (R S : SemiRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CD :=
                SemiRingCat.carrier)) ⋙
          forget SemiRingCat (FC := fun (R S : SemiRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
            SemiRingCat.carrier)).sections :
    Type (max v w)) :=
  ⋯
x : R
simp :
  Eq.{w + 1} (α :=
    ToType (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier) (F.obj j))
    ((↑((algebraMap R
                  (↑(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 : R) → (↑(F ⋙ forget (AlgCat R)).sections : Type (max w v)))
              x) :
          (j : J) → ToType (F.obj j))
        j :
      ToType (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier) (F.obj j))
    ((algebraMap R
            (ToType (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)
              (F.obj j)) :
          (a : R) → ToType (F.obj j))
        x :
      ToType (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier) (F.obj j))
⊢ Eq (α :=
    (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)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((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))).π.app
              j) :
          (a :
              (fun (X : Type w) ↦ X)
                (((Functor.const J).obj (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt).obj j)) →
            (fun (X : Type w) ↦ X) ((F ⋙ forget (AlgCat R)).obj j))
        ((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)
            x :
          (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) :
      (fun (X : Type w) ↦ X)
        ((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))
    ((algebraMap R
            ((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) :
          (a : R) → (F ⋙ forget (AlgCat R)).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)).obj
        j)

Tactic:
simp only [Functor.comp_obj, Types.Small.limitCone_pt, Functor.const_obj_obj,
        Types.Small.limitCone_π_app, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk,
        ← Shrink.algEquiv_apply R, AlgEquiv.commutes]

Premises used: CategoryTheory.Functor.comp_obj, AlgEquiv.commutes, TypeCat.Fun.coe_mk, CategoryTheory.Limits.Types.Small.limitCone_pt, Shrink.algEquiv_apply, CategoryTheory.Limits.Types.Small.limitCone_π_app, CategoryTheory.Functor.const_obj_obj, CategoryTheory.ConcreteCategory.hom_ofHom