awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
h : ∀ (x : X) (_ : x ∈ s), ¬ClusterPt x f
⊢ ∀ (x : (↑s : Type u)), ∃ (i : Set X), ((↑x : X) ∈ i ∧ IsOpen[inst] i) ∧ iᶜ ∈ f

Tactic:
simp only [ClusterPt, not_neBot, ← disjoint_iff, SetCoe.forall',
    (nhds_basis_opens _).disjoint_iff_left] at h

Premises used: disjoint_iff, ClusterPt, Filter.HasBasis.disjoint_iff_left, Filter.not_neBot, nhds_basis_opens, SetCoe.forall'
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
h : ∀ (x : (↑s : Type u)), ∃ (i : Set X), ((↑x : X) ∈ i ∧ IsOpen[inst] i) ∧ iᶜ ∈ f
choose :
  ∀ (U : (x : (↑s : Type u)) → Set X) (hU : ∀ (x : (↑s : Type u)), (↑x : X) ∈ U x ∧ IsOpen[inst] (U x))
    (hUf : ∀ (x : (↑s : Type u)), (U x)ᶜ ∈ f),
    ∃ (ι : Type u) (U : ι → Set X),
      (∀ (i : ι), IsOpen[inst] (U i)) ∧ s ⊆ ⋃ (i : ι), U i ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ i ∈ t, U i
⊢ ∃ (ι : Type u) (U : ι → Set X),
    (∀ (i : ι), IsOpen[inst] (U i)) ∧ s ⊆ ⋃ (i : ι), U i ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ i ∈ t, U i

Tactic:
choose U hU hUf using h
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
U : (x : (↑s : Type u)) → Set X
hU : ∀ (x : (↑s : Type u)), (↑x : X) ∈ U x ∧ IsOpen[inst] (U x)
hUf : ∀ (x : (↑s : Type u)), (U x)ᶜ ∈ f
⊢ ∃ (ι : Type u) (U : ι → Set X),
    (∀ (i : ι), IsOpen[inst] (U i)) ∧ s ⊆ ⋃ (i : ι), U i ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ i ∈ t, U i

Tactic:
⟨s, U, fun x => (hU x).2, fun x hx => mem_iUnion.2 ⟨⟨x, hx⟩, (hU _).1⟩, fun t ht => ?_⟩

Premises used: Iff.mpr, Set.mem_iUnion, Set.Elem, Subtype.mk, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
U : (x : (↑s : Type u)) → Set X
hU : ∀ (x : (↑s : Type u)), (↑x : X) ∈ U x ∧ IsOpen[inst] (U x)
hUf : ∀ (x : (↑s : Type u)), (U x)ᶜ ∈ f
refine : ∀ (t : Finset (↑s : Type u)) (ht : s ⊆ ⋃ i ∈ t, U i), False
⊢ ∃ (ι : Type u) (U : ι → Set X),
    (∀ (i : ι), IsOpen[inst] (U i)) ∧ s ⊆ ⋃ (i : ι), U i ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ i ∈ t, U i

Tactic:
refine ⟨s, U, fun x => (hU x).2, fun x hx => mem_iUnion.2 ⟨⟨x, hx⟩, (hU _).1⟩, fun t ht => ?_⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
U : (x : (↑s : Type u)) → Set X
hU : ∀ (x : (↑s : Type u)), (↑x : X) ∈ U x ∧ IsOpen[inst] (U x)
hUf : ∀ (x : (↑s : Type u)), (U x)ᶜ ∈ f
t : Finset (↑s : Type u)
ht : s ⊆ ⋃ i ∈ t, U i
⊢ False

Tactic:
compl_notMem (le_principal_iff.1 hfs) ?_

Premises used: Filter.le_principal_iff, Iff.mp, Filter.compl_notMem
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
U : (x : (↑s : Type u)) → Set X
hU : ∀ (x : (↑s : Type u)), (↑x : X) ∈ U x ∧ IsOpen[inst] (U x)
hUf : ∀ (x : (↑s : Type u)), (U x)ᶜ ∈ f
t : Finset (↑s : Type u)
ht : s ⊆ ⋃ i ∈ t, U i
refine : sᶜ ∈ f
⊢ False

