-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
J : Type w
inst_2 : SmallCategory J
inst_3 : FinCategory J
F : Functor.{w, v, w, u} J C
let let₁ let₂ let₃ : Nonempty (Cocone F)
let₄ :
  let O := Finset.image F.obj Finset.univ;
  let H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
    Finset.biUnion Finset.univ fun (X : J) ↦
      Finset.biUnion Finset.univ fun (Y : J) ↦
        Finset.image
          (fun (f : X ⟶ Y) ↦
            PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) (F.obj X)
              (PSigma.mk (β := fun (Y : C) ↦ (_ : F.obj X ∈ O) ×' (_ : Y ∈ O) ×' (F.obj X ⟶ Y)) (F.obj Y)
                (PSigma.mk (β := fun (x : F.obj X ∈ O) ↦ (_ : F.obj Y ∈ O) ×' (F.obj X ⟶ F.obj Y)) ⋯
                  (PSigma.mk (β := fun (x : F.obj Y ∈ O) ↦ F.obj X ⟶ F.obj Y) ⋯ (F.map f)))))
          Finset.univ;
  ∀ (Z : C) (f : {X : C} → X ∈ O → (X ⟶ Z))
    (w :
      ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
        PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
              (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
                (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
                  (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f_1))) ∈
            H →
          f_1 ≫ f mY = f mX),
    Nonempty (Cocone F)
let₅ let₆ :
  let O := Finset.image F.obj Finset.univ;
  let H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
    Finset.biUnion Finset.univ fun (X : J) ↦
      Finset.biUnion Finset.univ fun (Y : J) ↦
        Finset.image
          (fun (f : X ⟶ Y) ↦
            PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) (F.obj X)
              (PSigma.mk (β := fun (Y : C) ↦ (_ : F.obj X ∈ O) ×' (_ : Y ∈ O) ×' (F.obj X ⟶ Y)) (F.obj Y)
                (PSigma.mk (β := fun (x : F.obj X ∈ O) ↦ (_ : F.obj Y ∈ O) ×' (F.obj X ⟶ F.obj Y)) ⋯
                  (PSigma.mk (β := fun (x : F.obj Y ∈ O) ↦ F.obj X ⟶ F.obj Y) ⋯ (F.map f)))))
          Finset.univ;
  ∀ (Z : C) (f : {X : C} → X ∈ O → (X ⟶ Z))
    (w :
      ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
        PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
              (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
                (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
                  (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f_1))) ∈
            H →
          f_1 ≫ f mY = f mX)
    ⦃j j' : J⦄ (g : j ⟶ j'),
    Eq (α := F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) Z) j')
      (F.map g ≫ (fun (X : J) ↦ (f ⋯ : F.obj X ⟶ Z)) j')
      ((fun (X : J) ↦ (f ⋯ : F.obj X ⟶ Z)) j ≫ Functor.map (Functor.obj (Functor.const J) Z) g)
let₇ :
  let O := Finset.image F.obj Finset.univ;
  let H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
    Finset.biUnion Finset.univ fun (X : J) ↦
      Finset.biUnion Finset.univ fun (Y : J) ↦
        Finset.image
          (fun (f : X ⟶ Y) ↦
            PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) (F.obj X)
              (PSigma.mk (β := fun (Y : C) ↦ (_ : F.obj X ∈ O) ×' (_ : Y ∈ O) ×' (F.obj X ⟶ Y)) (F.obj Y)
                (PSigma.mk (β := fun (x : F.obj X ∈ O) ↦ (_ : F.obj Y ∈ O) ×' (F.obj X ⟶ F.obj Y)) ⋯
                  (PSigma.mk (β := fun (x : F.obj Y ∈ O) ↦ F.obj X ⟶ F.obj Y) ⋯ (F.map f)))))
          Finset.univ;
  ∀ (Z : C) (f : {X : C} → X ∈ O → (X ⟶ Z))
    (w :
      ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
        PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
              (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
                (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
                  (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f_1))) ∈
            H →
          f_1 ≫ f mY = f mX)
    ⦃j j' : J⦄ (g : j ⟶ j'), F.map g ≫ f ⋯ = f ⋯ ≫ 𝟙 Z
