-- 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)
x : c.pt.obj cX.pt
this : IsFiltered J
y : (↑(F ⋙ obj (evaluation C (Type w')) cX.pt).sections : Type (max w' u'))
hy :
  (Equiv.symm (Types.isLimitEquivSections (hc cX.pt)) :
        (a : (↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections : Type (max w' u'))) →
          (((evaluation C (Type w')).obj cX.pt).mapCone c).pt)
      y =
    x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz :
  ∀ (k : K),
    (↑y : (j : K) → (F ⋙ (evaluation C (Type w')).obj cX.pt).obj j) k =
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((F.obj k).map (cX.ι.app j₀)) :
          (a : (fun (X : Type w') ↦ X) ((F.obj k).obj (X.obj j₀))) →
            (fun (X : Type w') ↦ X) ((F.obj k).obj (((const J).obj cX.pt).obj j₀)))
        (z k)
H :
  ∀ {k k' : K} (φ : k ⟶ k'),
    ∃ (j : J) (f : j₀ ⟶ j),
      Eq (α := (fun (X : Type w') ↦ X) ((X ⋙ F.obj k').obj j))
        ((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))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.map φ).app (X.obj j₀)) :
                  (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₀)))
                (z k) :
              (fun (X : Type w') ↦ X) ((F.obj k').obj (X.obj j₀))) :
          (fun (X : Type w') ↦ X) ((X ⋙ F.obj k').obj j))
        ((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))
            (z k') :
          (fun (X : Type w') ↦ X) ((X ⋙ F.obj k').obj j))
j : {k k' : K} → (φ : k ⟶ k') → J :=
  fun {k k' : K} (φ : k ⟶ k') ↦
    ⋯.choose (p := fun (j : J) ↦
      ∃ (f : j₀ ⟶ j),
        Eq (α := (fun (X : Type w') ↦ X) ((X ⋙ F.obj k').obj j))
          ((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))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.map φ).app (X.obj j₀)) :
                    (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₀)))
                  (z k) :
                (fun (X : Type w') ↦ X) ((F.obj k').obj (X.obj j₀))) :
            (fun (X : Type w') ↦ X) ((X ⋙ F.obj k').obj j))
          ((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))
              (z k') :
            (fun (X : Type w') ↦ X) ((X ⋙ F.obj k').obj j)))
g : {k k' : K} → (φ : k ⟶ k') → j₀ ⟶ j φ :=
  fun {k k' : K} (φ : k ⟶ k') ↦
    ⋯.choose (p :=
      fun
        (f :
          j₀ ⟶
            ⋯.choose (p := fun (j : J) ↦
              ∃ (f : j₀ ⟶ j),
                Eq (α := (fun (X : Type w') ↦ X) ((X ⋙ F.obj k').obj j))
                  ((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))
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.map φ).app (X.obj j₀)) :
                            (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₀)))
                          (z k) :
                        (fun (X : Type w') ↦ X) ((F.obj k').obj (X.obj j₀))) :
                    (fun (X : Type w') ↦ X) ((X ⋙ F.obj k').obj j))
                  ((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))
                      (z k') :
                    (fun (X : Type w') ↦ X) ((X ⋙ F.obj k').obj j)))) ↦
      Eq (α :=
        (fun (X : Type w') ↦ X)
          ((X ⋙ F.obj k').obj
            (⋯.choose (p := fun (j : J) ↦
              ∃ (f : j₀ ⟶ j),
                Eq (α := (fun (X : Type w') ↦ X) ((X ⋙ F.obj k').obj j))
                  ((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))
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.map φ).app (X.obj j₀)) :
                            (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₀)))
                          (z k) :
                        (fun (X : Type w') ↦ X) ((F.obj k').obj (X.obj j₀))) :
                    (fun (X : Type w') ↦ X) ((X ⋙ F.obj k').obj j))
                  ((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))
                      (z k') :
                    (fun (X : Type w') ↦ X) ((X ⋙ F.obj k').obj j))))))
        ((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))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.map φ).app (X.obj j₀)) :
                  (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₀)))
                (z k) :
              (fun (X : Type w') ↦ X) ((F.obj k').obj (X.obj j₀))) :
          (fun (X : Type w') ↦ X)
            ((X ⋙ F.obj k').obj
              (⋯.choose (p := fun (j : J) ↦
                ∃ (f : j₀ ⟶ j),
                  Eq (α := (fun (X : Type w') ↦ X) ((X ⋙ F.obj k').obj j))
                    ((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))
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.map φ).app (X.obj j₀)) :
                              (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₀)))
                            (z k) :
                          (fun (X : Type w') ↦ X) ((F.obj k').obj (X.obj j₀))) :
                      (fun (X : Type w') ↦ X) ((X ⋙ F.obj k').obj j))
                    ((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))
                        (z k') :
                      (fun (X : Type w') ↦ X) ((X ⋙ F.obj k').obj j))))))
        ((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))
            (z k') :
          (fun (X : Type w') ↦ X)
            ((X ⋙ F.obj k').obj
              (⋯.choose (p := fun (j : J) ↦
                ∃ (f : j₀ ⟶ j),
                  Eq (α := (fun (X : Type w') ↦ X) ((X ⋙ F.obj k').obj j))
                    ((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))
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.map φ).app (X.obj j₀)) :
                              (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₀)))
                            (z k) :
                          (fun (X : Type w') ↦ X) ((F.obj k').obj (X.obj j₀))) :
                      (fun (X : Type w') ↦ X) ((X ⋙ F.obj k').obj j))
                    ((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))
                        (z k') :
                      (fun (X : Type w') ↦ X) ((X ⋙ F.obj k').obj j)))))))
hg :
  ∀ {k k' : K} (φ : k ⟶ k'),
    Eq (α := (fun (X : Type w') ↦ X) ((F.obj k').obj (X.obj (j φ))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.obj k').map (X.map (g φ))) :
            (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 φ))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.map φ).app (X.obj j₀)) :
                (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₀)))
              (z k) :
            (fun (X : Type w') ↦ X) ((F.obj k').obj (X.obj j₀))) :
        (fun (X : Type w') ↦ X) ((F.obj k').obj (X.obj (j φ))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.obj k').map (X.map (g φ))) :
            (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 φ))))
          (z k') :
        (fun (X : Type w') ↦ X) ((F.obj k').obj (X.obj (j φ))))
j'' : (f : Arrow.{v', u'} K) → J := fun (f : Arrow.{v', u'} K) ↦ j f.hom
ψ : (f : Arrow.{v', u'} K) → j₀ ⟶ IsCardinalFiltered.max j'' hK :=
  fun (f : Arrow.{v', u'} K) ↦ g f.hom ≫ IsCardinalFiltered.toMax j'' hK f
k k' : K
φ : k ⟶ k'
⊢ Eq (α := j₀ ⟶ IsCardinalFiltered.coeq ψ hK) (IsCardinalFiltered.toCoeq ψ hK)
    (g φ ≫
      (fun (k k' : K) (φ : k ⟶ k') ↦
          (IsCardinalFiltered.toMax j'' hK (Arrow.mk φ) ≫ IsCardinalFiltered.coeqHom ψ hK :
            j φ ⟶ IsCardinalFiltered.coeq ψ hK))
        k k' φ)

Tactic:
simpa [ψ] using (IsCardinalFiltered.coeq_condition ψ hK (Arrow.mk φ)).symm

Premises used: CategoryTheory.Arrow.mk, Eq.symm, CategoryTheory.IsCardinalFiltered.coeq_condition