awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ s ∈ cocompact X ↔ ∃ (t : Set X), IsCompact t ∧ tᶜ ⊆ s

Tactic:
hasBasis_cocompact.mem_iff

Premises used: Filter.HasBasis.mem_iff, Filter.hasBasis_cocompact
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ s ∈ cocompact X ↔ ∃ (t : Set X), IsCompact t ∧ sᶜ ⊆ t

Tactic:
mem_cocompact.trans <| exists_congr fun _ => and_congr_right fun _ => compl_subset_comm

Premises used: Set.compl_subset_comm, and_congr_right, exists_congr, Iff.trans, Filter.mem_cocompact
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
⊢ sᶜ ∈ cocompact X

Tactic:
hasBasis_cocompact.mem_of_mem hs

Premises used: Filter.hasBasis_cocompact, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
⊢ cocompact X ≤ cofinite

Tactic:
fun s hs =>
  compl_compl s ▸ hs.isCompact.compl_mem_cocompact

Premises used: compl_compl, IsCompact.compl_mem_cocompact, Eq.rec, Set.Finite.isCompact
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
⊢ cocompact X = cofinite

Tactic:
simp only [cocompact, hasBasis_cofinite.eq_biInf, isCompact_iff_finite]

Premises used: isCompact_iff_finite, Filter.hasBasis_cofinite, Filter.HasBasis.eq_biInf, Filter.cocompact
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
f : Filter X
simp_rw : (∃ (i : Set X), IsCompact i ∧ i ∈ f) ↔ ∃ K ∈ f, IsCompact K
⊢ Disjoint (cocompact X) f ↔ ∃ K ∈ f, IsCompact K

Tactic:
simp_rw [hasBasis_cocompact.disjoint_iff_left, compl_compl]

Premises used: compl_compl, Filter.HasBasis.disjoint_iff_left, Filter.hasBasis_cocompact
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
f : Filter X
mp : (∃ (i : Set X), IsCompact i ∧ i ∈ f) → ∃ K ∈ f, IsCompact K
mpr : (∃ K ∈ f, IsCompact K) → ∃ (i : Set X), IsCompact i ∧ i ∈ f
mp₁ mp₂ mp₃ : ∀ (w : Set X), IsCompact w → w ∈ f → ∃ K ∈ f, IsCompact K
mpr₁ mpr₂ mpr₃ : ∀ w ∈ f, IsCompact w → ∃ (i : Set X), IsCompact i ∧ i ∈ f
mp₄ mp₅ mp₆ : ∀ (w : Set X), IsCompact w → w ∈ f → ∃ K ∈ f, IsCompact K
mpr₄ mpr₅ mpr₆ : ∀ w ∈ f, IsCompact w → ∃ (i : Set X), IsCompact i ∧ i ∈ f
mp₇ mp₈ : ∀ (w : Set X), IsCompact w → w ∈ f → ∃ K ∈ f, IsCompact K
mpr₇ mpr₈ : ∀ w ∈ f, IsCompact w → ∃ (i : Set X), IsCompact i ∧ i ∈ f
⊢ (∃ (i : Set X), IsCompact i ∧ i ∈ f) ↔ ∃ K ∈ f, IsCompact K

Tactic:
tauto
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
f : Filter X
simp_rw : (∃ (i : Set X), IsCompact i ∧ i ∈ f) ↔ ∃ K ∈ f, IsCompact K
⊢ Disjoint f (cocompact X) ↔ ∃ K ∈ f, IsCompact K

Tactic:
simp_rw [hasBasis_cocompact.disjoint_iff_right, compl_compl]

Premises used: compl_compl, Filter.HasBasis.disjoint_iff_right, Filter.hasBasis_cocompact
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
pos : ∀ (hy : ClusterPt y l), ∃ x ∈ insert y (range f), ClusterPt x l
neg : ∀ (hy : ¬ClusterPt y l), ∃ x ∈ insert y (range f), ClusterPt x l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l

Tactic:
by_cases hy : ClusterPt y l

Premises used: ClusterPt
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
hy : ClusterPt y l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l

Tactic:
⟨y, Or.inl rfl, hy⟩

Premises used: And.intro, Exists.intro, Or.inl, rfl
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
hy : ClusterPt y l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l

