awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝[s] x
V : (x : X) → Set X
V_nhds : ∀ (x : X) (hx : x ∈ s), V x ∈ 𝓝 x
hV : ∀ (x : X) (hx : x ∈ s), V x ∩ s ⊆ U x
refine :
  ∀ (t : Finset X),
    (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, V x → ∀ (t_sub_s : ∀ x ∈ t, x ∈ s) (ht : s ⊆ ⋃ x ∈ t, V x), s ⊆ ⋃ i ∈ t, V i ∩ s
⊢ ∃ (t : Finset X), (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x

Tactic:
refine (hs.elim_nhds_subcover V V_nhds).imp fun t ⟨t_sub_s, ht⟩ =>
    ⟨t_sub_s, subset_trans ?_ (iUnion₂_mono fun x hx => hV x (t_sub_s x hx))⟩

Premises used: Exists.imp, IsCompact.elim_nhds_subcover
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝[s] x
V : (x : X) → Set X
V_nhds : ∀ (x : X) (hx : x ∈ s), V x ∈ 𝓝 x
hV : ∀ (x : X) (hx : x ∈ s), V x ∩ s ⊆ U x
t : Finset X
h : (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, V x
t_sub_s : ∀ x ∈ t, x ∈ s
ht : s ⊆ ⋃ x ∈ t, V x
⊢ s ⊆ ⋃ i ∈ t, V i ∩ s

Tactic:
simpa [← iUnion_inter]

Premises used: Set.iUnion_inter
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
⊢ Disjoint (𝓝ˢ s) l ↔ ∀ x ∈ s, Disjoint (𝓝 x) l

Tactic:
⟨fun h x hx => h.mono_left <| nhds_le_nhdsSet hx, fun H => ?_⟩

Premises used: nhds_le_nhdsSet, Disjoint.mono_left, Iff.intro
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
refine : ∀ (H : ∀ x ∈ s, Disjoint (𝓝 x) l), Disjoint (𝓝ˢ s) l
⊢ Disjoint (𝓝ˢ s) l ↔ ∀ x ∈ s, Disjoint (𝓝 x) l

Tactic:
refine ⟨fun h x hx => h.mono_left <| nhds_le_nhdsSet hx, fun H => ?_⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
choose! :
  ∀ (U : (x : X) → Set X) (hxU : ∀ (x : X) (hx : x ∈ s), x ∈ U x ∧ IsOpen[inst] (U x))
    (hUl : ∀ (x : X) (hx : x ∈ s), (U x)ᶜ ∈ l), Disjoint (𝓝ˢ s) l
⊢ Disjoint (𝓝ˢ s) l

Tactic:
choose! U hxU hUl using fun x hx => (nhds_basis_opens x).disjoint_iff_left.1 (H x hx)

Premises used: Filter.HasBasis.disjoint_iff_left, Iff.mp, nhds_basis_opens
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : (x : X) → Set X
hxU : ∀ (x : X) (hx : x ∈ s), x ∈ U x ∧ IsOpen[inst] (U x)
hUl : ∀ (x : X) (hx : x ∈ s), (U x)ᶜ ∈ l
⊢ ∀ (x : X) (hx : x ∈ s), x ∈ U x

Tactic:
choose hxU hUo using hxU
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : (x : X) → Set X
hxU : ∀ (x : X) (hx : x ∈ s), x ∈ U x ∧ IsOpen[inst] (U x)
hUl : ∀ (x : X) (hx : x ∈ s), (U x)ᶜ ∈ l
hxU₁ : ∀ (x : X) (hx : x ∈ s), x ∈ U x
⊢ ∀ (x : X) (hx : x ∈ s), IsOpen[inst] (U x)

Tactic:
choose hxU hUo using hxU
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : (x : X) → Set X
hUl : ∀ (x : X) (hx : x ∈ s), (U x)ᶜ ∈ l
hxU : ∀ (x : X) (hx : x ∈ s), x ∈ U x
hUo : ∀ (x : X) (hx : x ∈ s), IsOpen[inst] (U x)
rcases : ∀ (t : Finset X) (hts : ∀ x ∈ t, x ∈ s) (hst : s ⊆ ⋃ x ∈ t, U x), Disjoint (𝓝ˢ s) l
⊢ Disjoint (𝓝ˢ s) l

Tactic:
rcases hs.elim_nhds_subcover U fun x hx => (hUo x hx).mem_nhds (hxU x hx) with ⟨t, hts, hst⟩

Premises used: IsCompact.elim_nhds_subcover, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : (x : X) → Set X
hUl : ∀ (x : X) (hx : x ∈ s), (U x)ᶜ ∈ l
hxU : ∀ (x : X) (hx : x ∈ s), x ∈ U x
hUo : ∀ (x : X) (hx : x ∈ s), IsOpen[inst] (U x)
t : Finset X
hts : ∀ x ∈ t, x ∈ s
hst : s ⊆ ⋃ x ∈ t, U x
⊢ Disjoint (𝓝ˢ s) l

Tactic:
(hasBasis_nhdsSet _).disjoint_iff_left.2
    ⟨⋃ x ∈ t, U x, ⟨isOpen_biUnion fun x hx => hUo x (hts x hx), hst⟩, ?_⟩

Premises used: Iff.mpr, hasBasis_nhdsSet, Filter.HasBasis.disjoint_iff_left, And.intro, Exists.intro, isOpen_biUnion, Set.iUnion
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : (x : X) → Set X
hUl : ∀ (x : X) (hx : x ∈ s), (U x)ᶜ ∈ l
hxU : ∀ (x : X) (hx : x ∈ s), x ∈ U x
hUo : ∀ (x : X) (hx : x ∈ s), IsOpen[inst] (U x)
t : Finset X
hts : ∀ x ∈ t, x ∈ s
hst : s ⊆ ⋃ x ∈ t, U x
refine : (⋃ x ∈ t, U x)ᶜ ∈ l
⊢ Disjoint (𝓝ˢ s) l

Tactic:
refine (hasBasis_nhdsSet _).disjoint_iff_left.2
    ⟨⋃ x ∈ t, U x, ⟨isOpen_biUnion fun x hx => hUo x (hts x hx), hst⟩, ?_⟩

Premises used: Iff.mpr, hasBasis_nhdsSet, Filter.HasBasis.disjoint_iff_left, And.intro, Exists.intro, isOpen_biUnion, Set.iUnion
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : (x : X) → Set X
hUl : ∀ (x : X) (hx : x ∈ s), (U x)ᶜ ∈ l
hxU : ∀ (x : X) (hx : x ∈ s), x ∈ U x
hUo : ∀ (x : X) (hx : x ∈ s), IsOpen[inst] (U x)
t : Finset X
hts : ∀ x ∈ t, x ∈ s
hst : s ⊆ ⋃ x ∈ t, U x
rw : ∀ i ∈ t, (U i)ᶜ ∈ l
⊢ (⋃ x ∈ t, U x)ᶜ ∈ l

Tactic:
rw [compl_iUnion₂, biInter_finset_mem]

Premises used: Set.compl_iUnion₂, Filter.biInter_finset_mem
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : (x : X) → Set X
hUl : ∀ (x : X) (hx : x ∈ s), (U x)ᶜ ∈ l
hxU : ∀ (x : X) (hx : x ∈ s), x ∈ U x
hUo : ∀ (x : X) (hx : x ∈ s), IsOpen[inst] (U x)
t : Finset X
hts : ∀ x ∈ t, x ∈ s
hst : s ⊆ ⋃ x ∈ t, U x
⊢ ∀ i ∈ t, (U i)ᶜ ∈ l

Tactic:
fun x hx => hUl x (hts x hx)
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : (x : X) → Set X
hUl : ∀ (x : X) (hx : x ∈ s), (U x)ᶜ ∈ l
hxU : ∀ (x : X) (hx : x ∈ s), x ∈ U x
hUo : ∀ (x : X) (hx : x ∈ s), IsOpen[inst] (U x)
t : Finset X
hts : ∀ x ∈ t, x ∈ s
hst : s ⊆ ⋃ x ∈ t, U x
⊢ ∀ i ∈ t, (U i)ᶜ ∈ l

Tactic:
exact fun x hx => hUl x (hts x hx)
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
⊢ Disjoint l (𝓝ˢ s) ↔ ∀ x ∈ s, Disjoint l (𝓝 x)

Tactic:
simpa only [disjoint_comm] using hs.disjoint_nhdsSet_left

Premises used: disjoint_comm, IsCompact.disjoint_nhdsSet_left
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
inst_1 : Nonempty ι
hs : IsCompact s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : s ∩ ⋂ (i : ι), t i = ∅
hdt : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t
⊢ s ⊆ ⋃ (i : ι), (compl ∘ t) i

Tactic:
simpa only [subset_def, not_forall, eq_empty_iff_forall_notMem, mem_iUnion, exists_prop,
          mem_inter_iff, not_and, mem_iInter, mem_compl_iff] using hst

Premises used: Set.subset_def, Set.mem_inter_iff, Set.mem_iUnion, exists_prop, Set.mem_iInter, Set.eq_empty_iff_forall_notMem, not_and, Classical.not_forall, Set.mem_compl_iff
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
inst_1 : Nonempty ι
hs : IsCompact s
t_1 : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t_1 i)
hst : s ∩ ⋂ (i : ι), t_1 i = ∅
hdt : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t_1
t : ι
ht : s ⊆ (compl ∘ t_1) t
⊢ s ∩ t_1 t = ∅

Tactic:
simpa only [subset_def, not_forall, eq_empty_iff_forall_notMem, mem_iUnion, exists_prop,
      mem_inter_iff, not_and, mem_iInter, mem_compl_iff] using ht

Premises used: Set.subset_def, Set.mem_inter_iff, Set.mem_iUnion, exists_prop, Set.mem_iInter, Set.eq_empty_iff_forall_notMem, not_and, Classical.not_forall, Set.mem_compl_iff
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsCompact s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst rwa rwa₁ rwa₂ rwa₃ : s ∩ ⋂ (i : ι), t i = ∅
⊢ s ∩ ⋂ (i : Finset ι), ⋂ i_1 ∈ i, t i_1 = ∅

Tactic:
rwa [← iInter_eq_iInter_finset]

Premises used: Set.iInter_eq_iInter_finset
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsCompact s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : ∀ (u : Finset ι), (s ∩ ⋂ i ∈ u, t i).Nonempty
contrapose! : ∀ (hst : s ∩ ⋂ (i : ι), t i = ∅), ∃ (u : Finset ι), s ∩ ⋂ i ∈ u, t i = ∅
⊢ (s ∩ ⋂ (i : ι), t i).Nonempty

Tactic:
contrapose! hst
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsCompact s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : s ∩ ⋂ (i : ι), t i = ∅
⊢ ∃ (u : Finset ι), s ∩ ⋂ i ∈ u, t i = ∅

Tactic:
hs.elim_finite_subfamily_closed t htc hst

Premises used: IsCompact.elim_finite_subfamily_closed
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsCompact s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : s ∩ ⋂ (i : ι), t i = ∅
⊢ ∃ (u : Finset ι), s ∩ ⋂ i ∈ u, t i = ∅

Tactic:
exact hs.elim_finite_subfamily_closed t htc hst

Premises used: IsCompact.elim_finite_subfamily_closed
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
t : Set (Set X)
ht : ∀ a ∈ t, IsClosed[inst] a
h : ∀ a ⊆ t, a.Finite → (s ∩ ⋂₀ a).Nonempty
rw : (s ∩ ⋂ (i : (↑t : Type u)), (↑i : Set X)).Nonempty
⊢ (s ∩ ⋂₀ t).Nonempty

Tactic:
rw [Set.sInter_eq_iInter]

Premises used: Set.sInter_eq_iInter
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
t : Set (Set X)
ht : ∀ a ∈ t, IsClosed[inst] a
h : ∀ a ⊆ t, a.Finite → (s ∩ ⋂₀ a).Nonempty
⊢ (s ∩ ⋂ (i : (↑t : Type u)), (↑i : Set X)).Nonempty

Tactic:
hs.inter_iInter_nonempty _ (fun i ↦ ht _ i.2) fun a ↦ ?_

Premises used: IsCompact.inter_iInter_nonempty, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
t : Set (Set X)
ht : ∀ a ∈ t, IsClosed[inst] a
h : ∀ a ⊆ t, a.Finite → (s ∩ ⋂₀ a).Nonempty
refine : ∀ (a : Finset (↑t : Type u)), (s ∩ ⋂ i ∈ a, (↑i : Set X)).Nonempty
⊢ (s ∩ ⋂ (i : (↑t : Type u)), (↑i : Set X)).Nonempty

Tactic:
refine hs.inter_iInter_nonempty _ (fun i ↦ ht _ i.2) fun a ↦ ?_

Premises used: IsCompact.inter_iInter_nonempty
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
t : Set (Set X)
ht : ∀ a ∈ t, IsClosed[inst] a
h : ∀ a ⊆ t, a.Finite → (s ∩ ⋂₀ a).Nonempty
a : Finset (↑t : Type u)
⊢ Subtype.val (p := fun (x : Set X) ↦ x ∈ t) '' (↑a : Set (↑t : Type u)) ⊆ t

Tactic:
simp
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
t : Set (Set X)
ht : ∀ a ∈ t, IsClosed[inst] a
h : ∀ a ⊆ t, a.Finite → (s ∩ ⋂₀ a).Nonempty
a : Finset (↑t : Type u)
⊢ (s ∩ ⋂ i ∈ a, (↑i : Set X)).Nonempty

Tactic:
simpa using h (Subtype.val '' (a : Set t)) (by simp) (a.finite_toSet.image _)

Premises used: Set.Finite.image, SetLike.coe, Set.image, Finset.finite_toSet, Subtype.val
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
s : Set (Set X)
hsc : ∀ t ∈ s, IsClosed[inst] t
hs : ∀ t ⊆ s, t.Finite → (⋂₀ t).Nonempty
⊢ ∀ a ⊆ s, a.Finite → (univ ∩ ⋂₀ a).Nonempty

Tactic:
simpa using hs
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
s : Set (Set X)
hsc : ∀ t ∈ s, IsClosed[inst] t
hs : ∀ t ⊆ s, t.Finite → (⋂₀ t).Nonempty
⊢ (⋂₀ s).Nonempty

Tactic:
simpa using isCompact_univ.nonempty_inter_sInter hsc (by simpa using hs)

Premises used: CompactSpace.isCompact_univ, IsCompact.nonempty_inter_sInter
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t
htn : ∀ (i : ι), (t i).Nonempty
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst] (t i)
i₀ : ι := hι.some
this : (t i₀ ∩ ⋂ (i : ι), t i).Nonempty
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : Set.Nonempty.{u} (α := X) (⋂ (i : ι), t i)), Set.Nonempty.{u} (α := X) (⋂ (i : ι), t i)
⊢ Set.Nonempty.{u} (α := X) (⋂ (i : ι), t i)

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

