awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs_1 : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set (↑s : Type u)
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, (fun (x : (↑s : Type u)) ↦ interior (U (↑x : X) ⋯)) i
right :
  ∀ (i : (↑s : Type u)) (j : i ∈ r),
    Subset.{u} (α := Set X) ((fun (x : (↑s : Type u)) ↦ interior (U (↑x : X) ⋯)) i) (⋃ x ∈ r, U (↑x : X) ⋯)
⊢ Subset.{u} (α := Set X) (⋃ i ∈ r, (fun (x : (↑s : Type u)) ↦ interior (U (↑x : X) ⋯)) i) (⋃ x ∈ r, U (↑x : X) ⋯)

Tactic:
apply iUnion₂_subset

Premises used: Set.iUnion₂_subset
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs_1 : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set (↑s : Type u)
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, (fun (x : (↑s : Type u)) ↦ interior (U (↑x : X) ⋯)) i
i : (↑s : Type u)
hi : i ∈ r
right : U (↑i : X) ⋯ ⊆ ⋃ x ∈ r, U (↑x : X) ⋯
⊢ Subset.{u} (α := Set X) ((fun (x : (↑s : Type u)) ↦ interior (U (↑x : X) ⋯)) i) (⋃ x ∈ r, U (↑x : X) ⋯)

Tactic:
apply Subset.trans interior_subset

Premises used: interior_subset, Set.Subset.trans
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs_1 : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set (↑s : Type u)
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, (fun (x : (↑s : Type u)) ↦ interior (U (↑x : X) ⋯)) i
i : (↑s : Type u)
hi : i ∈ r
⊢ U (↑i : X) ⋯ ⊆ ⋃ x ∈ r, U (↑x : X) ⋯

Tactic:
subset_iUnion_of_subset i (subset_iUnion_of_subset hi (Subset.refl _))

Premises used: Set.Subset.refl, Set.subset_iUnion_of_subset
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs_1 : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set (↑s : Type u)
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, (fun (x : (↑s : Type u)) ↦ interior (U (↑x : X) ⋯)) i
i : (↑s : Type u)
hi : i ∈ r
⊢ U (↑i : X) ⋯ ⊆ ⋃ x ∈ r, U (↑x : X) ⋯

Tactic:
exact subset_iUnion_of_subset i (subset_iUnion_of_subset hi (Subset.refl _))

