-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : (Y : C) → IsLimit (F := F ⋙ obj (evaluation C (Type w')) Y) (mapCone (obj (evaluation C (Type w')) Y) c)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h :
  Eq (α := (fun (X : Type w') ↦ X) (c.pt.obj (obj.{w, v, w, u} (obj (const J) cX.pt) j)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (cX.ι.app j)) :
          (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) →
            (fun (X : Type w') ↦ X) (c.pt.obj (((const J).obj cX.pt).obj j)))
        x₁ :
      (fun (X : Type w') ↦ X) (c.pt.obj (obj.{w, v, w, u} (obj (const J) cX.pt) j)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (cX.ι.app j)) :
          (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) →
            (fun (X : Type w') ↦ X) (c.pt.obj (((const J).obj cX.pt).obj j)))
        x₂ :
      (fun (X : Type w') ↦ X) (c.pt.obj (obj.{w, v, w, u} (obj (const J) cX.pt) j)))
this : IsFiltered J
y₁ : (↑(F ⋙ obj (evaluation C (Type w')) (X.obj j)).sections : Type (max w' u')) :=
  (Types.isLimitEquivSections (hc (X.obj j)) :
      (a : (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt) →
        (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u')))
    x₁
y₂ : (↑(F ⋙ obj (evaluation C (Type w')) (X.obj j)).sections : Type (max w' u')) :=
  (Types.isLimitEquivSections (hc (X.obj j)) :
      (a : (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt) →
        (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u')))
    x₂
hy₁ :
  (Equiv.symm (Types.isLimitEquivSections (hc (X.obj j))) :
        (a : (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u'))) →
          (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt)
      y₁ =
    x₁
hy₂ :
  (Equiv.symm (Types.isLimitEquivSections (hc (X.obj j))) :
        (a : (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u'))) →
          (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt)
      y₂ =
    x₂
H :
  ∀ (k : K),
    ∃ (j_1 : J) (f : j ⟶ j_1),
      Eq (α := (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ F.obj k).map f) :
              (a : (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j)) → (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
            ((↑y₁ : (j_2 : K) → (F ⋙ (evaluation C (Type w')).obj (X.obj j)).obj j_2) k) :
          (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ F.obj k).map f) :
              (a : (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j)) → (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
            ((↑y₂ : (j_2 : K) → (F ⋙ (evaluation C (Type w')).obj (X.obj j)).obj j_2) k) :
          (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
j₁ : (k : K) → J :=
  fun (k : K) ↦
    ⋯.choose (p := fun (j_1 : J) ↦
      ∃ (f : j ⟶ j_1),
        Eq (α := (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ F.obj k).map f) :
                (a : (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j)) → (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
              ((↑y₁ : (j_2 : K) → (F ⋙ (evaluation C (Type w')).obj (X.obj j)).obj j_2) k) :
            (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ F.obj k).map f) :
                (a : (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j)) → (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
              ((↑y₂ : (j_2 : K) → (F ⋙ (evaluation C (Type w')).obj (X.obj j)).obj j_2) k) :
            (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1)))
f : (k : K) → j ⟶ j₁ k :=
  fun (k : K) ↦
    ⋯.choose (p :=
      fun
        (f :
          j ⟶
            ⋯.choose (p := fun (j_1 : J) ↦
              ∃ (f : j ⟶ j_1),
                Eq (α := (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ F.obj k).map f) :
                        (a : (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j)) →
                          (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
                      ((↑y₁ : (j_2 : K) → (F ⋙ (evaluation C (Type w')).obj (X.obj j)).obj j_2) k) :
                    (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ F.obj k).map f) :
                        (a : (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j)) →
                          (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
                      ((↑y₂ : (j_2 : K) → (F ⋙ (evaluation C (Type w')).obj (X.obj j)).obj j_2) k) :
                    (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1)))) ↦
      Eq (α :=
        (fun (X : Type w') ↦ X)
          ((X ⋙ F.obj k).obj
            (⋯.choose (p := fun (j_1 : J) ↦
              ∃ (f : j ⟶ j_1),
                Eq (α := (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ F.obj k).map f) :
                        (a : (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j)) →
                          (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
                      ((↑y₁ : (j_2 : K) → (F ⋙ (evaluation C (Type w')).obj (X.obj j)).obj j_2) k) :
                    (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ F.obj k).map f) :
                        (a : (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j)) →
                          (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
                      ((↑y₂ : (j_2 : K) → (F ⋙ (evaluation C (Type w')).obj (X.obj j)).obj j_2) k) :
                    (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ F.obj k).map f) :
              (a : (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j)) →
                (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj ⋯.choose))
            ((↑y₁ : (j_1 : K) → (F ⋙ (evaluation C (Type w')).obj (X.obj j)).obj j_1) k) :
          (fun (X : Type w') ↦ X)
            ((X ⋙ F.obj k).obj
              (⋯.choose (p := fun (j_1 : J) ↦
                ∃ (f : j ⟶ j_1),
                  Eq (α := (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ F.obj k).map f) :
                          (a : (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j)) →
                            (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
                        ((↑y₁ : (j_2 : K) → (F ⋙ (evaluation C (Type w')).obj (X.obj j)).obj j_2) k) :
                      (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ F.obj k).map f) :
                          (a : (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j)) →
                            (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
                        ((↑y₂ : (j_2 : K) → (F ⋙ (evaluation C (Type w')).obj (X.obj j)).obj j_2) k) :
                      (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ F.obj k).map f) :
              (a : (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j)) →
                (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj ⋯.choose))
            ((↑y₂ : (j_1 : K) → (F ⋙ (evaluation C (Type w')).obj (X.obj j)).obj j_1) k) :
          (fun (X : Type w') ↦ X)
            ((X ⋙ F.obj k).obj
              (⋯.choose (p := fun (j_1 : J) ↦
                ∃ (f : j ⟶ j_1),
                  Eq (α := (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ F.obj k).map f) :
                          (a : (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j)) →
                            (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
                        ((↑y₁ : (j_2 : K) → (F ⋙ (evaluation C (Type w')).obj (X.obj j)).obj j_2) k) :
                      (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ F.obj k).map f) :
                          (a : (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j)) →
                            (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1))
                        ((↑y₂ : (j_2 : K) → (F ⋙ (evaluation C (Type w')).obj (X.obj j)).obj j_2) k) :
                      (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j_1)))))))
hf :
  ∀ (k : K),
    Eq (α := (fun (X : Type w') ↦ X) ((F.obj k).obj (X.obj (j₁ k))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.obj k).map (X.map (f k))) :
            (a : (fun (X : Type w') ↦ X) ((F.obj k).obj (X.obj j))) →
              (fun (X : Type w') ↦ X) ((F.obj k).obj (X.obj (j₁ k))))
          ((↑y₁ : (j_1 : K) → (F ⋙ (evaluation C (Type w')).obj (X.obj j)).obj j_1) k) :
        (fun (X : Type w') ↦ X) ((F.obj k).obj (X.obj (j₁ k))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.obj k).map (X.map (f k))) :
            (a : (fun (X : Type w') ↦ X) ((F.obj k).obj (X.obj j))) →
              (fun (X : Type w') ↦ X) ((F.obj k).obj (X.obj (j₁ k))))
          ((↑y₂ : (j_1 : K) → (F ⋙ (evaluation C (Type w')).obj (X.obj j)).obj j_1) k) :
        (fun (X : Type w') ↦ X) ((F.obj k).obj (X.obj (j₁ k))))
hK' : HasCardinalLT K κ
ψ : (k : K) → j ⟶ IsCardinalFiltered.max j₁ hK' := fun (k : K) ↦ f k ≫ IsCardinalFiltered.toMax j₁ hK' k
a :
  ∀ (k : K),
    Eq.{w' + 1} (α := (F ⋙ obj (evaluation C (Type w')) (X.obj (IsCardinalFiltered.coeq ψ hK'))).obj k)
      ((↑((Types.isLimitEquivSections (hc (X.obj (IsCardinalFiltered.coeq ψ hK'))) :
                (a : (((evaluation C (Type w')).obj (X.obj (IsCardinalFiltered.coeq ψ hK'))).mapCone c).pt) →
                  (↑(F ⋙ (evaluation C (Type w')).obj (X.obj (IsCardinalFiltered.coeq ψ hK'))).sections :
                    Type (max w' u')))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (X.map (IsCardinalFiltered.toCoeq ψ hK'))) :
                  (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) →
                    (fun (X : Type w') ↦ X) (c.pt.obj (X.obj (IsCardinalFiltered.coeq ψ hK'))))
                x₁)) :
          (j_1 : K) → (F ⋙ (evaluation C (Type w')).obj (X.obj (IsCardinalFiltered.coeq ψ hK'))).obj j_1)
        k)
      ((↑((Types.isLimitEquivSections (hc (X.obj (IsCardinalFiltered.coeq ψ hK'))) :
                (a : (((evaluation C (Type w')).obj (X.obj (IsCardinalFiltered.coeq ψ hK'))).mapCone c).pt) →
                  (↑(F ⋙ (evaluation C (Type w')).obj (X.obj (IsCardinalFiltered.coeq ψ hK'))).sections :
                    Type (max w' u')))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (X.map (IsCardinalFiltered.toCoeq ψ hK'))) :
                  (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) →
                    (fun (X : Type w') ↦ X) (c.pt.obj (X.obj (IsCardinalFiltered.coeq ψ hK'))))
                x₂)) :
          (j_1 : K) → (F ⋙ (evaluation C (Type w')).obj (X.obj (IsCardinalFiltered.coeq ψ hK'))).obj j_1)
        k)
⊢ Eq (α := (↑(F ⋙ obj (evaluation C (Type w')) (X.obj (IsCardinalFiltered.coeq ψ hK'))).sections : Type (max w' u')))
    ((Types.isLimitEquivSections (hc (X.obj (IsCardinalFiltered.coeq ψ hK'))) :
          (a : (((evaluation C (Type w')).obj (X.obj (IsCardinalFiltered.coeq ψ hK'))).mapCone c).pt) →
            (↑(F ⋙ (evaluation C (Type w')).obj (X.obj (IsCardinalFiltered.coeq ψ hK'))).sections : Type (max w' u')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (X.map (IsCardinalFiltered.toCoeq ψ hK'))) :
            (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) →
              (fun (X : Type w') ↦ X) (c.pt.obj (X.obj (IsCardinalFiltered.coeq ψ hK'))))
          x₁) :
      (↑(F ⋙ obj (evaluation C (Type w')) (X.obj (IsCardinalFiltered.coeq ψ hK'))).sections : Type (max w' u')))
    ((Types.isLimitEquivSections (hc (X.obj (IsCardinalFiltered.coeq ψ hK'))) :
          (a : (((evaluation C (Type w')).obj (X.obj (IsCardinalFiltered.coeq ψ hK'))).mapCone c).pt) →
            (↑(F ⋙ (evaluation C (Type w')).obj (X.obj (IsCardinalFiltered.coeq ψ hK'))).sections : Type (max w' u')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (X.map (IsCardinalFiltered.toCoeq ψ hK'))) :
            (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) →
              (fun (X : Type w') ↦ X) (c.pt.obj (X.obj (IsCardinalFiltered.coeq ψ hK'))))
          x₂) :
      (↑(F ⋙ obj (evaluation C (Type w')) (X.obj (IsCardinalFiltered.coeq ψ hK'))).sections : Type (max w' u')))

Tactic:
ext k