awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : Filter Y
hs : IsCompact s
hf : Disjoint f (cocompact Y)
K : Set Y
hKf : K ∈ f
hK : IsCompact K
⊢ 𝓝ˢ s ×ˢ 𝓟 K ≤ 𝓝ˢ s ×ˢ 𝓝ˢ K

Tactic:
Filter.prod_mono_right _ principal_le_nhdsSet

Premises used: Filter.prod_mono_right, principal_le_nhdsSet
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : Filter Y
hs : IsCompact s
hf : Disjoint f (cocompact Y)
K : Set Y
hKf : K ∈ f
hK : IsCompact K
⊢ 𝓝ˢ s ×ˢ 𝓝ˢ K = 𝓝ˢ (s ×ˢ K)

Tactic:
(hs.nhdsSet_prod_eq hK).symm

Premises used: IsCompact.nhdsSet_prod_eq, Eq.symm
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : Filter Y
hs : IsCompact s
hf : Disjoint f (cocompact Y)
K : Set Y
hKf : K ∈ f
hK : IsCompact K
⊢ 𝓝ˢ (s ×ˢ K) ≤ 𝓝ˢ (SProd.sprod (β := Set Y) s univ)

Tactic:
nhdsSet_mono (prod_mono_right le_top)

Premises used: Set.prod_mono_right, nhdsSet_mono, le_top
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : Filter Y
hs : IsCompact s
hf : Disjoint f (cocompact Y)
K : Set Y
hKf : K ∈ f
hK : IsCompact K
⊢ 𝓝ˢ s ×ˢ f ≤ 𝓝ˢ (SProd.sprod (β := Set Y) s univ)

Tactic:
calc
    𝓝ˢ s ×ˢ f
    _ ≤ 𝓝ˢ s ×ˢ 𝓟 K := Filter.prod_mono_right _ (Filter.le_principal_iff.mpr hKf)
    _ ≤ 𝓝ˢ s ×ˢ 𝓝ˢ K := Filter.prod_mono_right _ principal_le_nhdsSet
    _ = 𝓝ˢ (s ×ˢ K) := (hs.nhdsSet_prod_eq hK).symm
    _ ≤ 𝓝ˢ (s ×ˢ Set.univ) := nhdsSet_mono (prod_mono_right le_top)

Premises used: Iff.mpr, Filter.le_principal_iff, Set.prod_mono_right, SProd.sprod, nhdsSet_mono, Set.univ, IsCompact.nhdsSet_prod_eq, le_top, Filter.principal, Eq.symm, nhdsSet, Filter.prod_mono_right, principal_le_nhdsSet
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
t : Set Y
f : Filter X
ht : IsCompact t
hf : Disjoint f (cocompact X)
obtain : ∀ (K : Set X) (hKf : K ∈ f) (hK : IsCompact K), f ×ˢ 𝓝ˢ t ≤ 𝓝ˢ (SProd.sprod (α := Set X) univ t)
⊢ f ×ˢ 𝓝ˢ t ≤ 𝓝ˢ (SProd.sprod (α := Set X) univ t)

Tactic:
obtain ⟨K, hKf, hK⟩ := (disjoint_cocompact_right f).mp hf

Premises used: Iff.mp, Filter.disjoint_cocompact_right
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
t : Set Y
f : Filter X
ht : IsCompact t
hf : Disjoint f (cocompact X)
K : Set X
hKf : K ∈ f
hK : IsCompact K
⊢ f ×ˢ 𝓝ˢ t ≤ 𝓟 K ×ˢ 𝓝ˢ t

Tactic:
Filter.prod_mono_left _ (Filter.le_principal_iff.mpr hKf)

Premises used: Iff.mpr, Filter.le_principal_iff, Filter.prod_mono_left
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
t : Set Y
f : Filter X
ht : IsCompact t
hf : Disjoint f (cocompact X)
K : Set X
hKf : K ∈ f
hK : IsCompact K
⊢ 𝓝ˢ K ×ˢ 𝓝ˢ t = 𝓝ˢ (K ×ˢ t)

Tactic:
(hK.nhdsSet_prod_eq ht).symm

Premises used: IsCompact.nhdsSet_prod_eq, Eq.symm
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
t : Set Y
f : Filter X
ht : IsCompact t
hf : Disjoint f (cocompact X)
K : Set X
hKf : K ∈ f
hK : IsCompact K
⊢ 𝓝ˢ (K ×ˢ t) ≤ 𝓝ˢ (SProd.sprod (α := Set X) univ t)