Premises used: Set.subset_iUnion_of_subset
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
let :
  ∀ (t : Set (↑s : Type u)) (htc : t.Countable) (htsub : s ⊆ ⋃ x ∈ t, U (↑x : X)),
    ∃ (t : Set X), t.Countable ∧ (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x
⊢ ∃ (t : Set X), t.Countable ∧ (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x

Tactic:
let ⟨t, ⟨htc, htsub⟩⟩ := hs.elim_nhds_subcover' (fun x _ ↦ U x) hU
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set (↑s : Type u)
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U (↑x : X)
⊢ ∃ (t : Set X), t.Countable ∧ (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x

Tactic:
⟨↑t, Countable.image htc Subtype.val, ?_⟩

Premises used: Set.Countable.image, And.intro, Exists.intro, Set.image, Subtype.val
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set (↑s : Type u)
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U (↑x : X)
refine :
  (∀ x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t, x ∈ s) ∧
    s ⊆ ⋃ x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t, U x
⊢ ∃ (t : Set X), t.Countable ∧ (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x

Tactic:
refine ⟨↑t, Countable.image htc Subtype.val, ?_⟩
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set (↑s : Type u)
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U (↑x : X)
left : ∀ x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t, x ∈ s
right : s ⊆ ⋃ x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t, U x
⊢ (∀ x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t, x ∈ s) ∧
    s ⊆ ⋃ x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t, U x

Tactic:
constructor
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set (↑s : Type u)
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U (↑x : X)
x : X
left : ∀ (x_1 : x ∈ s) (h : Subtype.mk (p := fun (a : X) ↦ a ∈ s) x ⋯ ∈ t), x ∈ s
⊢ x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t → x ∈ s

Tactic:
simp only [mem_image, Subtype.exists, exists_and_right, exists_eq_right, forall_exists_index]

Premises used: Set.mem_image, Subtype.exists, forall_exists_index, exists_eq_right, exists_and_right
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set (↑s : Type u)
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U (↑x : X)
x : X
left left₁ left₂ : ∀ (x_1 : x ∈ s), Subtype.mk (p := fun (a : X) ↦ a ∈ s) x ⋯ ∈ t → x ∈ s
⊢ ∀ (x_1 : x ∈ s) (h : Subtype.mk (p := fun (a : X) ↦ a ∈ s) x ⋯ ∈ t), x ∈ s

Tactic:
tauto
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set (↑s : Type u)
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U (↑x : X)
⊢ Eq.{u + 1} (α := Set X) (⋃ x ∈ t, U (↑x : X)) (⋃ x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t, U x)

Tactic:
have : ⋃ x ∈ t, U ↑x = ⋃ x ∈ Subtype.val '' t, U x := biUnion_image.symm
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set (↑s : Type u)
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U (↑x : X)
this : Eq.{u + 1} (α := Set X) (⋃ x ∈ t, U (↑x : X)) (⋃ x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t, U x)
right right₁ right₂ right₃ : s ⊆ ⋃ x ∈ t, U (↑x : X)
⊢ s ⊆ ⋃ x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t, U x

Tactic:
rwa [← this]
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
inst_1 : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
obtain : ∀ (c : Set ι) (c_count : c.Countable) (c_cov : s ⊆ ⋃ i ∈ c, U i), ∃ (f : ℕ → ι), s ⊆ ⋃ (n : ℕ), U (f n)
⊢ ∃ (f : ℕ → ι), s ⊆ ⋃ (n : ℕ), U (f n)

Tactic:
obtain ⟨c, ⟨c_count, c_cov⟩⟩ := hs.elim_countable_subcover U hUo hsU

Premises used: IsLindelof.elim_countable_subcover
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
inst_1 : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
c : Set ι
c_count : c.Countable
c_cov : s ⊆ ⋃ i ∈ c, U i
inl :
  ∀ (c_count : Set.Countable.{v} (α := ι) ∅) (c_cov : s ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ i), U i),
    ∃ (f : ℕ → ι), s ⊆ ⋃ (n : ℕ), U (f n)
inr : ∀ (c_nonempty : c.Nonempty), ∃ (f : ℕ → ι), s ⊆ ⋃ (n : ℕ), U (f n)
⊢ ∃ (f : ℕ → ι), s ⊆ ⋃ (n : ℕ), U (f n)

Tactic:
rcases c.eq_empty_or_nonempty with rfl | c_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
inst_1 : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
c_count : Set.Countable.{v} (α := ι) ∅
c_cov : s ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ i), U i
⊢ s ⊆ ∅

Tactic:
simp only [mem_empty_iff_false, iUnion_of_empty, iUnion_empty] at c_cov

Premises used: Set.iUnion_of_empty, Set.mem_empty_iff_false, Set.iUnion_empty
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
inst_1 : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
c_count : Set.Countable.{v} (α := ι) ∅
c_cov : s ⊆ ∅
⊢ ∃ (f : ℕ → ι), s ⊆ ⋃ (n : ℕ), U (f n)

Tactic:
simp only [subset_eq_empty c_cov rfl, empty_subset, exists_const]

Premises used: Set.empty_subset, exists_const, rfl, Set.subset_eq_empty
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
inst_1 : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
c : Set ι
c_count : c.Countable
c_cov : s ⊆ ⋃ i ∈ c, U i
c_nonempty : c.Nonempty
inr : ∀ (f : ℕ → (↑c : Type v)) (f_surj : Function.Surjective f), ∃ (f : ℕ → ι), s ⊆ ⋃ (n : ℕ), U (f n)
⊢ ∃ (f : ℕ → ι), s ⊆ ⋃ (n : ℕ), U (f n)

Tactic:
obtain ⟨f, f_surj⟩ := (Set.countable_iff_exists_surjective c_nonempty).mp c_count

Premises used: Set.countable_iff_exists_surjective, Iff.mp
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
inst_1 : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
c : Set ι
c_count : c.Countable
c_cov : s ⊆ ⋃ i ∈ c, U i
c_nonempty : c.Nonempty
f : ℕ → (↑c : Type v)
f_surj : Function.Surjective f
⊢ ∃ (f : ℕ → ι), s ⊆ ⋃ (n : ℕ), U (f n)

Tactic:
⟨fun x ↦ f x, c_cov.trans <| iUnion₂_subset_iff.mpr (?_ : ∀ i ∈ c, U i ⊆ ⋃ n, U (f n))⟩

Premises used: Iff.mpr, HasSubset.Subset.trans, Exists.intro, Set.iUnion₂_subset_iff, Subtype.val
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
inst_1 : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
c : Set ι
c_count : c.Countable
c_cov : s ⊆ ⋃ i ∈ c, U i
c_nonempty : c.Nonempty
f : ℕ → (↑c : Type v)
f_surj : Function.Surjective f
inr : ∀ i ∈ c, U i ⊆ ⋃ (n : ℕ), U (↑(f n) : ι)
⊢ ∃ (f : ℕ → ι), s ⊆ ⋃ (n : ℕ), U (f n)

Tactic:
refine ⟨fun x ↦ f x, c_cov.trans <| iUnion₂_subset_iff.mpr (?_ : ∀ i ∈ c, U i ⊆ ⋃ n, U (f n))⟩
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
inst_1 : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
c : Set ι
c_count : c.Countable
c_cov : s ⊆ ⋃ i ∈ c, U i
c_nonempty : c.Nonempty
f : ℕ → (↑c : Type v)
f_surj : Function.Surjective f
x : ι
hx : x ∈ c
inr : ∀ (n : ℕ) (hn : f n = Subtype.mk (p := fun (x : ι) ↦ x ∈ c) x hx), U x ⊆ ⋃ (n : ℕ), U (↑(f n) : ι)
⊢ U x ⊆ ⋃ (n : ℕ), U (↑(f n) : ι)

Tactic:
obtain ⟨n, hn⟩ := f_surj ⟨x, hx⟩

Premises used: Subtype.mk
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
inst_1 : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
c : Set ι
c_count : c.Countable
c_cov : s ⊆ ⋃ i ∈ c, U i
c_nonempty : c.Nonempty
f : ℕ → (↑c : Type v)
f_surj : Function.Surjective f
x : ι
hx : x ∈ c
n : ℕ
hn : f n = Subtype.mk (p := fun (x : ι) ↦ x ∈ c) x hx
rw rw₁ : U x = U (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ c) x hx) : ι)
⊢ U x = U (↑(f n) : ι)

