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

Proof state:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered 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 → (Z ⟶ X)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f mX ≫ f_1 = f mY
⊢ Nonempty (Cone F)

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

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

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered 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 → (Z ⟶ X)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f mX ≫ f_1 = f mY
j j' : J
g : j ⟶ j'
⊢ HEq ⟨F.obj j', ⟨⋯, ⟨⋯, F.map g⟩⟩⟩ ⟨F.obj j', ⟨⋯, ⟨⋯, F.map g⟩⟩⟩

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered 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 → (Z ⟶ X)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f mX ≫ f_1 = f mY
X : J
⊢ F.obj X ∈ O

Tactic:
simp [O]

Result:
no goals

Proof state:
case intro.intro.a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered 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 → (Z ⟶ X)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f mX ≫ f_1 = f mY
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✝² : IsCofiltered 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 → (Z ⟶ X)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f mX ≫ f_1 = f mY
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
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered 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 → (Z ⟶ X)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f mX ≫ f_1 = f mY
j j' : J
g : j ⟶ j'
⊢ f ⋯ ≫ F.map g = f ⋯

Tactic:
apply w

Result:
case intro.intro.a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered 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 → (Z ⟶ X)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f mX ≫ f_1 = f mY
j j' : J
g : j ⟶ j'
⊢ ⟨F.obj j, ⟨F.obj j', ⟨⋯, ⟨⋯, F.map g⟩⟩⟩⟩ ∈ H

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
⊢ Nonempty (Cone 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⟩ := inf_exists O H
refine ⟨⟨Z, ⟨fun X => f (by simp [O]), ?_⟩⟩⟩
intro j j' g
dsimp
simp only [Category.id_comp]
symm
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

Proof state:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered 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 → (Z ⟶ X)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f mX ≫ f_1 = f mY
j j' : J
g : j ⟶ j'
⊢ 𝟙 Z ≫ f ⋯ = f ⋯ ≫ F.map g

Tactic:
simp only [Category.id_comp]

Result:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered 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 → (Z ⟶ X)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f mX ≫ f_1 = f mY
j j' : J
g : j ⟶ j'
⊢ f ⋯ = f ⋯ ≫ F.map g