Tactic:
nhdsSet_mono (prod_mono_left le_top)

Premises used: Set.Mem, nhdsSet_mono, setOf, Set.prod_mono_left, le_top
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
t : Set Y
f : Filter X
ht : IsCompact t
hf : Disjoint f (cocompact X)
K : Set X
hKf : K ∈ f
hK : IsCompact K
⊢ f ×ˢ 𝓝ˢ t ≤ 𝓝ˢ (SProd.sprod (α := Set X) univ t)

Tactic:
calc
    f ×ˢ 𝓝ˢ t
    _ ≤ (𝓟 K) ×ˢ 𝓝ˢ t := Filter.prod_mono_left _ (Filter.le_principal_iff.mpr hKf)
    _ ≤ 𝓝ˢ K ×ˢ 𝓝ˢ t := Filter.prod_mono_left _ principal_le_nhdsSet
    _ = 𝓝ˢ (K ×ˢ t) := (hK.nhdsSet_prod_eq ht).symm
    _ ≤ 𝓝ˢ (Set.univ ×ˢ t) := nhdsSet_mono (prod_mono_left le_top)

Premises used: Iff.mpr, Filter.le_principal_iff, SProd.sprod, nhdsSet_mono, Set.univ, IsCompact.nhdsSet_prod_eq, Set.prod_mono_left, le_top, Filter.principal, Eq.symm, nhdsSet, Filter.prod_mono_left, principal_le_nhdsSet
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : Filter Y
x : X
hf : Disjoint f (cocompact Y)
⊢ 𝓝 x ×ˢ f ≤ 𝓝ˢ (SProd.sprod (α := Set X) (β := Set Y) {x} univ)

Tactic:
simpa using nhdsSet_prod_le_of_disjoint_cocompact isCompact_singleton hf

Premises used: isCompact_singleton, nhdsSet_prod_le_of_disjoint_cocompact
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : Filter X
y : Y
hf : Disjoint f (cocompact X)
⊢ f ×ˢ 𝓝 y ≤ 𝓝ˢ (SProd.sprod (α := Set X) (β := Set Y) univ {y})

Tactic:
simpa using prod_nhdsSet_le_of_disjoint_cocompact isCompact_singleton hf

Premises used: isCompact_singleton, prod_nhdsSet_le_of_disjoint_cocompact
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : IsOpen[instTopologicalSpaceProd] n
hp : s ×ˢ t ⊆ n
⊢ ∃ (i : Prod.{u, v} (Set X) (Set Y)), ((IsOpen[inst] i.1 ∧ s ⊆ i.1) ∧ IsOpen[inst_1] i.2 ∧ t ⊆ i.2) ∧ i.1 ×ˢ i.2 ⊆ n

Tactic:
rw [← hn.mem_nhdsSet, hs.nhdsSet_prod_eq ht,
    ((hasBasis_nhdsSet _).prod (hasBasis_nhdsSet _)).mem_iff] at hp

Premises used: Filter.HasBasis.mem_iff, hasBasis_nhdsSet, IsCompact.nhdsSet_prod_eq, IsOpen.mem_nhdsSet, Filter.HasBasis.prod
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : IsOpen[instTopologicalSpaceProd] n
hp : ∃ (i : Prod.{u, v} (Set X) (Set Y)), ((IsOpen[inst] i.1 ∧ s ⊆ i.1) ∧ IsOpen[inst_1] i.2 ∧ t ⊆ i.2) ∧ i.1 ×ˢ i.2 ⊆ n
rcases :
  ∀ (u : Set X) (v : Set Y) (hn : (u, v).1 ×ˢ (u, v).2 ⊆ n) (huo : IsOpen[inst] (u, v).1) (hsu : s ⊆ (u, v).1)
    (hvo : IsOpen[inst_1] (u, v).2) (htv : t ⊆ (u, v).2),
    ∃ (u : Set X) (v : Set Y), IsOpen[inst] u ∧ IsOpen[inst_1] v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n
⊢ ∃ (u : Set X) (v : Set Y), IsOpen[inst] u ∧ IsOpen[inst_1] v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n