Tactic:
refine compl_notMem (le_principal_iff.1 hfs) ?_

Premises used: Filter.le_principal_iff, Iff.mp, Filter.compl_notMem
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
U : (x : (↑s : Type u)) → Set X
hU : ∀ (x : (↑s : Type u)), (↑x : X) ∈ U x ∧ IsOpen[inst] (U x)
hUf : ∀ (x : (↑s : Type u)), (U x)ᶜ ∈ f
t : Finset (↑s : Type u)
ht : s ⊆ ⋃ i ∈ t, U i
⊢ sᶜ ∈ f

Tactic:
mem_of_superset ((biInter_finset_mem t).2 fun x _ => hUf x) ?_

Premises used: Iff.mpr, Filter.biInter_finset_mem, Filter.mem_of_superset
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
U : (x : (↑s : Type u)) → Set X
hU : ∀ (x : (↑s : Type u)), (↑x : X) ∈ U x ∧ IsOpen[inst] (U x)
hUf : ∀ (x : (↑s : Type u)), (U x)ᶜ ∈ f
t : Finset (↑s : Type u)
ht : s ⊆ ⋃ i ∈ t, U i
refine : ⋂ i ∈ t, (U i)ᶜ ⊆ sᶜ
⊢ sᶜ ∈ f

Tactic:
refine mem_of_superset ((biInter_finset_mem t).2 fun x _ => hUf x) ?_

Premises used: Iff.mpr, Filter.biInter_finset_mem, Filter.mem_of_superset
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
U : (x : (↑s : Type u)) → Set X
hU : ∀ (x : (↑s : Type u)), (↑x : X) ∈ U x ∧ IsOpen[inst] (U x)
hUf : ∀ (x : (↑s : Type u)), (U x)ᶜ ∈ f
t : Finset (↑s : Type u)
ht : s ⊆ ⋃ i ∈ t, U i
rw : s ⊆ ⋃ i ∈ t, (U i)ᶜᶜ
⊢ ⋂ i ∈ t, (U i)ᶜ ⊆ sᶜ

Tactic:
rw [subset_compl_comm, compl_iInter₂]

Premises used: Set.compl_iInter₂, Set.subset_compl_comm
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
U : (x : (↑s : Type u)) → Set X
hU : ∀ (x : (↑s : Type u)), (↑x : X) ∈ U x ∧ IsOpen[inst] (U x)
hUf : ∀ (x : (↑s : Type u)), (U x)ᶜ ∈ f
t : Finset (↑s : Type u)
ht : s ⊆ ⋃ i ∈ t, U i
⊢ s ⊆ ⋃ i ∈ t, (U i)ᶜᶜ

Tactic:
simpa only [compl_compl]

Premises used: compl_compl
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst] (t i)) → s ∩ ⋂ (i : ι), t i = ∅ → ∃ (u : Finset ι), s ∩ ⋂ i ∈ u, t i = ∅
ι : Type u
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
⊢ s ⊓ ⋂ (i : ι), (U i)ᶜ = ⊥

Tactic:
rw [← disjoint_compl_right_iff_subset, compl_iUnion, disjoint_iff] at hsU

Premises used: disjoint_iff, Set.disjoint_compl_right_iff_subset, Set.compl_iUnion
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst] (t i)) → s ∩ ⋂ (i : ι), t i = ∅ → ∃ (u : Finset ι), s ∩ ⋂ i ∈ u, t i = ∅
ι : Type u
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊓ ⋂ (i : ι), (U i)ᶜ = ⊥
rcases : ∀ (t : Finset ι) (ht : s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅), ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i
⊢ ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i

Tactic:
rcases h (fun i => (U i)ᶜ) (fun i => (hUo _).isClosed_compl) hsU with ⟨t, ht⟩

Premises used: Compl.compl, IsOpen.isClosed_compl
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst] (t i)) → s ∩ ⋂ (i : ι), t i = ∅ → ∃ (u : Finset ι), s ∩ ⋂ i ∈ u, t i = ∅
ι : Type u
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊓ ⋂ (i : ι), (U i)ᶜ = ⊥
t : Finset ι
ht : s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
⊢ ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i

