-- Mathlib/CategoryTheory/Filtered/Basic.lean
theorem cocone_nonempty (F : J ⥤ C) : Nonempty (Cocone F)

Proof state:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X =>
    Finset.univ.biUnion fun Y => Finset.image (fun f => ⟨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}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f_1 ≫ f mY = f mX
⊢ Nonempty (Cocone F)

Tactic:
refine ⟨⟨Z, ⟨fun X => f (by simp [O]), ?_⟩⟩⟩

Result:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X =>
    Finset.univ.biUnion fun Y => Finset.image (fun f => ⟨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}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f_1 ≫ f mY = f mX
⊢ ∀ ⦃X Y : J⦄ (f_1 : X ⟶ Y), F.map f_1 ≫ (fun X => f ⋯) Y = (fun X => f ⋯) X ≫ ((Functor.const J).obj Z).map f_1

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
⊢ Nonempty (Cocone F)

Tactic:
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⟩

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X =>
    Finset.univ.biUnion fun Y => Finset.image (fun f => ⟨F.obj X, ⟨F.obj Y, ⟨⋯, ⟨⋯, F.map f⟩⟩⟩⟩) Finset.univ
⊢ Nonempty (Cocone F)

Proof state:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X =>
    Finset.univ.biUnion fun Y => Finset.image (fun f => ⟨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}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f_1 ≫ f mY = f mX
j j' : J
g : j ⟶ j'
⊢ F.map g ≫ f ⋯ = f ⋯ ≫ 𝟙 Z

Tactic:
simp only [Category.comp_id]

Result:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X =>
    Finset.univ.biUnion fun Y => Finset.image (fun f => ⟨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}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f_1 ≫ f mY = f mX
j j' : J
g : j ⟶ j'
⊢ F.map g ≫ f ⋯ = f ⋯

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
X Y : J
f : X ⟶ Y
⊢ F.obj X ∈ O

Tactic:
simp [O]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
X Y : J
f : X ⟶ Y
⊢ F.obj Y ∈ O

Tactic:
simp [O]

Result:
no goals

Proof state:
case intro.intro.a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X =>
    Finset.univ.biUnion fun Y => Finset.image (fun f => ⟨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}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f_1 ≫ f mY = f mX
j j' : J
g : j ⟶ j'
⊢ ⟨F.obj j, ⟨F.obj j', ⟨⋯, ⟨⋯, F.map g⟩⟩⟩⟩ ∈ H

Tactic:
simp only [O, H, Finset.mem_biUnion, Finset.mem_univ, Finset.mem_image, PSigma.mk.injEq,
  true_and, exists_and_left]

Result:
case intro.intro.a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X =>
    Finset.univ.biUnion fun Y => Finset.image (fun f => ⟨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}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f_1 ≫ f mY = f mX
j j' : J
g : j ⟶ j'
⊢ ∃ a, F.obj a = F.obj j ∧ ∃ x x_1, HEq ⟨F.obj x, ⟨⋯, ⟨⋯, F.map x_1⟩⟩⟩ ⟨F.obj j', ⟨⋯, ⟨⋯, F.map g⟩⟩⟩

Proof state:
case intro.intro.a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X =>
    Finset.univ.biUnion fun Y => Finset.image (fun f => ⟨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}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f_1 ≫ f mY = f mX
j j' : J
g : j ⟶ j'
⊢ ∃ a, F.obj a = F.obj j ∧ ∃ x x_1, HEq ⟨F.obj x, ⟨⋯, ⟨⋯, F.map x_1⟩⟩⟩ ⟨F.obj j', ⟨⋯, ⟨⋯, F.map g⟩⟩⟩

Tactic:
exact ⟨j, rfl, j', g, by simp⟩

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
⊢ 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⟩

Result:
no goals