awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Disjoint (⋃ i ∈ u, U i)ᶜ s
⊢ Disjoint (⋂ i ∈ u, t i) s

Tactic:
simp only [U, Pi.compl_apply, compl_iUnion, compl_compl] at husub

Premises used: compl_compl, Set.compl_iUnion, 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)
hsU : s ⊆ ⋃ (i : ι), U i
u : Set ι
hucount : u.Countable
husub : Disjoint (⋂ i ∈ u, t i) s
⊢ s ∩ ⋂ i ∈ u, t i = ∅

Tactic:
disjoint_iff_inter_eq_empty.mp (Disjoint.symm husub)

Premises used: Set.disjoint_iff_inter_eq_empty, Disjoint.symm, 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)
hsU : s ⊆ ⋃ (i : ι), U i
u : Set ι
hucount : u.Countable
husub : Disjoint (⋂ i ∈ u, t i) s
⊢ s ∩ ⋂ i ∈ u, t i = ∅

Tactic:
exact disjoint_iff_inter_eq_empty.mp (Disjoint.symm husub)

Premises used: Set.disjoint_iff_inter_eq_empty, Disjoint.symm, 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 : ∀ (u : Set ι), u.Countable ∧ (s ∩ ⋂ i ∈ u, t i).Nonempty
contrapose! : ∀ (hst : s ∩ ⋂ (i : ι), t i = ∅), ∃ (u : Set ι), ∀ (_ : u.Countable), s ∩ ⋂ i ∈ u, t i = ∅
⊢ (s ∩ ⋂ (i : ι), t i).Nonempty

Tactic:
contrapose! 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 = ∅
rcases :
  ∀ (u : Set ι),
    u.Countable → ∀ (husub : s ∩ ⋂ i ∈ u, t i = ∅), ∃ (u : Set ι), ∀ (_ : u.Countable), s ∩ ⋂ i ∈ u, t i = ∅
⊢ ∃ (u : Set ι), ∀ (_ : u.Countable), s ∩ ⋂ i ∈ u, t i = ∅

Tactic:
rcases hs.elim_countable_subfamily_closed t htc hst with ⟨u, ⟨_, husub⟩⟩

Premises used: IsLindelof.elim_countable_subfamily_closed
-- 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 ι
left : u.Countable
husub : s ∩ ⋂ i ∈ u, t i = ∅
⊢ ∃ (u : Set ι), ∀ (_ : u.Countable), s ∩ ⋂ i ∈ u, t i = ∅

Tactic:
⟨u, fun _ ↦ husub⟩

Premises used: Exists.intro
-- 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 ι
left : u.Countable
husub : s ∩ ⋂ i ∈ u, t i = ∅
⊢ ∃ (u : Set ι), ∀ (_ : u.Countable), s ∩ ⋂ i ∈ u, t i = ∅

Tactic:
exact ⟨u, fun _ ↦ husub⟩
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ i ∈ b, IsOpen[inst] (c i)
hc₂ : s ⊆ ⋃ i ∈ b, c i
⊢ ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))

Tactic:
simp only [Subtype.forall', biUnion_eq_iUnion] at hc₁ hc₂

Premises used: Set.biUnion_eq_iUnion, Subtype.forall'
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ i ∈ b, IsOpen[inst] (c i)
hc₂ : s ⊆ ⋃ i ∈ b, c i
hc₃ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))
⊢ s ⊆ ⋃ (x : (↑b : Type u_1)), c (↑x : ι)

Tactic:
simp only [Subtype.forall', biUnion_eq_iUnion] at hc₁ hc₂

Premises used: Set.biUnion_eq_iUnion, Subtype.forall'
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))
hc₂ : s ⊆ ⋃ (x : (↑b : Type u_1)), c (↑x : ι)
rcases :
  ∀ (d : Set (↑b : Type u_1)) (hd : d.Countable ∧ s ⊆ ⋃ i ∈ d, c (↑i : ι)), ∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c i
⊢ ∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c i

Tactic:
rcases hs.elim_countable_subcover (fun i ↦ c i : b → Set X) hc₁ hc₂ with ⟨d, hd⟩

Premises used: IsLindelof.elim_countable_subcover, Subtype.val
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))
hc₂ : s ⊆ ⋃ (x : (↑b : Type u_1)), c (↑x : ι)
d : Set (↑b : Type u_1)
hd : d.Countable ∧ s ⊆ ⋃ i ∈ d, c (↑i : ι)
⊢ Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' d ⊆ b

