awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
s : Set ι
hs : s.Countable
⊢ IsOpen[inst] (⋃ i ∈ s, b i)

Tactic:
exact isOpen_biUnion fun i _ => hb.isOpen (Set.mem_range_self _)

Premises used: Set.mem_range_self, TopologicalSpace.IsTopologicalBasis.isOpen, isOpen_biUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
⊢ (coLindelof X).HasBasis IsLindelof compl

Tactic:
hasBasis_biInf_principal'
    (fun s hs t ht =>
      ⟨s ∪ t, hs.union ht, compl_subset_compl.2 subset_union_left,
        compl_subset_compl.2 subset_union_right⟩)
    ⟨∅, isLindelof_empty⟩

Premises used: Iff.mpr, Filter.coLindelof, Set.subset_union_right, IsLindelof.union, Set.compl_subset_compl, Set.subset_union_left, isLindelof_empty, Filter.hasBasis_biInf_principal', And.intro, Exists.intro, Union.union, EmptyCollection.emptyCollection
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ s ∈ coLindelof X ↔ ∃ (t : Set X), IsLindelof t ∧ tᶜ ⊆ s

Tactic:
hasBasis_coLindelof.mem_iff

Premises used: Filter.HasBasis.mem_iff, hasBasis_coLindelof
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ s ∈ coLindelof X ↔ ∃ (t : Set X), IsLindelof t ∧ sᶜ ⊆ t

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

Premises used: Set.compl_subset_comm, mem_coLindelof, and_congr_right, exists_congr, Iff.trans
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
⊢ sᶜ ∈ coLindelof X

Tactic:
hasBasis_coLindelof.mem_of_mem hs

Premises used: hasBasis_coLindelof, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
⊢ coLindelof X ≤ cofinite

Tactic:
fun s hs =>
  compl_compl s ▸ hs.isLindelof.compl_mem_coLindelof

Premises used: compl_compl, IsLindelof.compl_mem_coLindelof, Eq.rec, Set.Finite.isLindelof
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
_ : ∀ [CountableInterFilter l], l ≤ 𝓟 (insert y (range f)) → ∃ x ∈ insert y (range f), ClusterPt x l
⊢ ∀ [CountableInterFilter l], l ≤ 𝓟 (insert y (range f)) → ∃ x ∈ insert y (range f), ClusterPt x l