Premises used: Iff.mpr, Set.inter_eq_right, Set.iInter_subset
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t
htn : ∀ (i : ι), (t i).Nonempty
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst] (t i)
i₀ : ι := hι.some
suffices : (t i₀ ∩ ⋂ (i : ι), t i).Nonempty
⊢ Set.Nonempty.{u} (α := X) (⋂ (i : ι), t i)

Tactic:
suffices (t i₀ ∩ ⋂ i, t i).Nonempty by
    rwa [inter_eq_right.mpr (iInter_subset _ i₀)] at this
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t
htn : ∀ (i : ι), (t i).Nonempty
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst] (t i)
i₀ : ι := hι.some
simp : ∀ (htn : ∀ (i : ι), t i ≠ ∅), t i₀ ∩ ⋂ (i : ι), t i ≠ ∅
⊢ (t i₀ ∩ ⋂ (i : ι), t i).Nonempty

Tactic:
simp only [nonempty_iff_ne_empty] at htn ⊢

Premises used: Set.nonempty_iff_ne_empty
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst] (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), t i ≠ ∅
apply : ¬∀ (hdt : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t), ∃ (i : ι), t i₀ ∩ t i = ∅
⊢ t i₀ ∩ ⋂ (i : ι), t i ≠ ∅

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

Premises used: mt, IsCompact.elim_directed_family_closed
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst] (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), t i ≠ ∅
push : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t ∧ ∀ (i : ι), (t i₀ ∩ t i).Nonempty
⊢ ¬∀ (hdt : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t), ∃ (i : ι), t i₀ ∩ t i = ∅

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst] (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), t i ≠ ∅
⊢ ∀ (i : ι), (t i).Nonempty