Tactic:
rw [hn]
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
inst_1 : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
c : Set ι
c_count : c.Countable
c_cov : s ⊆ ⋃ i ∈ c, U i
c_nonempty : c.Nonempty
f : ℕ → (↑c : Type v)
f_surj : Function.Surjective f
x : ι
hx : x ∈ c
n : ℕ
hn : f n = Subtype.mk (p := fun (x : ι) ↦ x ∈ c) x hx
⊢ U x ⊆ ⋃ (n : ℕ), U (↑(f n) : ι)

Tactic:
exact subset_iUnion_of_subset n <| subset_of_eq (by rw [hn])

Premises used: Set.subset_iUnion_of_subset, subset_of_eq
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
inst_1 : CountableInterFilter l
hs : IsLindelof s
⊢ Disjoint (𝓝ˢ s) l ↔ ∀ x ∈ s, Disjoint (𝓝 x) l

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

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

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

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

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

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

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

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

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

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

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

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

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

Tactic:
rw [compl_iUnion₂]

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

Tactic:
(countable_bInter_mem htc).mpr (fun i hi ↦ hUl _ (hts _ hi))

Premises used: countable_bInter_mem, Iff.mpr
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
inst_1 : CountableInterFilter l
hs : IsLindelof s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : (x : X) → Set X
hUl : ∀ (x : X) (hx : x ∈ s), (U x)ᶜ ∈ l
hxU : ∀ (x : X) (hx : x ∈ s), x ∈ U x
hUo : ∀ (x : X) (hx : x ∈ s), IsOpen[inst] (U x)
t : Set X
htc : t.Countable
hts : ∀ x ∈ t, x ∈ s
hst : s ⊆ ⋃ x ∈ t, U x
⊢ ⋂ i ∈ t, (U i)ᶜ ∈ l

Tactic:
exact (countable_bInter_mem htc).mpr (fun i hi ↦ hUl _ (hts _ hi))

Premises used: countable_bInter_mem, Iff.mpr
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
inst_1 : CountableInterFilter l
hs : IsLindelof s
⊢ Disjoint l (𝓝ˢ s) ↔ ∀ x ∈ s, Disjoint l (𝓝 x)

Tactic:
simpa only [disjoint_comm] using hs.disjoint_nhdsSet_left

Premises used: IsLindelof.disjoint_nhdsSet_left, disjoint_comm
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : s ∩ ⋂ (i : ι), t i = ∅
U : ι → Set X := tᶜ
simp : ∀ (i : ι), IsClosed[inst] (t i)
⊢ ∀ (i : ι), IsOpen[inst] (U i)

Tactic:
simp only [U, Pi.compl_apply, isOpen_compl_iff]

Premises used: Pi.compl_apply, isOpen_compl_iff
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : s ∩ ⋂ (i : ι), t i = ∅
U : ι → Set X := tᶜ
⊢ ∀ (i : ι), IsClosed[inst] (t i)

Tactic:
htc
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : s ∩ ⋂ (i : ι), t i = ∅
U : ι → Set X := tᶜ
⊢ ∀ (i : ι), IsClosed[inst] (t i)

Tactic:
exact htc
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : s ∩ ⋂ (i : ι), t i = ∅
U : ι → Set X := tᶜ
⊢ ∀ (i : ι), IsOpen[inst] (U i)