Tactic:
⟨t, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst] (t i)) → s ∩ ⋂ (i : ι), t i = ∅ → ∃ (u : Finset ι), s ∩ ⋂ i ∈ u, t i = ∅
ι : Type u
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊓ ⋂ (i : ι), (U i)ᶜ = ⊥
t : Finset ι
ht : s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
refine : s ⊆ ⋃ i ∈ t, U i
⊢ ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i

Tactic:
refine ⟨t, ?_⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst] (t i)) → s ∩ ⋂ (i : ι), t i = ∅ → ∃ (u : Finset ι), s ∩ ⋂ i ∈ u, t i = ∅
ι : Type u
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊓ ⋂ (i : ι), (U i)ᶜ = ⊥
t : Finset ι
ht : s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
rwa : Disjoint s (⋃ i ∈ t, U i)ᶜ
rwa₁ : Disjoint s (⋂ i ∈ t, (U i)ᶜ)
rwa₂ rwa₃ rwa₄ rwa₅ : s ⊓ ⋂ i ∈ t, (U i)ᶜ = ⊥
⊢ s ⊆ ⋃ i ∈ t, U i

Tactic:
rwa [← disjoint_compl_right_iff_subset, compl_iUnion₂, disjoint_iff]

Premises used: disjoint_iff, Set.compl_iUnion₂, Set.disjoint_compl_right_iff_subset
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsCompact s ↔
    ∀ {ι : Type u} (U : ι → Set X),
      (∀ (i : ι), IsOpen[inst] (U i)) → s ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i

Tactic:
⟨fun hs => hs.elim_finite_subcover, isCompact_of_finite_subcover⟩

Premises used: IsCompact.elim_finite_subcover, Iff.intro, isCompact_of_finite_subcover
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsCompact s ↔
    ∀ {ι : Type u} (t : ι → Set X),
      (∀ (i : ι), IsClosed[inst] (t i)) → s ∩ ⋂ (i : ι), t i = ∅ → ∃ (u : Finset ι), s ∩ ⋂ i ∈ u, t i = ∅

Tactic:
⟨fun hs => hs.elim_finite_subfamily_closed, isCompact_of_finite_subfamily_closed⟩

Premises used: Iff.intro, IsCompact.elim_finite_subfamily_closed, isCompact_of_finite_subfamily_closed
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
⊢ s ∈ SProd.sprod (α := Filter X) (𝓝ˢ ∅) l