Tactic:
simp only [← nonempty_iff_ne_empty] at htn ⊢

Premises used: Set.nonempty_iff_ne_empty
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst] (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), (t i).Nonempty
⊢ Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t ∧ ∀ (i : ι), (t i₀ ∩ t i).Nonempty

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

Premises used: And.intro
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst] (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), (t i).Nonempty
refine : ∀ (i : ι), (t i₀ ∩ t i).Nonempty
⊢ Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t ∧ ∀ (i : ι), (t i₀ ∩ t i).Nonempty

Tactic:
refine ⟨htd, fun i => ?_⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst] (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), (t i).Nonempty
i : ι
rcases : ∀ (j : ι) (hji₀ : t i₀ ⊇ t j) (hji : t i ⊇ t j), (t i₀ ∩ t i).Nonempty
⊢ (t i₀ ∩ t i).Nonempty

Tactic:
rcases htd i₀ i with ⟨j, hji₀, hji⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst] (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:
(htn j).mono (subset_inter hji₀ hji)

Premises used: Set.Nonempty.mono, Set.subset_inter
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst] (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)

Premises used: Set.Nonempty.mono, Set.subset_inter
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
hS : Nonempty.{u + 1} (↑S : Type u)
hSd : DirectedOn (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) S
hSn : ∀ U ∈ S, U.Nonempty
hSc : ∀ U ∈ S, IsCompact U
hScl : ∀ U ∈ S, IsClosed[inst] U
rw : Set.Nonempty.{u} (α := X) (⋂ (i : (↑S : Type u)), (↑i : Set X))
⊢ (⋂₀ S).Nonempty