Tactic:
rcases hp with ⟨⟨u, v⟩, ⟨⟨huo, hsu⟩, hvo, htv⟩, hn⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn_1 : IsOpen[instTopologicalSpaceProd] n
u : Set X
v : Set Y
hn : (u, v).1 ×ˢ (u, v).2 ⊆ n
huo : IsOpen[inst] (u, v).1
hsu : s ⊆ (u, v).1
hvo : IsOpen[inst_1] (u, v).2
htv : t ⊆ (u, v).2
⊢ ∃ (u : Set X) (v : Set Y), IsOpen[inst] u ∧ IsOpen[inst_1] v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n

Tactic:
⟨u, v, huo, hvo, hsu, htv, hn⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn_1 : IsOpen[instTopologicalSpaceProd] n
u : Set X
v : Set Y
hn : (u, v).1 ×ˢ (u, v).2 ⊆ n
huo : IsOpen[inst] (u, v).1
hsu : s ⊆ (u, v).1
hvo : IsOpen[inst_1] (u, v).2
htv : t ⊆ (u, v).2
⊢ ∃ (u : Set X) (v : Set Y), IsOpen[inst] u ∧ IsOpen[inst_1] v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n

Tactic:
exact ⟨u, v, huo, hvo, hsu, htv, hn⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s s' : Set X
t t' : Set Y
hs : IsCompact s
ht : IsCompact t
⊢ 𝓝ˢ[s' ×ˢ t'] (s ×ˢ t) = 𝓝ˢ[s'] s ×ˢ 𝓝ˢ[t'] t

Tactic:
simp [nhdsSetWithin, ← prod_inf_prod, hs.nhdsSet_prod_eq ht]

Premises used: Filter.prod_inf_prod, IsCompact.nhdsSet_prod_eq, nhdsSetWithin
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s s' : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : n ∈ 𝓝ˢ[s' ×ˢ t'] (s ×ˢ t)
rwa : ∀ (hn : n ∈ 𝓝ˢ[s'] s ×ˢ 𝓝ˢ[t'] t), ∃ u ∈ 𝓝ˢ[s'] s, ∃ v ∈ 𝓝ˢ[t'] t, u ×ˢ v ⊆ n
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (hn : ∃ t₁ ∈ 𝓝ˢ[s'] s, ∃ t₂ ∈ 𝓝ˢ[t'] t, t₁ ×ˢ t₂ ⊆ n), ∃ u ∈ 𝓝ˢ[s'] s, ∃ v ∈ 𝓝ˢ[t'] t, u ×ˢ v ⊆ n
⊢ ∃ u ∈ 𝓝ˢ[s'] s, ∃ v ∈ 𝓝ˢ[t'] t, u ×ˢ v ⊆ n

Tactic:
rwa [hs.nhdsSetWithin_prod_eq ht, Filter.mem_prod_iff] at hn