Tactic:
exact ⟨y, Or.inl rfl, hy⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
hy : ¬ClusterPt y l
⊢ ∃ (x : Set Y) (_ : x ∈ 𝓝 y) (x_1 : Set Y) (_ : x_1 ∈ l), Disjoint x x_1

Tactic:
simp only [clusterPt_iff_nonempty, not_forall, ← not_disjoint_iff_nonempty_inter, not_not] at hy

Premises used: Classical.not_not, Set.not_disjoint_iff_nonempty_inter, clusterPt_iff_nonempty, Classical.not_forall
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
hy : ∃ (x : Set Y) (_ : x ∈ 𝓝 y) (x_1 : Set Y) (_ : x_1 ∈ l), Disjoint x x_1
neg :
  ∀ (s : Set Y) (hsy : s ∈ 𝓝 y) (t : Set Y) (htl : t ∈ l) (hd : Disjoint s t), ∃ x ∈ insert y (range f), ClusterPt x l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l

Tactic:
rcases hy with ⟨s, hsy, t, htl, hd⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
neg : ∀ (K : Set X) (hKc : IsCompact K) (hKs : Kᶜ ⊆ f ⁻¹' s), ∃ x ∈ insert y (range f), ClusterPt x l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l

Tactic:
rcases mem_cocompact.1 (hf hsy) with ⟨K, hKc, hKs⟩

Premises used: Iff.mp, Filter.mem_cocompact
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
h : ∀ (y_1 : Y) (hyt : y_1 ∈ t) (hyf : y_1 ∈ insert y (range f)), y_1 ∈ f '' K
⊢ f '' K ∈ l

Tactic:
filter_upwards [htl, le_principal_iff.1 hle] with y hyt hyf

Premises used: Filter.le_principal_iff, Iff.mp
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y_1 : Y
hf : Tendsto f (cocompact X) (𝓝 y_1)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y_1 (range f))
s : Set Y
hsy : s ∈ 𝓝 y_1
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
y : Y
hyt : y ∈ t
hyf : y ∈ insert y_1 (range f)
h : ∀ (hf : Tendsto f (cocompact X) (𝓝 y)) (hle : l ≤ 𝓟 (insert y (range f))) (hsy : s ∈ 𝓝 y), y ∈ f '' K
h₁ : ∀ (x : X) (hyt : f x ∈ t), f x ∈ f '' K
⊢ y ∈ f '' K

Tactic:
rcases hyf with (rfl | ⟨x, rfl⟩)

Premises used: rfl
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
s t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
y : Y
hyt : y ∈ t
hf : Tendsto f (cocompact X) (𝓝 y)
hle : l ≤ 𝓟 (insert y (range f))
hsy : s ∈ 𝓝 y
⊢ y ∈ f '' K

Tactic:
(hd.le_bot ⟨mem_of_mem_nhds hsy, hyt⟩).elim

Premises used: Disjoint.le_bot, False.elim, mem_of_mem_nhds, And.intro
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
x : X
hyt : f x ∈ t
⊢ f x ∈ f '' K

Tactic:
mem_image_of_mem _ (not_not.1 fun hxK => hd.le_bot ⟨hKs hxK, hyt⟩)

Premises used: Disjoint.le_bot, Classical.not_not, Set.mem_image_of_mem, And.intro, Iff.mp
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
s t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
y : Y
hyt : y ∈ t
hf : Tendsto f (cocompact X) (𝓝 y)
hle : l ≤ 𝓟 (insert y (range f))
hsy : s ∈ 𝓝 y
⊢ y ∈ f '' K

Tactic:
exacts [(hd.le_bot ⟨mem_of_mem_nhds hsy, hyt⟩).elim,
      mem_image_of_mem _ (not_not.1 fun hxK => hd.le_bot ⟨hKs hxK, hyt⟩)]

Premises used: Disjoint.le_bot, False.elim, mem_of_mem_nhds, And.intro
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
⊢ f '' K ∈ l

Tactic:
have : f '' K ∈ l := by
    filter_upwards [htl, le_principal_iff.1 hle] with y hyt hyf
    rcases hyf with (rfl | ⟨x, rfl⟩)
    exacts [(hd.le_bot ⟨mem_of_mem_nhds hsy, hyt⟩).elim,
      mem_image_of_mem _ (not_not.1 fun hxK => hd.le_bot ⟨hKs hxK, hyt⟩)]
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
this : f '' K ∈ l
neg : ∀ (y_1 : Y) (hy : y_1 ∈ f '' K) (hyl : ClusterPt y_1 l), ∃ x ∈ insert y (range f), ClusterPt x l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l