Tactic:
rw [sInter_eq_iInter]

Premises used: Set.sInter_eq_iInter
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
hS : Nonempty.{u + 1} (↑S : Type u)
hSd : DirectedOn (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) S
hSn : ∀ U ∈ S, U.Nonempty
hSc : ∀ U ∈ S, IsCompact U
hScl : ∀ U ∈ S, IsClosed[inst] U
⊢ Set.Nonempty.{u} (α := X) (⋂ (i : (↑S : Type u)), (↑i : Set X))

Tactic:
IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _
    (DirectedOn.directed_val hSd) (fun i ↦ hSn i i.2) (fun i ↦ hSc i i.2) (fun i ↦ hScl i i.2)

Premises used: IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed, DirectedOn.directed_val, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
hS : Nonempty.{u + 1} (↑S : Type u)
hSd : DirectedOn (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) S
hSn : ∀ U ∈ S, U.Nonempty
hSc : ∀ U ∈ S, IsCompact U
hScl : ∀ U ∈ S, IsClosed[inst] U
⊢ Set.Nonempty.{u} (α := X) (⋂ (i : (↑S : Type u)), (↑i : Set X))

Tactic:
exact IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _
    (DirectedOn.directed_val hSd) (fun i ↦ hSn i i.2) (fun i ↦ hSc i i.2) (fun i ↦ hScl i i.2)