Tactic:
_
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
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.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
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.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
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.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
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.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
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.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
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 : IsLindelof K) (hKs : Kᶜ ⊆ f ⁻¹' s), ∃ x ∈ insert y (range f), ClusterPt x l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l

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

Premises used: mem_coLindelof, Iff.mp
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
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 : IsLindelof 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.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y_1 : Y
hf : Tendsto f (coLindelof X) (𝓝 y_1)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
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 : IsLindelof K
hKs : Kᶜ ⊆ f ⁻¹' s
y : Y
hyt : y ∈ t
hyf : y ∈ insert y_1 (range f)
h : ∀ (hf : Tendsto f (coLindelof 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.Lindelof
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
inst_2 : CountableInterFilter l
s t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsLindelof K
hKs : Kᶜ ⊆ f ⁻¹' s
y : Y
hyt : y ∈ t
hf : Tendsto f (coLindelof 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.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
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 : IsLindelof 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.Lindelof
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
inst_2 : CountableInterFilter l
s t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsLindelof K
hKs : Kᶜ ⊆ f ⁻¹' s
y : Y
hyt : y ∈ t
hf : Tendsto f (coLindelof 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.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
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 : IsLindelof 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.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
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 : IsLindelof 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, IsLindelof.image
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y_1 : Y
hf : Tendsto f (coLindelof X) (𝓝 y_1)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
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 : IsLindelof 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.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y_1 : Y
hf : Tendsto f (coLindelof X) (𝓝 y_1)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
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 : IsLindelof 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.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
simp :
  HasBasis (⨅ (s : Set X), ⨅ (_ : IsClosed[inst] s ∧ IsLindelof s), 𝓟 sᶜ)
    (fun (s : Set X) ↦ IsClosed[inst] s ∧ IsLindelof s) compl
⊢ (coclosedLindelof X).HasBasis (fun (s : Set X) ↦ IsClosed[inst] s ∧ IsLindelof s) compl

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

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

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

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

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

Premises used: Filter.hasBasis_biInf_principal', Exists.intro, EmptyCollection.emptyCollection
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs₁ : IsClosed[inst] s
hs₂ : IsLindelof s
t : Set X
ht₁ : IsClosed[inst] t
ht₂ : IsLindelof t
⊢ ∃ (k : Set X), (IsClosed[inst] k ∧ IsLindelof 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, IsLindelof.union, Set.compl_subset_compl, Set.subset_union_left, And.intro, Exists.intro, Union.union
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs₁ : IsClosed[inst] s
hs₂ : IsLindelof s
t : Set X
ht₁ : IsClosed[inst] t
ht₂ : IsLindelof t
⊢ ∃ (k : Set X), (IsClosed[inst] k ∧ IsLindelof 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.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ s ∈ coclosedLindelof X ↔ ∃ (t : Set X), IsClosed[inst] t ∧ IsLindelof t ∧ tᶜ ⊆ s

Tactic:
simp only [hasBasis_coclosedLindelof.mem_iff, and_assoc]

Premises used: Filter.HasBasis.mem_iff, hasBasis_coclosedLindelof, and_assoc
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ s ∈ coclosedLindelof X ↔ ∃ (t : Set X), IsClosed[inst] t ∧ IsLindelof t ∧ sᶜ ⊆ t

Tactic:
simp only [mem_coclosedLindelof, compl_subset_comm]

Premises used: Set.compl_subset_comm, mem_coclosedLindelof
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
⊢ coLindelof X ≤ coclosedLindelof X

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

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

Tactic:
hasBasis_coclosedLindelof.mem_of_mem ⟨hs', hs⟩

Premises used: hasBasis_coclosedLindelof, And.intro, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : Subsingleton X
⊢ LindelofSpace X

Tactic:
⟨subsingleton_univ.isLindelof⟩

Premises used: Set.subsingleton_univ, Set.Subsingleton.isLindelof, LindelofSpace.mk
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsLindelof.{u} (X := X) univ ↔ LindelofSpace X

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

Premises used: LindelofSpace.mk, LindelofSpace.isLindelof_univ, Iff.intro
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
h : LindelofSpace X
⊢ IsLindelof.{u} (X := X) univ

Tactic:
h.isLindelof_univ

Premises used: LindelofSpace.isLindelof_univ
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : LindelofSpace X
f : Filter X
inst_2 : f.NeBot
inst_3 : CountableInterFilter f
⊢ f ≤ 𝓟 univ

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

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

Premises used: isLindelof_univ
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : LindelofSpace X
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
obtain :
  ∀ (t : Set X) (tc : t.Countable) (s : Subset.{u} (α := Set X) univ (⋃ x ∈ t, U x)),
    ∃ (t : Set X), t.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ x ∈ t, U x) univ
⊢ ∃ (t : Set X), t.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ x ∈ t, U x) univ

Tactic:
obtain ⟨t, tc, -, s⟩ := IsLindelof.elim_nhds_subcover isLindelof_univ U fun x _ => hU x

Premises used: IsLindelof.elim_nhds_subcover, LindelofSpace.isLindelof_univ
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : LindelofSpace X
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
t : Set X
tc : t.Countable
s : Subset.{u} (α := Set X) univ (⋃ x ∈ t, U x)
right : Eq.{u + 1} (α := Set X) (⋃ x ∈ t, U x) univ
⊢ ∃ (t : Set X), t.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ x ∈ t, U x) univ

Tactic:
use t, tc
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : LindelofSpace X
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
t : Set X
tc : t.Countable
s : Subset.{u} (α := Set X) univ (⋃ x ∈ t, U x)
⊢ Eq.{u + 1} (α := Set X) (⋃ x ∈ t, U x) univ

Tactic:
apply top_unique s

Premises used: top_unique
-- Module: Mathlib.Topology.Compactness.Lindelof
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 : Set ι), u.Countable ∧ 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 : Set ι), u.Countable ∧ Eq.{u + 1} (α := Set X) (univ ∩ ⋂ i ∈ u, t i) ∅

Tactic:
simpa using h t
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : LindelofSpace X
h : IsClosed[inst] s
⊢ IsLindelof s

Tactic:
isLindelof_univ.of_isClosed_subset h (subset_univ _)

Premises used: IsLindelof.of_isClosed_subset, Set.subset_univ, isLindelof_univ
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ tauto₈ tauto₉ tauto₁₀ :
  ∀ ⦃f : Filter X⦄ [f.NeBot] [CountableInterFilter f], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f
⊢ IsLindelof s

Tactic:
tauto
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsSigmaCompact s
⊢ ∃ (K : ℕ → Set X), (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ (n : ℕ), K n = s

Tactic:
rw [IsSigmaCompact] at hs

Premises used: IsSigmaCompact
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : ∃ (K : ℕ → Set X), (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ (n : ℕ), K n = s
rcases : ∀ (K : ℕ → Set X) (hc : ∀ (n : ℕ), IsCompact (K n)) (huniv : ⋃ (n : ℕ), K n = s), IsLindelof s
⊢ IsLindelof s

Tactic:
rcases hs with ⟨K, ⟨hc, huniv⟩⟩
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
K : ℕ → Set X
hc : ∀ (n : ℕ), IsCompact (K n)
huniv : ⋃ (n : ℕ), K n = s
rw : IsLindelof.{u} (X := X) (⋃ (n : ℕ), K n)
⊢ IsLindelof s

Tactic:
rw [← huniv]
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
K : ℕ → Set X
hc : ∀ (n : ℕ), IsCompact (K n)
huniv : ⋃ (n : ℕ), K n = s
⊢ ∀ (n : ℕ), IsLindelof (K n)

Tactic:
have hl : ∀ n, IsLindelof (K n) := fun n ↦ IsCompact.isLindelof (hc n)
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
K : ℕ → Set X
hc : ∀ (n : ℕ), IsCompact (K n)
huniv : ⋃ (n : ℕ), K n = s
hl : ∀ (n : ℕ), IsLindelof (K n)
⊢ IsLindelof.{u} (X := X) (⋃ (n : ℕ), K n)

Tactic:
isLindelof_iUnion hl

Premises used: isLindelof_iUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
K : ℕ → Set X
hc : ∀ (n : ℕ), IsCompact (K n)
huniv : ⋃ (n : ℕ), K n = s
hl : ∀ (n : ℕ), IsLindelof (K n)
⊢ IsLindelof.{u} (X := X) (⋃ (n : ℕ), K n)

Tactic:
exact isLindelof_iUnion hl

Premises used: isLindelof_iUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : CompactSpace X
⊢ LindelofSpace X

Tactic:
{ isLindelof_univ := isCompact_univ.isLindelof }

Premises used: isCompact_univ, LindelofSpace.mk, IsCompact.isLindelof
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : SigmaCompactSpace X
⊢ LindelofSpace X

Tactic:
{ isLindelof_univ := isSigmaCompact_univ.isLindelof }

Premises used: isSigmaCompact_univ, LindelofSpace.mk, IsSigmaCompact.isLindelof
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : NonLindelofSpace X
⊢ ¬IsLindelof.{u_2} (X := X) univ

Tactic:
NonLindelofSpace.nonLindelof_univ

Premises used: NonLindelofSpace.nonLindelof_univ
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : NonLindelofSpace X
hs : IsLindelof s
⊢ s ≠ univ

Tactic:
fun h ↦
  nonLindelof_univ X (h ▸ hs)

Premises used: Eq.rec, nonLindelof_univ, Not
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : NonLindelofSpace X
⊢ (coLindelof X).NeBot

Tactic:
hasBasis_coLindelof.neBot_iff.2 fun {s} hs => ?_

Premises used: Iff.mpr, Filter.HasBasis.neBot_iff, hasBasis_coLindelof
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : NonLindelofSpace X
refine : ∀ {s : Set X} (hs : IsLindelof s), sᶜ.Nonempty
⊢ (coLindelof X).NeBot

Tactic:
refine hasBasis_coLindelof.neBot_iff.2 fun {s} hs => ?_

Premises used: Iff.mpr, Filter.HasBasis.neBot_iff, hasBasis_coLindelof
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s_1 t : Set X
inst_2 : NonLindelofSpace X
s : Set X
hs : IsLindelof s
contrapose : ∀ (hs : ¬sᶜ.Nonempty), ¬IsLindelof s
⊢ sᶜ.Nonempty

Tactic:
contrapose hs
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s_1 t : Set X
inst_2 : NonLindelofSpace X
s : Set X
hs : ¬sᶜ.Nonempty
⊢ s = 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.Lindelof
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s_1 t : Set X
inst_2 : NonLindelofSpace X
s : Set X
hs : s = univ
rw : ¬IsLindelof.{u} (X := X) univ
⊢ ¬IsLindelof s

Tactic:
rw [hs]
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s_1 t : Set X
inst_2 : NonLindelofSpace X
s : Set X
hs : s = univ
⊢ ¬IsLindelof.{u} (X := X) univ

Tactic:
nonLindelof_univ X

Premises used: nonLindelof_univ
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s_1 t : Set X
inst_2 : NonLindelofSpace X
s : Set X
hs : s = univ
⊢ ¬IsLindelof.{u} (X := X) univ

Tactic:
exact nonLindelof_univ X

Premises used: nonLindelof_univ