Tactic:
simp
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))
hc₂ : s ⊆ ⋃ (x : (↑b : Type u_1)), c (↑x : ι)
d : Set (↑b : Type u_1)
hd : d.Countable ∧ s ⊆ ⋃ i ∈ d, c (↑i : ι)
refine : s ⊆ ⋃ i ∈ Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' d, c i
⊢ ∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c i

Tactic:
refine ⟨Subtype.val '' d, by simp, Countable.image hd.1 Subtype.val, ?_⟩
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))
hc₂ : s ⊆ ⋃ (x : (↑b : Type u_1)), c (↑x : ι)
d : Set (↑b : Type u_1)
hd : d.Countable ∧ s ⊆ ⋃ i ∈ d, c (↑i : ι)
rw : s ⊆ ⋃ y ∈ d, c (↑y : ι)
⊢ s ⊆ ⋃ i ∈ Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' d, c i

Tactic:
rw [biUnion_image]

Premises used: Set.biUnion_image
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))
hc₂ : s ⊆ ⋃ (x : (↑b : Type u_1)), c (↑x : ι)
d : Set (↑b : Type u_1)
hd : d.Countable ∧ s ⊆ ⋃ i ∈ d, c (↑i : ι)
⊢ s ⊆ ⋃ y ∈ d, c (↑y : ι)

Tactic:
hd.2

Premises used: Set.Mem, And.right
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))
hc₂ : s ⊆ ⋃ (x : (↑b : Type u_1)), c (↑x : ι)
d : Set (↑b : Type u_1)
hd : d.Countable ∧ s ⊆ ⋃ i ∈ d, c (↑i : ι)
⊢ s ⊆ ⋃ y ∈ d, c (↑y : ι)

Tactic:
exact hd.2

Premises used: And.right
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (U : ι → Set X),
    (∀ (i : ι), IsOpen[inst] (U i)) → s ⊆ ⋃ (i : ι), U i → ∃ (t : Set ι), t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
contrapose! :
  ∀ (h : f ≤ 𝓟 s ∧ ∀ (x : X) (_ : x ∈ s), ¬ClusterPt x f),
    ∃ (ι : Type u) (U : ι → Set X),
      (∀ (i : ι), IsOpen[inst] (U i)) ∧ s ⊆ ⋃ (i : ι), U i ∧ ∀ (t : Set ι) (_ : t.Countable), ¬s ⊆ ⋃ i ∈ t, U i
⊢ f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f

Tactic:
contrapose! h
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
h : f ≤ 𝓟 s ∧ ∀ (x : X) (_ : x ∈ s), ¬ClusterPt x f
⊢ f ≤ 𝓟 s ∧ ∀ (x : (↑s : Type u)), ∃ (i : Set X), ((↑x : X) ∈ i ∧ IsOpen[inst] i) ∧ iᶜ ∈ f

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

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

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

Tactic:
⟨s, U, fun x ↦ (hU x).2, fun x hx ↦ mem_iUnion.2 ⟨⟨x, hx⟩, (hU _).1 ⟩, ?_⟩

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

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

Tactic:
have uinf := f.sets_of_superset (le_principal_iff.1 fsub) h
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
fsub : f ≤ 𝓟 s
U : (x : (↑s : Type u)) → Set X
hU : ∀ (x : (↑s : Type u)), (↑x : X) ∈ U x ∧ IsOpen[inst] (U x)
hUf : ∀ (x : (↑s : Type u)), (U x)ᶜ ∈ f
t : Set (↑s : Type u)
ht : t.Countable
h : s ⊆ ⋃ i ∈ t, U i
uinf : ⋃ i ∈ t, U i ∈ f.sets
⊢ ⋂ i ∈ t, (U i)ᶜ ∈ f

Tactic:
have uninf : ⋂ i ∈ t, (U i)ᶜ ∈ f := (countable_bInter_mem ht).mpr (fun _ _ ↦ hUf _)
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
fsub : f ≤ 𝓟 s
U : (x : (↑s : Type u)) → Set X
hU : ∀ (x : (↑s : Type u)), (↑x : X) ∈ U x ∧ IsOpen[inst] (U x)
hUf : ∀ (x : (↑s : Type u)), (U x)ᶜ ∈ f
t : Set (↑s : Type u)
ht : t.Countable
h : s ⊆ ⋃ i ∈ t, U i
uinf : ⋃ i ∈ t, U i ∈ f.sets
uninf : ⋂ i ∈ t, (U i)ᶜ ∈ f
⊢ (⋃ i ∈ t, U i)ᶜ ∈ f