Tactic:
rcases hKc.image hfc (le_principal_iff.2 this) with ⟨y, hy, hyl⟩

Premises used: Iff.mpr, Filter.le_principal_iff, IsCompact.image
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y_1 : Y
hf : Tendsto f (cocompact X) (𝓝 y_1)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y_1 (range f))
s : Set Y
hsy : s ∈ 𝓝 y_1
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
this : f '' K ∈ l
y : Y
hy : y ∈ f '' K
hyl : ClusterPt y l
⊢ ∃ x ∈ insert y_1 (range f), ClusterPt x l

Tactic:
⟨y, Or.inr <| image_subset_range _ _ hy, hyl⟩

Premises used: Set.image_subset_range, And.intro, Exists.intro, Or.inr
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y_1 : Y
hf : Tendsto f (cocompact X) (𝓝 y_1)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y_1 (range f))
s : Set Y
hsy : s ∈ 𝓝 y_1
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
this : f '' K ∈ l
y : Y
hy : y ∈ f '' K
hyl : ClusterPt y l
⊢ ∃ x ∈ insert y_1 (range f), ClusterPt x l

Tactic:
exact ⟨y, Or.inr <| image_subset_range _ _ hy, hyl⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
f : ι → X
x : X
hf : Tendsto f cofinite (𝓝 x)
this : TopologicalSpace ι := ⊥
⊢ DiscreteTopology ι

Tactic:
haveI h : DiscreteTopology ι := ⟨rfl⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
f : ι → X
x : X
hf : Tendsto f cofinite (𝓝 x)
this : TopologicalSpace ι := ⊥
h : DiscreteTopology ι
⊢ Tendsto f (cocompact ι) (𝓝 x)

Tactic:
rw [← cocompact_eq_cofinite ι] at hf

Premises used: Filter.cocompact_eq_cofinite
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
f : ι → X
x : X
hf : Tendsto f cofinite (𝓝 x)
this : TopologicalSpace ι := ⊥
h : DiscreteTopology ι
hf₁ : Tendsto f (cocompact ι) (𝓝 x)
⊢ DiscreteTopology ι

Tactic:
rw [← cocompact_eq_cofinite ι] at hf

Premises used: Filter.cocompact_eq_cofinite
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
f : ι → X
x : X
this : TopologicalSpace ι := ⊥
hf : Tendsto f (cocompact ι) (𝓝 x)
h : DiscreteTopology ι
⊢ IsCompact (insert x (range f))

Tactic:
hf.isCompact_insert_range_of_cocompact continuous_of_discreteTopology

Premises used: Filter.Tendsto.isCompact_insert_range_of_cocompact, continuous_of_discreteTopology
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
f : ι → X
x : X
this : TopologicalSpace ι := ⊥
hf : Tendsto f (cocompact ι) (𝓝 x)
h : DiscreteTopology ι
⊢ IsCompact (insert x (range f))

Tactic:
exact hf.isCompact_insert_range_of_cocompact continuous_of_discreteTopology

Premises used: Filter.Tendsto.isCompact_insert_range_of_cocompact, continuous_of_discreteTopology
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
f : ℕ → X
x : X
hf : Tendsto f atTop (𝓝 x)
⊢ IsCompact (insert x (range f))

Tactic:
Filter.Tendsto.isCompact_insert_range_of_cofinite <| Nat.cofinite_eq_atTop.symm ▸ hf

Premises used: Filter.Tendsto.isCompact_insert_range_of_cofinite, Eq.rec, Nat.cofinite_eq_atTop, Eq.symm
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
simp :
  HasBasis (⨅ (s : Set X), ⨅ (_ : IsClosed[inst] s ∧ IsCompact s), 𝓟 sᶜ)
    (fun (s : Set X) ↦ IsClosed[inst] s ∧ IsCompact s) compl
⊢ (coclosedCompact X).HasBasis (fun (s : Set X) ↦ IsClosed[inst] s ∧ IsCompact s) compl