Tactic:
have hUo : ∀ i, IsOpen (U i) := by simp only [U, Pi.compl_apply, isOpen_compl_iff]; exact htc
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : s ∩ ⋂ (i : ι), t i = ∅
U : ι → Set X := tᶜ
hUo : ∀ (i : ι), IsOpen[inst] (U i)
simp : s ⊆ ⋃ (i : ι), (t i)ᶜ
⊢ s ⊆ ⋃ (i : ι), U i

Tactic:
simp only [U, Pi.compl_apply]

Premises used: Pi.compl_apply
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : s ∩ ⋂ (i : ι), t i = ∅
U : ι → Set X := tᶜ
hUo : ∀ (i : ι), IsOpen[inst] (U i)
rw : s ⊆ (⋂ (i : ι), t i)ᶜ
⊢ s ⊆ ⋃ (i : ι), (t i)ᶜ

Tactic:
rw [← compl_iInter]

Premises used: Set.compl_iInter
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : s ∩ ⋂ (i : ι), t i = ∅
U : ι → Set X := tᶜ
hUo : ∀ (i : ι), IsOpen[inst] (U i)
apply : Disjoint (⋂ (i : ι), t i)ᶜᶜ s
⊢ s ⊆ (⋂ (i : ι), t i)ᶜ

Tactic:
apply disjoint_compl_left_iff_subset.mp

Premises used: Set.disjoint_compl_left_iff_subset, Iff.mp
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : s ∩ ⋂ (i : ι), t i = ∅
U : ι → Set X := tᶜ
hUo : ∀ (i : ι), IsOpen[inst] (U i)
simp : Disjoint (⋂ (i : ι), t i) s
⊢ Disjoint (⋂ (i : ι), t i)ᶜᶜ s

Tactic:
simp only [compl_iInter, compl_iUnion, compl_compl]

Premises used: Set.compl_iInter, compl_compl, Set.compl_iUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : s ∩ ⋂ (i : ι), t i = ∅
U : ι → Set X := tᶜ
hUo : ∀ (i : ι), IsOpen[inst] (U i)
a : Disjoint s (⋂ (i : ι), t i)
⊢ Disjoint (⋂ (i : ι), t i) s

Tactic:
apply Disjoint.symm

Premises used: Disjoint.symm
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : s ∩ ⋂ (i : ι), t i = ∅
U : ι → Set X := tᶜ
hUo : ∀ (i : ι), IsOpen[inst] (U i)
⊢ Disjoint s (⋂ (i : ι), t i)

Tactic:
disjoint_iff_inter_eq_empty.mpr hst

Premises used: Iff.mpr, Set.disjoint_iff_inter_eq_empty
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : s ∩ ⋂ (i : ι), t i = ∅
U : ι → Set X := tᶜ
hUo : ∀ (i : ι), IsOpen[inst] (U i)
⊢ Disjoint s (⋂ (i : ι), t i)

Tactic:
exact disjoint_iff_inter_eq_empty.mpr hst

Premises used: Iff.mpr, Set.disjoint_iff_inter_eq_empty
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : s ∩ ⋂ (i : ι), t i = ∅
U : ι → Set X := tᶜ
hUo : ∀ (i : ι), IsOpen[inst] (U i)
⊢ s ⊆ ⋃ (i : ι), U i

Tactic:
have hsU : s ⊆ ⋃ i, U i := by
    simp only [U, Pi.compl_apply]
    rw [← compl_iInter]
    apply disjoint_compl_left_iff_subset.mp
    simp only [compl_iInter, compl_iUnion, compl_compl]
    apply Disjoint.symm
    exact disjoint_iff_inter_eq_empty.mpr hst
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : s ∩ ⋂ (i : ι), t i = ∅
U : ι → Set X := tᶜ
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
rcases :
  ∀ (u : Set ι) (hucount : u.Countable) (husub : s ⊆ ⋃ i ∈ u, U i), ∃ (u : Set ι), u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
⊢ ∃ (u : Set ι), u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅

Tactic:
rcases hs.elim_countable_subcover U hUo hsU with ⟨u, ⟨hucount, husub⟩⟩

Premises used: IsLindelof.elim_countable_subcover
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : s ∩ ⋂ (i : ι), t i = ∅
U : ι → Set X := tᶜ
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
u : Set ι
hucount : u.Countable
husub : s ⊆ ⋃ i ∈ u, U i
right : s ∩ ⋂ i ∈ u, t i = ∅
⊢ ∃ (u : Set ι), u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅

Tactic:
use u, hucount
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : s ∩ ⋂ (i : ι), t i = ∅
U : ι → Set X := tᶜ
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
u : Set ι
hucount : u.Countable
husub : s ⊆ ⋃ i ∈ u, U i
⊢ Disjoint (⋃ i ∈ u, U i)ᶜ s

Tactic:
rw [← disjoint_compl_left_iff_subset] at husub

Premises used: Set.disjoint_compl_left_iff_subset