Tactic:
rw [← compl_iUnion₂] at uninf

Premises used: Set.compl_iUnion₂
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
fsub : f ≤ 𝓟 s
U : (x : (↑s : Type u)) → Set X
hU : ∀ (x : (↑s : Type u)), (↑x : X) ∈ U x ∧ IsOpen[inst] (U x)
hUf : ∀ (x : (↑s : Type u)), (U x)ᶜ ∈ f
t : Set (↑s : Type u)
ht : t.Countable
h : s ⊆ ⋃ i ∈ t, U i
uinf : ⋃ i ∈ t, U i ∈ f.sets
uninf : (⋃ i ∈ t, U i)ᶜ ∈ f
⊢ (⋃ i ∈ t, U i)ᶜᶜ ∉ f

Tactic:
have uninf := compl_notMem uninf
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
fsub : f ≤ 𝓟 s
U : (x : (↑s : Type u)) → Set X
hU : ∀ (x : (↑s : Type u)), (↑x : X) ∈ U x ∧ IsOpen[inst] (U x)
hUf : ∀ (x : (↑s : Type u)), (U x)ᶜ ∈ f
t : Set (↑s : Type u)
ht : t.Countable
h : s ⊆ ⋃ i ∈ t, U i
uinf : ⋃ i ∈ t, U i ∈ f.sets
uninf_1 : (⋃ i ∈ t, U i)ᶜ ∈ f
uninf : (⋃ i ∈ t, U i)ᶜᶜ ∉ f
⊢ ⋃ i ∈ t, U i ∉ f

Tactic:
simp only [compl_compl] at uninf

Premises used: compl_compl
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
fsub : f ≤ 𝓟 s
U : (x : (↑s : Type u)) → Set X
hU : ∀ (x : (↑s : Type u)), (↑x : X) ∈ U x ∧ IsOpen[inst] (U x)
hUf : ∀ (x : (↑s : Type u)), (U x)ᶜ ∈ f
t : Set (↑s : Type u)
ht : t.Countable
h : s ⊆ ⋃ i ∈ t, U i
uinf : ⋃ i ∈ t, U i ∈ f.sets
uninf_1 : (⋃ i ∈ t, U i)ᶜ ∈ f
uninf : ⋃ i ∈ t, U i ∉ f
⊢ False

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

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

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

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

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

Tactic:
⟨t, ?_⟩

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

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

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

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

Tactic:
⟨fun hs ↦ hs.elim_countable_subcover, isLindelof_of_countable_subcover⟩

Premises used: isLindelof_of_countable_subcover, Iff.intro, IsLindelof.elim_countable_subcover
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsLindelof s ↔
    ∀ {ι : Type u} (t : ι → Set X),
      (∀ (i : ι), IsClosed[inst] (t i)) → s ∩ ⋂ (i : ι), t i = ∅ → ∃ (u : Set ι), u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅

Tactic:
⟨fun hs ↦ hs.elim_countable_subfamily_closed, isLindelof_of_countable_subfamily_closed⟩

Premises used: isLindelof_of_countable_subfamily_closed, IsLindelof.elim_countable_subfamily_closed, Iff.intro
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsLindelof.{u} (X := X) ∅

Tactic:
fun _f hnf _ hsf ↦
  Not.elim hnf.ne <| empty_mem_iff_bot.1 <| le_principal_iff.1 hsf

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

Tactic:
simpa only [principal_singleton] using pure_le_nhds x

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

Tactic:
Subsingleton.induction_on hs isLindelof_empty fun _ ↦ isLindelof_singleton

Premises used: isLindelof_singleton, Set.Subsingleton.induction_on, isLindelof_empty
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
h :
  ∀ {ι_1 : Type u} (U : ι_1 → Set X),
    (∀ (i : ι_1), IsOpen[inst] (U i)) →
      Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ (i : ι_1), U i) →
        ∃ (t : Set ι_1), t.Countable ∧ Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ i ∈ t, U i)
⊢ IsLindelof.{u} (X := X) (⋃ i ∈ s, f i)

Tactic:
apply isLindelof_of_countable_subcover

Premises used: isLindelof_of_countable_subcover
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen[inst] (U i)
hUcover : Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ (i : i), U i)
⊢ ∀ i_1 ∈ s, f i_1 ⊆ ⋃ (i : i), U i