Tactic:
simp
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
refine_1 : ∀ (t t' : Set X) (ht : t ⊆ t') (hs : s ∈ 𝓝ˢ t' ×ˢ l), s ∈ 𝓝ˢ t ×ˢ l
refine_2 : ∀ (t t' : Set X) (ht : s ∈ 𝓝ˢ t ×ˢ l) (ht' : s ∈ 𝓝ˢ t' ×ˢ l), s ∈ 𝓝ˢ (t ∪ t') ×ˢ l
refine_3 : ∀ (x : X) (hx : x ∈ K), ∃ t ∈ 𝓝[K] x, s ∈ 𝓝ˢ t ×ˢ l
⊢ s ∈ 𝓝ˢ K ×ˢ l

Tactic:
refine hK.induction_on (by simp) (fun t t' ht hs ↦ ?_) (fun t t' ht ht' ↦ ?_) fun x hx ↦ ?_
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs_1 : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
t t' : Set X
ht : t ⊆ t'
hs : s ∈ 𝓝ˢ t' ×ˢ l
⊢ s ∈ 𝓝ˢ t ×ˢ l

Tactic:
prod_mono (nhdsSet_mono ht) le_rfl hs

Premises used: le_rfl, nhdsSet_mono, Filter.prod_mono
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs_1 : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
t t' : Set X
ht : t ⊆ t'
hs : s ∈ 𝓝ˢ t' ×ˢ l
⊢ s ∈ 𝓝ˢ t ×ˢ l

Tactic:
exact prod_mono (nhdsSet_mono ht) le_rfl hs

Premises used: le_rfl, nhdsSet_mono, Filter.prod_mono
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
t t' : Set X
ht : s ∈ 𝓝ˢ t ×ˢ l
ht' : s ∈ 𝓝ˢ t' ×ˢ l
⊢ s ∈ 𝓝ˢ (t ∪ t') ×ˢ l

Tactic:
simp [sup_prod, *]

Premises used: Filter.sup_prod
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
x : X
hx : x ∈ K
refine_3 :
  ∀ (u : Set X) (v : Set Y) (hs : (u, v).1 ×ˢ id (u, v).2 ⊆ s) (hv : (u, v).2 ∈ l) (hx : x ∈ (u, v).1)
    (huo : IsOpen[inst] (u, v).1), ∃ t ∈ 𝓝[K] x, s ∈ 𝓝ˢ t ×ˢ l
⊢ ∃ t ∈ 𝓝[K] x, s ∈ 𝓝ˢ t ×ˢ l

Tactic:
rcases ((nhds_basis_opens _).prod l.basis_sets).mem_iff.1 (hs x hx)
      with ⟨⟨u, v⟩, ⟨⟨hx, huo⟩, hv⟩, hs⟩

Premises used: Filter.HasBasis.mem_iff, Filter.basis_sets, Iff.mp, nhds_basis_opens, Filter.HasBasis.prod
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs_1 : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
x : X
hx_1 : x ∈ K
u : Set X
v : Set Y
hs : (u, v).1 ×ˢ id (u, v).2 ⊆ s
hv : (u, v).2 ∈ l
hx : x ∈ (u, v).1
huo : IsOpen[inst] (u, v).1
⊢ ∃ t ∈ 𝓝[K] x, s ∈ 𝓝ˢ t ×ˢ l

Tactic:
⟨u, nhdsWithin_le_nhds (huo.mem_nhds hx), mem_of_superset ?_ hs⟩

Premises used: nhdsWithin_le_nhds, And.intro, IsOpen.mem_nhds, Exists.intro, Filter.mem_of_superset
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs_1 : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
x : X
hx_1 : x ∈ K
u : Set X
v : Set Y
hs : (u, v).1 ×ˢ id (u, v).2 ⊆ s
hv : (u, v).2 ∈ l
hx : x ∈ (u, v).1
huo : IsOpen[inst] (u, v).1
refine_3 : (u, v).1 ×ˢ id (u, v).2 ∈ 𝓝ˢ u ×ˢ l
⊢ ∃ t ∈ 𝓝[K] x, s ∈ 𝓝ˢ t ×ˢ l

Tactic:
refine ⟨u, nhdsWithin_le_nhds (huo.mem_nhds hx), mem_of_superset ?_ hs⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs_1 : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
x : X
hx_1 : x ∈ K
u : Set X
v : Set Y
hs : (u, v).1 ×ˢ id (u, v).2 ⊆ s
hv : (u, v).2 ∈ l
hx : x ∈ (u, v).1
huo : IsOpen[inst] (u, v).1
⊢ (u, v).1 ×ˢ id (u, v).2 ∈ 𝓝ˢ u ×ˢ l

Tactic:
prod_mem_prod (huo.mem_nhdsSet.2 Subset.rfl) hv

Premises used: Iff.mpr, Set.Subset.rfl, Filter.prod_mem_prod, IsOpen.mem_nhdsSet
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs_1 : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
x : X
hx_1 : x ∈ K
u : Set X
v : Set Y
hs : (u, v).1 ×ˢ id (u, v).2 ⊆ s
hv : (u, v).2 ∈ l
hx : x ∈ (u, v).1
huo : IsOpen[inst] (u, v).1
⊢ (u, v).1 ×ˢ id (u, v).2 ∈ 𝓝ˢ u ×ˢ l

Tactic:
exact prod_mem_prod (huo.mem_nhdsSet.2 Subset.rfl) hv

Premises used: Iff.mpr, Set.Subset.rfl, Filter.prod_mem_prod, IsOpen.mem_nhdsSet
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
hK : IsCompact K
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hs : Membership.mem (γ := Filter (X × Y)) (⨆ x ∈ K, 𝓝 x ×ˢ l) s
⊢ ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l

Tactic:
simpa using hs
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
Y : Type v
inst : TopologicalSpace Y
K : Set Y
hK : IsCompact K
X : Type u_2
l : Filter X
⊢ l ×ˢ 𝓝ˢ K = ⨆ y ∈ K, l ×ˢ 𝓝 y

Tactic:
simp only [prod_comm (f := l), hK.nhdsSet_prod_eq_biSup, map_iSup]

Premises used: Filter.map_iSup, Filter.prod_comm, IsCompact.nhdsSet_prod_eq_biSup
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
Y : Type v
inst : TopologicalSpace Y
K : Set Y
X : Type u_2
l : Filter X
s : Set (X × Y)
hK : IsCompact K
hs : ∀ y ∈ K, s ∈ l ×ˢ 𝓝 y
⊢ Membership.mem (γ := Filter (X × Y)) (⨆ y ∈ K, l ×ˢ 𝓝 y) s

Tactic:
simpa using hs
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
hK : IsCompact K
l f : Filter X
⊢ f ⊓ l = comap (fun (x : X) ↦ (x, x)) (f ×ˢ l)

Tactic:
simpa only [comap_prod] using congrArg₂ (· ⊓ ·) comap_id.symm comap_id.symm

Premises used: Filter.comap_prod, congrArg₂, Filter.comap_id, Eq.symm, Min.min
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
hK : IsCompact K
l : Filter X
⊢ ∀ (f : Filter X), f ⊓ l = comap (fun (x : X) ↦ (x, x)) (f ×ˢ l)

Tactic:
have : ∀ f : Filter X, f ⊓ l = comap (fun x ↦ (x, x)) (f ×ˢ l) := fun f ↦ by
    simpa only [comap_prod] using congrArg₂ (· ⊓ ·) comap_id.symm comap_id.symm
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
hK : IsCompact K
l : Filter X
this : ∀ (f : Filter X), f ⊓ l = comap (fun (x : X) ↦ (x, x)) (f ×ˢ l)
simp_rw :
  Eq (α := Filter X) (comap (fun (x : X) ↦ (x, x)) (𝓝ˢ K ×ˢ l)) (⨆ x ∈ K, comap (fun (x : X) ↦ (x, x)) (𝓝 x ×ˢ l))
simp_rw₁ :
  Eq (α := Filter X) (comap (fun (x : X) ↦ (x, x)) (𝓝ˢ K ×ˢ l))
    (comap (β := X × X) (fun (x : X) ↦ (x, x)) (⨆ i ∈ K, 𝓝 i ×ˢ l))
⊢ 𝓝ˢ K ⊓ l = ⨆ x ∈ K, 𝓝 x ⊓ l

Tactic:
simp_rw [this, ← comap_iSup, hK.nhdsSet_prod_eq_biSup]

Premises used: IsCompact.nhdsSet_prod_eq_biSup, Filter.comap_iSup
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
hK : IsCompact K
l : Filter X
⊢ l ⊓ 𝓝ˢ K = ⨆ x ∈ K, l ⊓ 𝓝 x

Tactic:
simp only [inf_comm l, hK.nhdsSet_inf_eq_biSup]

Premises used: inf_comm, IsCompact.nhdsSet_inf_eq_biSup
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
l : Filter X
s : Set X
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ⊓ l
⊢ Membership.mem (γ := Filter X) (⨆ x ∈ K, 𝓝 x ⊓ l) s

Tactic:
simpa using hs
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
l : Filter X
s : Set X
hK : IsCompact K
hs : ∀ y ∈ K, s ∈ l ⊓ 𝓝 y
⊢ Membership.mem (γ := Filter X) (⨆ x ∈ K, l ⊓ 𝓝 x) s

Tactic:
simpa using hs
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ : X
K : Set Y
hK : IsCompact K
P : X → Y → Prop
hP : ∀ y ∈ K, ∀ᶠ (z : X × Y) in 𝓝 (x₀, y), P z.1 z.2
⊢ ∀ᶠ (z : X × Y) in 𝓝 x₀ ×ˢ 𝓝ˢ K, P z.1 z.2

Tactic:
simp only [nhds_prod_eq, ← eventually_iSup, ← hK.prod_nhdsSet_eq_biSup] at hP

Premises used: Filter.eventually_iSup, IsCompact.prod_nhdsSet_eq_biSup, nhds_prod_eq
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ : X
K : Set Y
hK : IsCompact K
P : X → Y → Prop
hP : ∀ᶠ (z : X × Y) in 𝓝 x₀ ×ˢ 𝓝ˢ K, P z.1 z.2
⊢ ∀ᶠ (x : X) in 𝓝 x₀, ∀ y ∈ K, P x y

Tactic:
hP.curry.mono fun _ h ↦ h.self_of_nhdsSet

Premises used: Filter.Eventually.curry, Filter.Eventually.mono, Filter.Eventually.self_of_nhdsSet
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ : X
K : Set Y
hK : IsCompact K
P : X → Y → Prop
hP : ∀ᶠ (z : X × Y) in 𝓝 x₀ ×ˢ 𝓝ˢ K, P z.1 z.2
⊢ ∀ᶠ (x : X) in 𝓝 x₀, ∀ y ∈ K, P x y

Tactic:
exact hP.curry.mono fun _ h ↦ h.self_of_nhdsSet

Premises used: Filter.Eventually.curry, Filter.Eventually.mono, Filter.Eventually.self_of_nhdsSet
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsCompact.{u} (X := X) ∅

Tactic:
fun _f hnf hsf =>
  Not.elim hnf.ne <| empty_mem_iff_bot.1 <| le_principal_iff.1 hsf

Premises used: Filter.le_principal_iff, Filter.NeBot.ne, Not.elim, Filter.empty_mem_iff_bot, Iff.mp, IsCompact
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
x : X
x_1 : Filter X
hf : x_1.NeBot
hfa : x_1 ≤ 𝓟 {x}
⊢ 𝓟 {x} ≤ 𝓝 x

Tactic:
simpa only [principal_singleton] using pure_le_nhds x

Premises used: pure_le_nhds, Filter.principal_singleton
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : s.Subsingleton
⊢ IsCompact s

Tactic:
Subsingleton.induction_on hs isCompact_empty fun _ => isCompact_singleton

Premises used: Set.Subsingleton.induction_on, isCompact_singleton, isCompact_empty
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
hl : ⋃ i ∈ s, f i ∈ l
⊢ ∃ i ∈ s, f i ∈ l

Tactic:
rw [Ultrafilter.finite_biUnion_mem_iff hs] at hl

Premises used: Ultrafilter.finite_biUnion_mem_iff
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
hl : ∃ i ∈ s, f i ∈ l
rcases :
  ∀ (i : ι) (his : i ∈ s) (hi : f i ∈ l),
    ∃ (x : X), Membership.mem (γ := Set X) (⋃ i ∈ s, f i) x ∧ (↑l : Filter X) ≤ 𝓝 x
⊢ ∃ (x : X), Membership.mem (γ := Set X) (⋃ i ∈ s, f i) x ∧ (↑l : Filter X) ≤ 𝓝 x

Tactic:
rcases hl with ⟨i, his, hi⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
i : ι
his : i ∈ s
hi : f i ∈ l
rcases :
  ∀ (x : X) (hxi : x ∈ f i) (hlx : (↑l : Filter X) ≤ 𝓝 x),
    ∃ (x : X), Membership.mem (γ := Set X) (⋃ i ∈ s, f i) x ∧ (↑l : Filter X) ≤ 𝓝 x
⊢ ∃ (x : X), Membership.mem (γ := Set X) (⋃ i ∈ s, f i) x ∧ (↑l : Filter X) ≤ 𝓝 x

Tactic:
rcases (hf i his).ultrafilter_le_nhds _ (le_principal_iff.2 hi) with ⟨x, hxi, hlx⟩

Premises used: Iff.mpr, Filter.le_principal_iff, IsCompact.ultrafilter_le_nhds
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
i : ι
his : i ∈ s
hi : f i ∈ l
x : X
hxi : x ∈ f i
hlx : (↑l : Filter X) ≤ 𝓝 x
⊢ ∃ (x : X), Membership.mem (γ := Set X) (⋃ i ∈ s, f i) x ∧ (↑l : Filter X) ≤ 𝓝 x

Tactic:
⟨x, mem_iUnion₂.2 ⟨i, his, hxi⟩, hlx⟩

Premises used: Iff.mpr, Set.mem_iUnion₂, And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
i : ι
his : i ∈ s
hi : f i ∈ l
x : X
hxi : x ∈ f i
hlx : (↑l : Filter X) ≤ 𝓝 x
⊢ ∃ (x : X), Membership.mem (γ := Set X) (⋃ i ∈ s, f i) x ∧ (↑l : Filter X) ≤ 𝓝 x

Tactic:
exact ⟨x, mem_iUnion₂.2 ⟨i, his, hxi⟩, hlx⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Finset ι
f : ι → Set X
hf : ∀ i ∈ s, IsCompact (f i)
⊢ IsCompact.{u} (X := X) (⋃ i ∈ s, f i)

Tactic:
s.finite_toSet.isCompact_biUnion hf

Premises used: Set.Finite.isCompact_biUnion, Finset.finite_toSet
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
K : ℕ → Set X
hK : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
⊢ IsCompact (accumulate K n)

Tactic:
(finite_le_nat n).isCompact_biUnion fun k _ => hK k

Premises used: Set.Mem, setOf, Set.accumulate, Set.Finite.isCompact_biUnion, Set.finite_le_nat
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
hf : S.Finite
hc : ∀ s ∈ S, IsCompact s
rw : IsCompact.{u} (X := X) (⋃ i ∈ S, i)
⊢ IsCompact (⋃₀ S)

Tactic:
rw [sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
hf : S.Finite
hc : ∀ s ∈ S, IsCompact s
⊢ IsCompact.{u} (X := X) (⋃ i ∈ S, i)

Tactic:
hf.isCompact_biUnion hc

Premises used: Set.Finite.isCompact_biUnion
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
hf : S.Finite
hc : ∀ s ∈ S, IsCompact s
⊢ IsCompact.{u} (X := X) (⋃ i ∈ S, i)

Tactic:
exact hf.isCompact_biUnion hc

Premises used: Set.Finite.isCompact_biUnion
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
ι : Sort u_2
f : ι → Set X
inst_1 : Finite ι
h : ∀ (i : ι), IsCompact (f i)
⊢ IsCompact.{u} (X := X) (⋃ (i : ι), f i)

Tactic:
(finite_range f).isCompact_sUnion <| forall_mem_range.2 h

Premises used: Iff.mpr, Set.forall_mem_range, Set.Mem, iSup, setOf, Set.finite_range, Set.Finite.isCompact_sUnion, Set.iUnion
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : s.Finite
⊢ IsCompact s

Tactic:
biUnion_of_singleton s ▸ hs.isCompact_biUnion fun _ _ => isCompact_singleton

Premises used: Set.biUnion_of_singleton, Eq.rec, isCompact_singleton, Set.Finite.isCompact_biUnion
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
x : X
⊢ Membership.mem (γ := Set (Set X))
      {x : Set X |
        match (motive := Set X → Prop) x with
        | s => IsCompact s}
      {x} ∧
    Membership.mem (γ := Set X) {x} x

Tactic:
simp
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : DiscreteTopology X
hs : IsCompact s
⊢ ∀ (x : X), {x} ∈ 𝓝 x

Tactic:
simp [nhds_discrete]

Premises used: nhds_discrete
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : DiscreteTopology X
hs : IsCompact s
⊢ ∀ (x : X), {x} ∈ 𝓝 x

Tactic:
have : ∀ x : X, ({x} : Set X) ∈ 𝓝 x := by simp [nhds_discrete]
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : DiscreteTopology X
hs : IsCompact s
this : ∀ (x : X), {x} ∈ 𝓝 x
rcases : ∀ (t : Finset X), (∀ x ∈ t, x ∈ s) → ∀ (hst : s ⊆ ⋃ x ∈ t, {x}), s.Finite
⊢ s.Finite

Tactic:
rcases hs.elim_nhds_subcover (fun x => {x}) fun x _ => this x with ⟨t, _, hst⟩

Premises used: IsCompact.elim_nhds_subcover, Singleton.singleton