-- Mathlib/Topology/Category/TopCat/Limits/Konig.lean
theorem nonempty_limitCone_of_compact_t2_cofiltered_system (F : J ⥤ TopCat.{max v u})
    [IsCofilteredOrEmpty J]
    [∀ j : J, Nonempty (F.obj j)] [∀ j : J, CompactSpace (F.obj j)] [∀ j : J, T2Space (F.obj j)] :
    Nonempty (TopCat.limitCone F).pt

Proof state:
J : Type u
inst✝⁴ : SmallCategory J
F : J ⥤ TopCat
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
⊢ Nonempty ↑(limitCone F).pt

Tactic:
obtain ⟨u, hu⟩ :=
  IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed (fun G => partialSections F _)
    (partialSections.directed F) (fun G => partialSections.nonempty F _)
    (fun G => IsClosed.isCompact (partialSections.closed F _)) fun G =>
    partialSections.closed F _

Result:
case intro
J : Type u
inst✝⁴ : SmallCategory J
F : J ⥤ TopCat
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ i, partialSections F i.snd
⊢ Nonempty ↑(limitCone F).pt

Proof state:
J : Type u
inst✝⁴ : SmallCategory J
F : J ⥤ TopCat
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
⊢ Nonempty ↑(limitCone F).pt

Tactic:
classical
obtain ⟨u, hu⟩ :=
  IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed (fun G => partialSections F _)
    (partialSections.directed F) (fun G => partialSections.nonempty F _)
    (fun G => IsClosed.isCompact (partialSections.closed F _)) fun G =>
    partialSections.closed F _
use u
intro X Y f
let G : FiniteDiagram J :=
  ⟨{X, Y},
    {⟨X, Y, by simp only [true_or, eq_self_iff_true, Finset.mem_insert], by
        simp only [eq_self_iff_true, or_true, Finset.mem_insert, Finset.mem_singleton], f⟩}⟩
exact hu _ ⟨G, rfl⟩ (Finset.mem_singleton_self _)

Result:
no goals

Proof state:
case intro
J : Type u
inst✝⁴ : SmallCategory J
F : J ⥤ TopCat
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ i, partialSections F i.snd
⊢ Nonempty ↑(limitCone F).pt

Tactic:
use u

Result:
case property
J : Type u
inst✝⁴ : SmallCategory J
F : J ⥤ TopCat
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ i, partialSections F i.snd
⊢ u ∈ {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j}

Proof state:
J : Type u
inst✝⁴ : SmallCategory J
F : J ⥤ TopCat
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ i, partialSections F i.snd
X Y : J
f : X ⟶ Y
⊢ Y ∈ {X, Y}

Tactic:
simp only [eq_self_iff_true, or_true, Finset.mem_insert, Finset.mem_singleton]

Result:
no goals

Proof state:
case property
J : Type u
inst✝⁴ : SmallCategory J
F : J ⥤ TopCat
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ i, partialSections F i.snd
X Y : J
f : X ⟶ Y
G : TopCat.FiniteDiagram J := ⟨{X, Y}, {⟨X, ⟨Y, ⟨⋯, ⟨⋯, f⟩⟩⟩⟩}⟩
⊢ (ConcreteCategory.hom (F.map f)) (u X) = u Y

Tactic:
exact hu _ ⟨G, rfl⟩ (Finset.mem_singleton_self _)

Result:
no goals

Proof state:
J : Type u
inst✝⁴ : SmallCategory J
F : J ⥤ TopCat
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ i, partialSections F i.snd
X Y : J
f : X ⟶ Y
⊢ X ∈ {X, Y}

Tactic:
simp only [true_or, eq_self_iff_true, Finset.mem_insert]

Result:
no goals

Proof state:
case property
J : Type u
inst✝⁴ : SmallCategory J
F : J ⥤ TopCat
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ i, partialSections F i.snd
X Y : J
f : X ⟶ Y
⊢ (ConcreteCategory.hom (F.map f)) (u X) = u Y

Tactic:
let G : FiniteDiagram J :=
  ⟨{X, Y},
    {⟨X, Y, by simp only [true_or, eq_self_iff_true, Finset.mem_insert], by
        simp only [eq_self_iff_true, or_true, Finset.mem_insert, Finset.mem_singleton], f⟩}⟩

Result:
case property
J : Type u
inst✝⁴ : SmallCategory J
F : J ⥤ TopCat
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ i, partialSections F i.snd
X Y : J
f : X ⟶ Y
G : TopCat.FiniteDiagram J := ⟨{X, Y}, {⟨X, ⟨Y, ⟨⋯, ⟨⋯, f⟩⟩⟩⟩}⟩
⊢ (ConcreteCategory.hom (F.map f)) (u X) = u Y

Proof state:
case property
J : Type u
inst✝⁴ : SmallCategory J
F : J ⥤ TopCat
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ i, partialSections F i.snd
⊢ u ∈ {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j}

Tactic:
intro X Y f

Result:
case property
J : Type u
inst✝⁴ : SmallCategory J
F : J ⥤ TopCat
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ i, partialSections F i.snd
X Y : J
f : X ⟶ Y
⊢ (ConcreteCategory.hom (F.map f)) (u X) = u Y