Premises used: IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed, DirectedOn.directed_val, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
t : ℕ → Set X
htd : ∀ (i : ℕ), t (i + 1) ⊆ t i
htn : ∀ (i : ℕ), (t i).Nonempty
ht0 : IsCompact (t 0)
htcl : ∀ (i : ℕ), IsClosed[inst] (t i)
⊢ Set.Nonempty.{u} (α := X) (⋂ (i : ℕ), t i)

Tactic:
have tmono : Antitone t := antitone_nat_of_succ_le htd
  have htd : Directed (· ⊇ ·) t := tmono.directed_ge
  have : ∀ i, t i ⊆ t 0 := fun i => tmono <| Nat.zero_le i
  have htc : ∀ i, IsCompact (t i) := fun i => ht0.of_isClosed_subset (htcl i) (this i)
  IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed t htd htn htc htcl

Premises used: Nat.zero_le, Antitone.directed_ge, IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed, antitone_nat_of_succ_le, IsCompact.of_isClosed_subset
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ i ∈ b, IsOpen[inst] (c i)
hc₂ : s ⊆ ⋃ i ∈ b, c i
⊢ ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))

Tactic:
simp only [Subtype.forall', biUnion_eq_iUnion] at hc₁ hc₂

Premises used: Set.biUnion_eq_iUnion, Subtype.forall'
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ i ∈ b, IsOpen[inst] (c i)
hc₂ : s ⊆ ⋃ i ∈ b, c i
hc₃ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))
⊢ s ⊆ ⋃ (x : (↑b : Type u_1)), c (↑x : ι)