Premises used: IsCompact.nhdsSetWithin_prod_eq, Filter.mem_prod_iff
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s s' : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : n ∈ 𝓝ˢ[s' ×ˢ t] (s ×ˢ t)
⊢ {a : X | ∀ b ∈ t, (a, b) ∈ n} ∈ 𝓝ˢ[s'] s

Tactic:
rw [hs.nhdsSetWithin_prod_eq ht, nhdsSetWithin_self, Filter.mem_prod_principal] at hn

Premises used: IsCompact.nhdsSetWithin_prod_eq, Filter.mem_prod_principal, nhdsSetWithin_self
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s s' : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : {a : X | ∀ b ∈ t, (a, b) ∈ n} ∈ 𝓝ˢ[s'] s
⊢ ∃ u ∈ 𝓝ˢ[s'] s, u ×ˢ t ⊆ n

Tactic:
⟨_, hn, fun x hx ↦ hx.1 _ hx.2⟩

Premises used: And.right, And.left, And.intro, Exists.intro, Prod.snd
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s s' : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : {a : X | ∀ b ∈ t, (a, b) ∈ n} ∈ 𝓝ˢ[s'] s
⊢ ∃ u ∈ 𝓝ˢ[s'] s, u ×ˢ t ⊆ n

Tactic:
exact ⟨_, hn, fun x hx ↦ hx.1 _ hx.2⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : n ∈ 𝓝ˢ[s ×ˢ t'] (s ×ˢ t)
⊢ ∃ t₁ ∈ 𝓟 s, ∃ t₂ ∈ 𝓝ˢ[t'] t, t₁ ×ˢ t₂ ⊆ n

Tactic:
rw [hs.nhdsSetWithin_prod_eq ht, nhdsSetWithin_self, Filter.mem_prod_iff] at hn

Premises used: IsCompact.nhdsSetWithin_prod_eq, nhdsSetWithin_self, Filter.mem_prod_iff
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : ∃ t₁ ∈ 𝓟 s, ∃ t₂ ∈ 𝓝ˢ[t'] t, t₁ ×ˢ t₂ ⊆ n
obtain : ∀ (s' : Set X) (hs' : s' ∈ 𝓟 s) (u : Set Y) (hu : u ∈ 𝓝ˢ[t'] t) (h : s' ×ˢ u ⊆ n), ∃ u ∈ 𝓝ˢ[t'] t, s ×ˢ u ⊆ n
⊢ ∃ u ∈ 𝓝ˢ[t'] t, s ×ˢ u ⊆ n

Tactic:
obtain ⟨s', hs', u, hu, h⟩ := hn
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
s' : Set X
hs' : s' ∈ 𝓟 s
u : Set Y
hu : u ∈ 𝓝ˢ[t'] t
h : s' ×ˢ u ⊆ n
⊢ ∃ u ∈ 𝓝ˢ[t'] t, s ×ˢ u ⊆ n

Tactic:
⟨u, hu, (prod_mono_left hs').trans h⟩

Premises used: HasSubset.Subset.trans, Set.prod_mono_left, And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
s' : Set X
hs' : s' ∈ 𝓟 s
u : Set Y
hu : u ∈ 𝓝ˢ[t'] t
h : s' ×ˢ u ⊆ n
⊢ ∃ u ∈ 𝓝ˢ[t'] t, s ×ˢ u ⊆ n

Tactic:
exact ⟨u, hu, (prod_mono_left hs').trans h⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : Subsingleton X
⊢ CompactSpace X

Tactic:
⟨subsingleton_univ.isCompact⟩

Premises used: Set.subsingleton_univ, CompactSpace.mk, Set.Subsingleton.isCompact
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsCompact.{u} (X := X) univ ↔ CompactSpace X

Tactic:
⟨fun h => ⟨h⟩, fun h => h.1⟩

Premises used: CompactSpace.isCompact_univ, CompactSpace.mk, Iff.intro
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
h : CompactSpace X
⊢ IsCompact.{u} (X := X) univ

Tactic:
h.isCompact_univ

Premises used: CompactSpace.isCompact_univ
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
f : Filter X
inst_2 : f.NeBot
⊢ f ≤ 𝓟 univ

Tactic:
simp
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
f : Filter X
inst_2 : f.NeBot
⊢ ∃ (x : X), ClusterPt x f

Tactic:
simpa using isCompact_univ (show f ≤ 𝓟 univ by simp)

Premises used: isCompact_univ
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
F : Ultrafilter X
⊢ (↑F : Filter X) ≤ 𝓟 univ

Tactic:
simp
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
⊢ ∃ (t : Finset X), Eq.{u + 1} (α := Set X) (⋃ x ∈ t, U x) ⊤

Tactic:
have ⟨t, _, s⟩ := IsCompact.elim_nhds_subcover isCompact_univ U fun x _ => hU x
  ⟨t, top_unique s⟩

Premises used: CompactSpace.isCompact_univ, Exists, IsCompact.elim_nhds_subcover, top_unique, _private.0.CompactSpace.elim_nhds_subcover.match_1, Exists.intro, Top.top, Eq, Set.iUnion
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst] (t i)) →
      Eq.{u + 1} (α := Set X) (⋂ (i : ι), t i) ∅ → ∃ (u : Finset ι), Eq.{u + 1} (α := Set X) (⋂ i ∈ u, t i) ∅
ι : Type u
t : ι → Set X
⊢ (∀ (i : ι), IsClosed[inst] (t i)) →
    Eq.{u + 1} (α := Set X) (univ ∩ ⋂ (i : ι), t i) ∅ →
      ∃ (u : Finset ι), Eq.{u + 1} (α := Set X) (univ ∩ ⋂ i ∈ u, t i) ∅

Tactic:
simpa using h t
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type v
inst_1 : CompactSpace X
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : ∀ (s : Finset ι), Set.Nonempty.{u} (α := X) (⋂ i ∈ s, t i)
⊢ ∀ (u : Finset ι), Set.Nonempty.{u} (α := X) (univ ∩ ⋂ i ∈ u, t i)

Tactic:
simpa using hst
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type v
inst_1 : CompactSpace X
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : ∀ (s : Finset ι), Set.Nonempty.{u} (α := X) (⋂ i ∈ s, t i)
⊢ Set.Nonempty.{u} (α := X) (⋂ (i : ι), t i)

Tactic:
simpa using isCompact_univ.inter_iInter_nonempty t htc (by simpa using hst)

Premises used: CompactSpace.isCompact_univ, IsCompact.inter_iInter_nonempty
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
h : ∀ P ⊆ S, ⋃₀ P = univ → ∃ Q ⊆ P, Q.Finite ∧ ⋃₀ Q = univ
⊢ ∀ P ⊆ S, univ ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ univ ⊆ ⋃₀ Q

Tactic:
simpa
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
h :
  ∀ (ι : Type u) (U : ι → (↑S : Type u)),
    Eq.{u + 1} (α := Set X) (⋃ (i : ι), (↑(U i) : Set X)) univ →
      ∃ (J : Set ι), J.Finite ∧ Eq.{u + 1} (α := Set X) (⋃ i ∈ J, (↑(U i) : Set X)) univ
⊢ ∀ (ι : Type u) (U : ι → (↑S : Type u)),
    Subset.{u} (α := Set X) univ (⋃ (i : ι), (↑(U i) : Set X)) →
      ∃ (J : Set ι), J.Finite ∧ Subset.{u} (α := Set X) univ (⋃ i ∈ J, (↑(U i) : Set X))

Tactic:
simpa
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
⊢ CompactSpace X

Tactic:
compactSpace_generateFrom hT fun P hP𝔅 hP ↦ ?_

Premises used: compactSpace_generateFrom
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
refine : ∀ (P : Set (Set X)) (hP𝔅 : P ⊆ 𝔅) (hP : ⋃₀ P = univ), ∃ Q ⊆ P, Q.Finite ∧ ⋃₀ Q = univ
⊢ CompactSpace X

Tactic:
refine compactSpace_generateFrom hT fun P hP𝔅 hP ↦ ?_

Premises used: compactSpace_generateFrom
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ⋃₀ P = univ
contrapose! : ∀ (hP : ∀ (Q : Set (Set X)) (_ : Q ⊆ P) (_ : Q.Finite), ⋃₀ Q ≠ univ), ⋃₀ P ≠ univ
⊢ ∃ Q ⊆ P, Q.Finite ∧ ⋃₀ Q = univ

Tactic:
contrapose! hP
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ (Q : Set (Set X)) (_ : Q ⊆ P) (_ : Q.Finite), ⋃₀ Q ≠ univ
simp_rw :
  ∀ (hP : ∀ (Q : Set (Set X)) (_ : Q ⊆ P) (_ : Q.Finite), (⋂₀ (compl '' Q)).Nonempty), (⋂₀ (compl '' P)).Nonempty
⊢ ⋃₀ P ≠ univ

Tactic:
simp_rw [← Set.nonempty_compl, Set.compl_sUnion] at hP ⊢

Premises used: Set.compl_sUnion, Set.nonempty_compl
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ (Q : Set (Set X)) (_ : Q ⊆ P) (_ : Q.Finite), (⋂₀ (compl '' Q)).Nonempty
⊢ (⋂₀ (compl '' P)).Nonempty

Tactic:
h _ ?_ fun Q hQP hQ ↦ ?_
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ (Q : Set (Set X)) (_ : Q ⊆ P) (_ : Q.Finite), (⋂₀ (compl '' Q)).Nonempty
refine_1 : compl '' P ⊆ 𝔅
refine_2 : ∀ (Q : Set (Set X)) (hQP : Q ⊆ compl '' P) (hQ : Q.Finite), (⋂₀ Q).Nonempty
⊢ (⋂₀ (compl '' P)).Nonempty

Tactic:
refine h _ ?_ fun Q hQP hQ ↦ ?_
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ (Q : Set (Set X)) (_ : Q ⊆ P) (_ : Q.Finite), (⋂₀ (compl '' Q)).Nonempty
S : Set X
hS : S ∈ P
⊢ Sᶜ ∈ 𝔅

Tactic:
h𝔅 _ (hP𝔅 hS)
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ (Q : Set (Set X)) (_ : Q ⊆ P) (_ : Q.Finite), (⋂₀ (compl '' Q)).Nonempty
S : Set X
hS : S ∈ P
⊢ Sᶜ ∈ 𝔅

Tactic:
exact h𝔅 _ (hP𝔅 hS)
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ (Q : Set (Set X)) (_ : Q ⊆ P) (_ : Q.Finite), (⋂₀ (compl '' Q)).Nonempty
Q : Set (Set X)
hQP : Q ⊆ compl '' P
hQ : Q.Finite
⊢ Q ⊆ compl '' P → (compl '' Q).Finite → (⋂₀ Q).Nonempty

Tactic:
simpa [← compl_involutive.image_eq_preimage_symm] using hP (compl '' Q)

Premises used: Compl.compl, compl_involutive, Set.image, Function.Involutive.image_eq_preimage_symm
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ (Q : Set (Set X)) (_ : Q ⊆ P) (_ : Q.Finite), (⋂₀ (compl '' Q)).Nonempty
Q : Set (Set X)
hQP : Q ⊆ compl '' P
hQ : Q.Finite
⊢ Q ⊆ compl '' P → (compl '' Q).Finite → (⋂₀ Q).Nonempty

Tactic:
replace hP : Q ⊆ compl '' P → (compl '' Q).Finite → (⋂₀ Q).Nonempty := by
      simpa [← compl_involutive.image_eq_preimage_symm] using hP (compl '' Q)
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
Q : Set (Set X)
hQP : Q ⊆ compl '' P
hQ : Q.Finite
hP : Q ⊆ compl '' P → (compl '' Q).Finite → (⋂₀ Q).Nonempty
⊢ (⋂₀ Q).Nonempty

Tactic:
hP hQP (hQ.image _)

Premises used: Set.Finite.image
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
Q : Set (Set X)
hQP : Q ⊆ compl '' P
hQ : Q.Finite
hP : Q ⊆ compl '' P → (compl '' Q).Finite → (⋂₀ Q).Nonempty
⊢ (⋂₀ Q).Nonempty

Tactic:
exact hP hQP (hQ.image _)

Premises used: Set.Finite.image
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : CompactSpace X
h : IsClosed[inst] s
⊢ IsCompact s

Tactic:
isCompact_univ.of_isClosed_subset h (subset_univ _)

Premises used: Set.subset_univ, IsCompact.of_isClosed_subset, isCompact_univ
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
l : Filter X
y : X
h : ∀ (x : X), ClusterPt x l → x = y
⊢ l ≤ 𝓝 y

Tactic:
isCompact_univ.le_nhds_of_unique_clusterPt univ_mem fun x _ ↦ h x

Premises used: isCompact_univ, Filter.univ_mem, IsCompact.le_nhds_of_unique_clusterPt
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
Y : Type u_2
l : Filter Y
y : X
f : Y → X
h : ∀ (x : X), MapClusterPt x l f → x = y
⊢ Tendsto f l (𝓝 y)

Tactic:
le_nhds_of_unique_clusterPt h

Premises used: Filter.Tendsto, le_nhds_of_unique_clusterPt
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : NoncompactSpace X
⊢ ¬IsCompact.{u_2} (X := X) univ

Tactic:
NoncompactSpace.noncompact_univ

Premises used: NoncompactSpace.noncompact_univ
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : NoncompactSpace X
hs : IsCompact s
⊢ s ≠ univ

Tactic:
fun h =>
  noncompact_univ X (h ▸ hs)

Premises used: noncompact_univ, Eq.rec, Not
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : NoncompactSpace X
⊢ (cocompact X).NeBot

Tactic:
Filter.hasBasis_cocompact.neBot_iff.2 fun hs => ?_

Premises used: Iff.mpr, Filter.HasBasis.neBot_iff, Filter.hasBasis_cocompact
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : NoncompactSpace X
refine : ∀ {i : Set X} (hs : IsCompact i), iᶜ.Nonempty
⊢ (cocompact X).NeBot

Tactic:
refine Filter.hasBasis_cocompact.neBot_iff.2 fun hs => ?_

Premises used: Iff.mpr, Filter.HasBasis.neBot_iff, Filter.hasBasis_cocompact
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : NoncompactSpace X
i : Set X
hs : IsCompact i
contrapose : ∀ (hs : ¬iᶜ.Nonempty), ¬IsCompact i
⊢ iᶜ.Nonempty

Tactic:
contrapose hs
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : NoncompactSpace X
i : Set X
hs : ¬iᶜ.Nonempty
⊢ i = univ

Tactic:
rw [not_nonempty_iff_eq_empty, compl_empty_iff] at hs

Premises used: Set.not_nonempty_iff_eq_empty, Set.compl_empty_iff
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : NoncompactSpace X
i : Set X
hs : i = univ
rw : ¬IsCompact.{u} (X := X) univ
⊢ ¬IsCompact i

Tactic:
rw [hs]