let₈ :
  let O := Finset.image F.obj Finset.univ;
  let H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
    Finset.biUnion Finset.univ fun (X : J) ↦
      Finset.biUnion Finset.univ fun (Y : J) ↦
        Finset.image
          (fun (f : X ⟶ Y) ↦
            PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) (F.obj X)
              (PSigma.mk (β := fun (Y : C) ↦ (_ : F.obj X ∈ O) ×' (_ : Y ∈ O) ×' (F.obj X ⟶ Y)) (F.obj Y)
                (PSigma.mk (β := fun (x : F.obj X ∈ O) ↦ (_ : F.obj Y ∈ O) ×' (F.obj X ⟶ F.obj Y)) ⋯
                  (PSigma.mk (β := fun (x : F.obj Y ∈ O) ↦ F.obj X ⟶ F.obj Y) ⋯ (F.map f)))))
          Finset.univ;
  ∀ (Z : C) (f : {X : C} → X ∈ O → (X ⟶ Z))
    (w :
      ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
        PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
              (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
                (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
                  (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f_1))) ∈
            H →
          f_1 ≫ f mY = f mX)
    ⦃j j' : J⦄ (g : j ⟶ j'), F.map g ≫ f ⋯ = f ⋯
a :
  let O := Finset.image F.obj Finset.univ;
  let H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
    Finset.biUnion Finset.univ fun (X : J) ↦
      Finset.biUnion Finset.univ fun (Y : J) ↦
        Finset.image
          (fun (f : X ⟶ Y) ↦
            PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) (F.obj X)
              (PSigma.mk (β := fun (Y : C) ↦ (_ : F.obj X ∈ O) ×' (_ : Y ∈ O) ×' (F.obj X ⟶ Y)) (F.obj Y)
                (PSigma.mk (β := fun (x : F.obj X ∈ O) ↦ (_ : F.obj Y ∈ O) ×' (F.obj X ⟶ F.obj Y)) ⋯
                  (PSigma.mk (β := fun (x : F.obj Y ∈ O) ↦ F.obj X ⟶ F.obj Y) ⋯ (F.map f)))))
          Finset.univ;
  ∀ (Z : C) (f : {X : C} → X ∈ O → (X ⟶ Z))
    (w :
      ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
        PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
              (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
                (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
                  (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f_1))) ∈
            H →
          f_1 ≫ f mY = f mX)
    ⦃j j' : J⦄ (g : j ⟶ j'),
    PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) (F.obj j)
        (PSigma.mk (β := fun (Y : C) ↦ (_ : F.obj j ∈ O) ×' (_ : Y ∈ O) ×' (F.obj j ⟶ Y)) (F.obj j')
          (PSigma.mk (β := fun (x : F.obj j ∈ O) ↦ (_ : F.obj j' ∈ O) ×' (F.obj j ⟶ F.obj j')) ⋯
            (PSigma.mk (β := fun (x : F.obj j' ∈ O) ↦ F.obj j ⟶ F.obj j') ⋯ (F.map g)))) ∈
      H
a₁ :
  let O := Finset.image F.obj Finset.univ;
  let H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
    Finset.biUnion Finset.univ fun (X : J) ↦
      Finset.biUnion Finset.univ fun (Y : J) ↦
        Finset.image
          (fun (f : X ⟶ Y) ↦
            PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) (F.obj X)
              (PSigma.mk (β := fun (Y : C) ↦ (_ : F.obj X ∈ O) ×' (_ : Y ∈ O) ×' (F.obj X ⟶ Y)) (F.obj Y)
                (PSigma.mk (β := fun (x : F.obj X ∈ O) ↦ (_ : F.obj Y ∈ O) ×' (F.obj X ⟶ F.obj Y)) ⋯
                  (PSigma.mk (β := fun (x : F.obj Y ∈ O) ↦ F.obj X ⟶ F.obj Y) ⋯ (F.map f)))))
          Finset.univ;
  ∀ (Z : C) (f : {X : C} → X ∈ O → (X ⟶ Z))
    (w :
      ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
        PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
              (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
                (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
                  (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f_1))) ∈
            H →
          f_1 ≫ f mY = f mX)
    ⦃j j' : J⦄ (g : j ⟶ j'),
    ∃ (a : J),
      F.obj a = F.obj j ∧
        ∃ (x : J) (x_1 : a ⟶ x),
          HEq (α :=
            (Y : C) ×'
              (_ : F.obj a ∈ Finset.image F.obj Finset.univ) ×'
                (_ : Y ∈ Finset.image F.obj Finset.univ) ×' (F.obj a ⟶ Y))
            (PSigma.mk (β := fun (Y : C) ↦
              (_ : F.obj a ∈ Finset.image F.obj Finset.univ) ×'
                (_ : Y ∈ Finset.image F.obj Finset.univ) ×' (F.obj a ⟶ Y))
              (F.obj x)
              (PSigma.mk (β := fun (x_2 : F.obj a ∈ Finset.image F.obj Finset.univ) ↦
                (_ : F.obj x ∈ Finset.image F.obj Finset.univ) ×' (F.obj a ⟶ F.obj x)) ⋯
                (PSigma.mk (β := fun (x_2 : F.obj x ∈ Finset.image F.obj Finset.univ) ↦ F.obj a ⟶ F.obj x) ⋯
                  (F.map x_1))))
            (β :=
            (Y : C) ×'
              (_ : F.obj j ∈ Finset.image F.obj Finset.univ) ×'
                (_ : Y ∈ Finset.image F.obj Finset.univ) ×' (F.obj j ⟶ Y))
            (PSigma.mk (β := fun (Y : C) ↦
              (_ : F.obj j ∈ Finset.image F.obj Finset.univ) ×'
                (_ : Y ∈ Finset.image F.obj Finset.univ) ×' (F.obj j ⟶ Y))
              (F.obj j')
              (PSigma.mk (β := fun (x : F.obj j ∈ Finset.image F.obj Finset.univ) ↦
                (_ : F.obj j' ∈ Finset.image F.obj Finset.univ) ×' (F.obj j ⟶ F.obj j')) ⋯
                (PSigma.mk (β := fun (x : F.obj j' ∈ Finset.image F.obj Finset.univ) ↦ F.obj j ⟶ F.obj j') ⋯
                  (F.map g))))
⊢ Nonempty (Cocone F)

Tactic:
classical
  let O := Finset.univ.image F.obj
  let H : Finset (Σ' (X Y : C) (_ : X ∈ O) (_ : Y ∈ O), X ⟶ Y) :=
    Finset.univ.biUnion fun X : J => Finset.univ.biUnion fun Y : J =>
      Finset.univ.image fun f : X ⟶ Y => ⟨F.obj X, F.obj Y, by simp [O], by simp [O], F.map f⟩
  obtain ⟨Z, f, w⟩ := sup_exists O H
  refine ⟨⟨Z, ⟨fun X => f (by simp [O]), ?_⟩⟩⟩
  intro j j' g
  dsimp
  simp only [Category.comp_id]
  apply w
  simp only [O, H, Finset.mem_biUnion, Finset.mem_univ, Finset.mem_image, PSigma.mk.injEq,
    true_and, exists_and_left]
  exact ⟨j, rfl, j', g, by simp⟩

Premises used: Finset.mem_univ, Finset.mem_image, exists_and_left, CategoryTheory.Category.comp_id, PSigma.mk.injEq, Finset.mem_biUnion, true_and