Tactic:
have hiU : ∀ i ∈ s, f i ⊆ ⋃ i, U i :=
    fun _ is ↦ _root_.subset_trans (subset_biUnion_of_mem is) hUcover
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen[inst] (U i)
hUcover : Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ (i : i), U i)
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ (i : i), U i
⊢ ∀ (i_1 : ι) (is : i_1 ∈ s), ∃ (r : Set i), r.Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r, U i_2

Tactic:
have iSets := fun i is ↦ (hf i is).elim_countable_subcover U hU (hiU i is)
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen[inst] (U i)
hUcover : Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ (i : i), U i)
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ (i : i), U i
iSets : ∀ (i_1 : ι) (is : i_1 ∈ s), ∃ (r : Set i), r.Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r, U i_2
h :
  ∀ (r : (i_1 : ι) → Set i) (hr : ∀ (i_1 : ι) (is : i_1 ∈ s), (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2),
    ∃ (t : Set i), t.Countable ∧ Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ i_1 ∈ t, U i_1)
⊢ ∃ (t : Set i), t.Countable ∧ Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ i_1 ∈ t, U i_1)

Tactic:
choose! r hr using iSets
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen[inst] (U i)
hUcover : Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ (i : i), U i)
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ (i : i), U i
r : (i_1 : ι) → Set i
hr : ∀ (i_1 : ι) (is : i_1 ∈ s), (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2
h :
  Set.Countable.{u} (α := i) (⋃ i_1 ∈ s, r i_1) ∧
    Subset.{u} (α := Set X) (⋃ i ∈ s, f i)
      (⋃ (i_1 : i), ⋃ (_ : Membership.mem (γ := Set i) (⋃ i_2 ∈ s, r i_2) i_1), U i_1)
⊢ ∃ (t : Set i), t.Countable ∧ Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ i_1 ∈ t, U i_1)

Tactic:
use ⋃ i ∈ s, r i
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen[inst] (U i)
hUcover : Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ (i : i), U i)
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ (i : i), U i
r : (i_1 : ι) → Set i
hr : ∀ (i_1 : ι) (is : i_1 ∈ s), (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2
h : Set.Countable.{u} (α := i) (⋃ i_1 ∈ s, r i_1)
h₁ :
  Subset.{u} (α := Set X) (⋃ i ∈ s, f i)
    (⋃ (i_1 : i), ⋃ (_ : Membership.mem (γ := Set i) (⋃ i_2 ∈ s, r i_2) i_1), U i_1)
⊢ Set.Countable.{u} (α := i) (⋃ i_1 ∈ s, r i_1) ∧
    Subset.{u} (α := Set X) (⋃ i ∈ s, f i)
      (⋃ (i_1 : i), ⋃ (_ : Membership.mem (γ := Set i) (⋃ i_2 ∈ s, r i_2) i_1), U i_1)

Tactic:
constructor
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen[inst] (U i)
hUcover : Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ (i : i), U i)
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ (i : i), U i
r : (i_1 : ι) → Set i
hr : ∀ (i_1 : ι) (is : i_1 ∈ s), (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2
⊢ Set.Countable.{u} (α := i) (⋃ i_1 ∈ s, r i_1)

Tactic:
(Countable.biUnion_iff hs).mpr ?h.left.a

Premises used: Iff.mpr, Set.Countable.biUnion_iff
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen[inst] (U i)
hUcover : Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ (i : i), U i)
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ (i : i), U i
r : (i_1 : ι) → Set i
hr : ∀ (i_1 : ι) (is : i_1 ∈ s), (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2
h : ∀ (a : ι) (ha : a ∈ s), (r a).Countable
⊢ Set.Countable.{u} (α := i) (⋃ i_1 ∈ s, r i_1)

Tactic:
refine (Countable.biUnion_iff hs).mpr ?h.left.a

Premises used: Iff.mpr, Set.Countable.biUnion_iff
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen[inst] (U i)
hUcover : Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ (i : i), U i)
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ (i : i), U i
r : (i_1 : ι) → Set i
hr : ∀ (i_1 : ι) (is : i_1 ∈ s), (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2
⊢ ∀ (a : ι) (ha : a ∈ s), (r a).Countable

Tactic:
fun s hs ↦ (hr s hs).1

Premises used: And.left
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen[inst] (U i)
hUcover : Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ (i : i), U i)
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ (i : i), U i
r : (i_1 : ι) → Set i
hr : ∀ (i_1 : ι) (is : i_1 ∈ s), (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2
⊢ ∀ (a : ι) (ha : a ∈ s), (r a).Countable

Tactic:
exact fun s hs ↦ (hr s hs).1

Premises used: And.left