-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
    {ι : Type v} [hι : Nonempty ι] (t : ι → Set X) (htd : Directed (· ⊇ ·) t)
    (htn : ∀ i, (t i).Nonempty) (htc : ∀ i, IsCompact (t i)) (htcl : ∀ i, IsClosed (t i)) :
    (⋂ i, t i).Nonempty

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 => x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), (t i).Nonempty
i j : ι
hji₀ : t i₀ ⊇ t j
hji : t i ⊇ t j
⊢ (t i₀ ∩ t i).Nonempty

Tactic:
exact (htn j).mono (subset_inter hji₀ hji)

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 => x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), t i ≠ ∅
⊢ t i₀ ∩ ⋂ i, t i ≠ ∅

Tactic:
apply mt ((htc i₀).elim_directed_family_closed t htcl)

Result:
X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 => x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), t i ≠ ∅
⊢ ¬(Directed (fun x1 x2 => x1 ⊇ x2) t → ∃ i, t i₀ ∩ t i = ∅)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 => x1 ⊇ x2) t
htn : ∀ (i : ι), (t i).Nonempty
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed (t i)
⊢ (⋂ i, t i).Nonempty

Tactic:
let i₀ := hι.some

Result:
X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 => x1 ⊇ x2) t
htn : ∀ (i : ι), (t i).Nonempty
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed (t i)
i₀ : ι := hι.some
⊢ (⋂ i, t i).Nonempty

Proof state:
X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 => x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), t i ≠ ∅
⊢ Directed (fun x1 x2 => x1 ⊇ x2) t ∧ ∀ (i : ι), (t i₀ ∩ t i).Nonempty

Tactic:
simp only [← nonempty_iff_ne_empty] at htn ⊢

Result:
X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 => x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), (t i).Nonempty
⊢ Directed (fun x1 x2 => x1 ⊇ x2) t ∧ ∀ (i : ι), (t i₀ ∩ t i).Nonempty

Proof state:
X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 => x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), (t i).Nonempty
⊢ Directed (fun x1 x2 => x1 ⊇ x2) t ∧ ∀ (i : ι), (t i₀ ∩ t i).Nonempty

Tactic:
refine ⟨htd, fun i => ?_⟩

Result:
X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 => x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), (t i).Nonempty
i : ι
⊢ (t i₀ ∩ t i).Nonempty

Proof state:
X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 => x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), (t i).Nonempty
i : ι
⊢ (t i₀ ∩ t i).Nonempty

Tactic:
rcases htd i₀ i with ⟨j, hji₀, hji⟩

Result:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 => x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), (t i).Nonempty
i j : ι
hji₀ : t i₀ ⊇ t j
hji : t i ⊇ t j
⊢ (t i₀ ∩ t i).Nonempty

Proof state:
X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 => x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), t i ≠ ∅
⊢ ¬(Directed (fun x1 x2 => x1 ⊇ x2) t → ∃ i, t i₀ ∩ t i = ∅)

Tactic:
push_neg

Result:
X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 => x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), t i ≠ ∅
⊢ Directed (fun x1 x2 => x1 ⊇ x2) t ∧ ∀ (i : ι), (t i₀ ∩ t i).Nonempty

Proof state:
X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 => x1 ⊇ x2) t
htn : ∀ (i : ι), (t i).Nonempty
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed (t i)
i₀ : ι := hι.some
⊢ (t i₀ ∩ ⋂ i, t i).Nonempty

Tactic:
simp only [nonempty_iff_ne_empty] at htn ⊢

Result:
X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 => x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), t i ≠ ∅
⊢ t i₀ ∩ ⋂ i, t i ≠ ∅

Proof state:
X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 => x1 ⊇ x2) t
htn : ∀ (i : ι), (t i).Nonempty
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed (t i)
i₀ : ι := hι.some
⊢ (⋂ i, t i).Nonempty

Tactic:
suffices (t i₀ ∩ ⋂ i, t i).Nonempty by
  rwa [inter_eq_right.mpr (iInter_subset _ i₀)] at this

Result:
X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 => x1 ⊇ x2) t
htn : ∀ (i : ι), (t i).Nonempty
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed (t i)
i₀ : ι := hι.some
⊢ (t i₀ ∩ ⋂ i, t i).Nonempty

Proof state:
X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 => x1 ⊇ x2) t
htn : ∀ (i : ι), (t i).Nonempty
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed (t i)
i₀ : ι := hι.some
this : (t i₀ ∩ ⋂ i, t i).Nonempty
⊢ (⋂ i, t i).Nonempty

Tactic:
rwa [inter_eq_right.mpr (iInter_subset _ i₀)] at this

Result:
no goals