Tactic:
simp only [Filter.coclosedCompact, iInf_and']

Premises used: Filter.coclosedCompact, iInf_and'
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
⊢ HasBasis (⨅ (s : Set X), ⨅ (_ : IsClosed[inst] s ∧ IsCompact s), 𝓟 sᶜ)
    (fun (s : Set X) ↦ IsClosed[inst] s ∧ IsCompact s) compl

Tactic:
hasBasis_biInf_principal' ?_ ⟨∅, isClosed_empty, isCompact_empty⟩

Premises used: isClosed_empty, Filter.hasBasis_biInf_principal', And.intro, Exists.intro, EmptyCollection.emptyCollection, isCompact_empty
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
refine :
  ∀ (i : Set X),
    IsClosed[inst] i ∧ IsCompact i →
      ∀ (j : Set X),
        IsClosed[inst] j ∧ IsCompact j → ∃ (k : Set X), (IsClosed[inst] k ∧ IsCompact k) ∧ kᶜ ⊆ iᶜ ∧ kᶜ ⊆ jᶜ
⊢ HasBasis (⨅ (s : Set X), ⨅ (_ : IsClosed[inst] s ∧ IsCompact s), 𝓟 sᶜ)
    (fun (s : Set X) ↦ IsClosed[inst] s ∧ IsCompact s) compl

Tactic:
refine hasBasis_biInf_principal' ?_ ⟨∅, isClosed_empty, isCompact_empty⟩

Premises used: Filter.hasBasis_biInf_principal', Exists.intro, EmptyCollection.emptyCollection
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs₁ : IsClosed[inst] s
hs₂ : IsCompact s
t : Set X
ht₁ : IsClosed[inst] t
ht₂ : IsCompact t
⊢ ∃ (k : Set X), (IsClosed[inst] k ∧ IsCompact k) ∧ kᶜ ⊆ sᶜ ∧ kᶜ ⊆ tᶜ

Tactic:
⟨s ∪ t, ⟨⟨hs₁.union ht₁, hs₂.union ht₂⟩, compl_subset_compl.2 subset_union_left,
    compl_subset_compl.2 subset_union_right⟩⟩

Premises used: Iff.mpr, IsClosed.union, Set.subset_union_right, Set.compl_subset_compl, Set.subset_union_left, And.intro, Exists.intro, IsCompact.union, Union.union
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs₁ : IsClosed[inst] s
hs₂ : IsCompact s
t : Set X
ht₁ : IsClosed[inst] t
ht₂ : IsCompact t
⊢ ∃ (k : Set X), (IsClosed[inst] k ∧ IsCompact k) ∧ kᶜ ⊆ sᶜ ∧ kᶜ ⊆ tᶜ

Tactic:
exact ⟨s ∪ t, ⟨⟨hs₁.union ht₁, hs₂.union ht₂⟩, compl_subset_compl.2 subset_union_left,
    compl_subset_compl.2 subset_union_right⟩⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ s ∈ coclosedCompact X ↔ IsCompact (closure[inst] sᶜ)

Tactic:
hasBasis_coclosedCompact.mem_iff.trans ⟨?_, fun h ↦ ?_⟩

Premises used: Filter.HasBasis.mem_iff, Filter.hasBasis_coclosedCompact, Iff.intro, Iff.trans
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
refine_1 : (∃ (i : Set X), (IsClosed[inst] i ∧ IsCompact i) ∧ iᶜ ⊆ s) → IsCompact (closure[inst] sᶜ)
refine_2 : ∀ (h : IsCompact (closure[inst] sᶜ)), ∃ (i : Set X), (IsClosed[inst] i ∧ IsCompact i) ∧ iᶜ ⊆ s
⊢ s ∈ coclosedCompact X ↔ IsCompact (closure[inst] sᶜ)

Tactic:
refine hasBasis_coclosedCompact.mem_iff.trans ⟨?_, fun h ↦ ?_⟩

Premises used: Filter.HasBasis.mem_iff, Filter.hasBasis_coclosedCompact, Iff.intro, Iff.trans
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hst : tᶜ ⊆ s
htcl : IsClosed[inst] t
htco : IsCompact t
⊢ IsCompact (closure[inst] sᶜ)

Tactic:
htco.of_isClosed_subset isClosed_closure <|
      closure_minimal (compl_subset_comm.2 hst) htcl

Premises used: Iff.mpr, closure_minimal, Set.compl_subset_comm, IsCompact.of_isClosed_subset, isClosed_closure
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hst : tᶜ ⊆ s
htcl : IsClosed[inst] t
htco : IsCompact t
⊢ IsCompact (closure[inst] sᶜ)

Tactic:
exact htco.of_isClosed_subset isClosed_closure <|
      closure_minimal (compl_subset_comm.2 hst) htcl

Premises used: Iff.mpr, closure_minimal, Set.compl_subset_comm, IsCompact.of_isClosed_subset, isClosed_closure
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : IsCompact (closure[inst] sᶜ)
⊢ ∃ (i : Set X), (IsClosed[inst] i ∧ IsCompact i) ∧ iᶜ ⊆ s

Tactic:
⟨closure sᶜ, ⟨isClosed_closure, h⟩, compl_subset_comm.2 subset_closure⟩

Premises used: Iff.mpr, subset_closure, Compl.compl, Set.compl_subset_comm, closure, And.intro, Exists.intro, isClosed_closure
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : IsCompact (closure[inst] sᶜ)
⊢ ∃ (i : Set X), (IsClosed[inst] i ∧ IsCompact i) ∧ iᶜ ⊆ s

Tactic:
exact ⟨closure sᶜ, ⟨isClosed_closure, h⟩, compl_subset_comm.2 subset_closure⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : IsCompact (closure[inst] sᶜᶜ) ↔ IsCompact (closure[inst] s)
rw₁ rw₂ : IsCompact (closure[inst] s) ↔ IsCompact (closure[inst] s)
⊢ sᶜ ∈ coclosedCompact X ↔ IsCompact (closure[inst] s)

Tactic:
rw [mem_coclosedCompact_iff, compl_compl]

Premises used: compl_compl, Filter.mem_coclosedCompact_iff
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
⊢ cocompact X ≤ coclosedCompact X

Tactic:
iInf_mono fun _ => le_iInf fun _ => le_rfl

Premises used: le_rfl, Set.Mem, le_iInf, iInf_mono
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
hs' : IsClosed[inst] s
⊢ sᶜ ∈ coclosedCompact X

Tactic:
hasBasis_coclosedCompact.mem_of_mem ⟨hs', hs⟩

Premises used: Filter.hasBasis_coclosedCompact, And.intro, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : (∃ (t : Set X), IsCompact t ∧ tᶜ ⊆ sᶜ) ↔ ∃ (t : Set X), IsCompact t ∧ s ⊆ t
⊢ sᶜ ∈ cocompact X ↔ ∃ (t : Set X), IsCompact t ∧ s ⊆ t

Tactic:
rw [Filter.mem_cocompact]

Premises used: Filter.mem_cocompact
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ (∃ (t : Set X), IsCompact t ∧ tᶜ ⊆ sᶜ) ↔ ∃ (t : Set X), IsCompact t ∧ s ⊆ t

Tactic:
simp
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Bornology Y
s : Set X
hs : IsCompact s
f : X → Y
hf : ∀ (x : X), ∃ t ∈ 𝓝 x, IsBounded (f '' t)
choose : ∀ (U : (x : X) → Set X) (hU : ∀ (x : X), U x ∈ 𝓝 x ∧ IsBounded (f '' U x)), IsBounded (f '' s)
⊢ IsBounded (f '' s)

Tactic:
choose U hU using hf
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Bornology Y
s : Set X
hs : IsCompact s
f : X → Y
U : (x : X) → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x ∧ IsBounded (f '' U x)
obtain : ∀ (I : Finset X) (hI : (∀ x ∈ I, x ∈ s) ∧ s ⊆ ⋃ x ∈ I, U x), IsBounded (f '' s)
⊢ IsBounded (f '' s)

Tactic:
obtain ⟨I, hI⟩ := hs.elim_nhds_subcover U (fun x _ => (hU x).1)

Premises used: IsCompact.elim_nhds_subcover, And.left
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Bornology Y
s : Set X
hs : IsCompact s
f : X → Y
U : (x : X) → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x ∧ IsBounded (f '' U x)
I : Finset X
hI : (∀ x ∈ I, x ∈ s) ∧ s ⊆ ⋃ x ∈ I, U x
⊢ f '' ⋃ x ∈ I, U x = ⋃ x ∈ I, f '' U x

Tactic:
simp [Set.image_iUnion₂]

Premises used: Set.image_iUnion₂
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Bornology Y
s : Set X
hs : IsCompact s
f : X → Y
U : (x : X) → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x ∧ IsBounded (f '' U x)
I : Finset X
hI : (∀ x ∈ I, x ∈ s) ∧ s ⊆ ⋃ x ∈ I, U x
⊢ f '' ⋃ x ∈ I, U x = ⋃ x ∈ I, f '' U x

Tactic:
have : f '' ⋃ x ∈ I, U x = ⋃ x ∈ I, f '' U x := by simp [Set.image_iUnion₂]
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Bornology Y
s : Set X
hs : IsCompact s
f : X → Y
U : (x : X) → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x ∧ IsBounded (f '' U x)
I : Finset X
hI : (∀ x ∈ I, x ∈ s) ∧ s ⊆ ⋃ x ∈ I, U x
this : f '' ⋃ x ∈ I, U x = ⋃ x ∈ I, f '' U x
⊢ IsBounded (f '' s)

Tactic:
((isBounded_biUnion_finset I).2 fun i _ => (hU i).2).subset (this ▸ Set.image_mono hI.2)

Premises used: Iff.mpr, Set.image_mono, Eq.rec, Bornology.isBounded_biUnion_finset, And.right, Bornology.IsBounded.subset
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Bornology Y
s : Set X
hs : IsCompact s
f : X → Y
U : (x : X) → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x ∧ IsBounded (f '' U x)
I : Finset X
hI : (∀ x ∈ I, x ∈ s) ∧ s ⊆ ⋃ x ∈ I, U x
this : f '' ⋃ x ∈ I, U x = ⋃ x ∈ I, f '' U x
⊢ IsBounded (f '' s)

Tactic:
exact ((isBounded_biUnion_finset I).2 fun i _ => (hU i).2).subset (this ▸ Set.image_mono hI.2)

Premises used: Iff.mpr, Bornology.isBounded_biUnion_finset, And.right, Bornology.IsBounded.subset
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : IsCompact s
ht : IsCompact t
simp_rw : 𝓝ˢ (s ×ˢ t) = ⨆ x ∈ s, 𝓝 x ×ˢ 𝓝ˢ t
simp_rw₁ : 𝓝ˢ (s ×ˢ t) = ⨆ x ∈ s, ⨆ y ∈ t, 𝓝 x ×ˢ 𝓝 y
simp_rw₂ : sSup (𝓝 '' s ×ˢ t) = ⨆ x ∈ s, ⨆ y ∈ t, 𝓝 x ×ˢ 𝓝 y
simp_rw₃ : Eq (α := Filter (X × Y)) (⨆ a ∈ s ×ˢ t, 𝓝 a) (⨆ x ∈ s, ⨆ y ∈ t, 𝓝 x ×ˢ 𝓝 y)
simp_rw₄ : Eq (α := Filter (X × Y)) (⨆ a ∈ s, ⨆ b ∈ t, 𝓝 (a, b)) (⨆ x ∈ s, ⨆ y ∈ t, 𝓝 x ×ˢ 𝓝 y)
⊢ 𝓝ˢ (s ×ˢ t) = 𝓝ˢ s ×ˢ 𝓝ˢ t

Tactic:
simp_rw [hs.nhdsSet_prod_eq_biSup, ht.prod_nhdsSet_eq_biSup, nhdsSet, sSup_image, biSup_prod,
    nhds_prod_eq]

Premises used: biSup_prod, IsCompact.prod_nhdsSet_eq_biSup, IsCompact.nhdsSet_prod_eq_biSup, sSup_image, nhds_prod_eq, 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)
obtain : ∀ (K : Set Y) (hKf : K ∈ f) (hK : IsCompact K), 𝓝ˢ s ×ˢ f ≤ 𝓝ˢ (SProd.sprod (β := Set Y) s univ)
⊢ 𝓝ˢ s ×ˢ f ≤ 𝓝ˢ (SProd.sprod (β := Set Y) s univ)

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
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 ≤ 𝓝ˢ s ×ˢ 𝓟 K

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

Premises used: Iff.mpr, Filter.le_principal_iff, Filter.prod_mono_right