Tactic:
simp only [Subtype.forall', biUnion_eq_iUnion] at hc₁ hc₂

Premises used: Set.biUnion_eq_iUnion, Subtype.forall'
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))
hc₂ : s ⊆ ⋃ (x : (↑b : Type u_1)), c (↑x : ι)
rcases : ∀ (d : Finset (↑b : Type u_1)) (hd : s ⊆ ⋃ i ∈ d, c (↑i : ι)), ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i
⊢ ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i

Tactic:
rcases hs.elim_finite_subcover (fun i => c i : b → Set X) hc₁ hc₂ with ⟨d, hd⟩

Premises used: IsCompact.elim_finite_subcover, Subtype.val
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))
hc₂ : s ⊆ ⋃ (x : (↑b : Type u_1)), c (↑x : ι)
d : Finset (↑b : Type u_1)
hd : s ⊆ ⋃ i ∈ d, c (↑i : ι)
⊢ ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i

Tactic:
⟨Subtype.val '' (d : Set b), ?_, d.finite_toSet.image _, ?_⟩

Premises used: Set.Finite.image, SetLike.coe, And.intro, Exists.intro, Set.image, Finset.finite_toSet, Subtype.val
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))
hc₂ : s ⊆ ⋃ (x : (↑b : Type u_1)), c (↑x : ι)
d : Finset (↑b : Type u_1)
hd : s ⊆ ⋃ i ∈ d, c (↑i : ι)
refine_1 : Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' (↑d : Set (↑b : Type u_1)) ⊆ b
refine_2 : s ⊆ ⋃ i ∈ Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' (↑d : Set (↑b : Type u_1)), c i
⊢ ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i

Tactic:
refine ⟨Subtype.val '' (d : Set b), ?_, d.finite_toSet.image _, ?_⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))
hc₂ : s ⊆ ⋃ (x : (↑b : Type u_1)), c (↑x : ι)
d : Finset (↑b : Type u_1)
hd : s ⊆ ⋃ i ∈ d, c (↑i : ι)
⊢ Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' (↑d : Set (↑b : Type u_1)) ⊆ b

Tactic:
simp
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))
hc₂ : s ⊆ ⋃ (x : (↑b : Type u_1)), c (↑x : ι)
d : Finset (↑b : Type u_1)
hd : s ⊆ ⋃ i ∈ d, c (↑i : ι)
refine_2 refine_2₁ refine_2₂ refine_2₃ : s ⊆ ⋃ y ∈ (↑d : Set (↑b : Type u_1)), c (↑y : ι)
⊢ s ⊆ ⋃ i ∈ Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' (↑d : Set (↑b : Type u_1)), c i

Tactic:
rwa [biUnion_image]

Premises used: Set.biUnion_image
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (U : ι → Set X),
    (∀ (i : ι), IsOpen[inst] (U i)) → s ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
contrapose! :
  ∀ (h : ∀ (x : X) (_ : x ∈ s), ¬ClusterPt x f),
    ∃ (ι : Type u) (U : ι → Set X),
      (∀ (i : ι), IsOpen[inst] (U i)) ∧ s ⊆ ⋃ (i : ι), U i ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ i ∈ t, U i
⊢ ∃ x ∈ s, ClusterPt x f

Tactic:
contrapose! h