awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
⊢ Disjoint (𝓝ˢ s) l
have 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
Tactic: choose! U hxU hUl using fun x hx ↦ (nhds_basis_opens x).disjoint_iff_left.1 (H x hx)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
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
⊢ Disjoint (𝓝ˢ s) l
have hxU₁ : ∀ (x : X) (hx : x ∈ s), x ∈ U x
Tactic: choose hxU hUo using hxU
Cleared hypotheses: hxU
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
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
⊢ Disjoint (𝓝ˢ s) l
have hUo : ∀ (x : X) (hx : x ∈ s), IsOpen[inst] (U x)
Tactic: choose hxU hUo using hxU
Cleared hypotheses: hxU
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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)
⊢ Disjoint (𝓝ˢ s) l
have rcases : ∀ (t : Set X) (htc : t.Countable) (hts : ∀ x ∈ t, x ∈ s) (hst : s ⊆ ⋃ x ∈ t, U x), 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⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
have refine : (⋃ x ∈ t, U x)ᶜ ∈ l
Tactic: refine (hasBasis_nhdsSet _).disjoint_iff_left.2
    ⟨⋃ x ∈ t, U x, ⟨isOpen_biUnion fun x hx ↦ hUo x (hts x hx), hst⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
⊢ (⋃ x ∈ t, U x)ᶜ ∈ l
have rw : ⋂ i ∈ t, (U i)ᶜ ∈ l
Tactic: rw [compl_iUnion₂]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
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ᶜ
⊢ ∃ (u : Set ι), u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
have hUo : ∀ (i : ι), IsOpen[inst] (U i)
Tactic: have hUo : ∀ i, IsOpen (U i) := by simp only [U, Pi.compl_apply, isOpen_compl_iff]; exact htc
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
have simp : s ⊆ ⋃ (i : ι), (t i)ᶜ
Tactic: simp only [U, Pi.compl_apply]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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 : ι), (t i)ᶜ
have rw : s ⊆ (⋂ (i : ι), t i)ᶜ
Tactic: rw [← compl_iInter]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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 : ι), t i)ᶜ
have apply : Disjoint (⋂ (i : ι), t i)ᶜᶜ s
Tactic: apply disjoint_compl_left_iff_subset.mp
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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 (⋂ (i : ι), t i)ᶜᶜ s
have simp : Disjoint (⋂ (i : ι), t i) s
Tactic: simp only [compl_iInter, compl_iUnion, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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 (⋂ (i : ι), t i) s
have a : Disjoint s (⋂ (i : ι), t i)
Tactic: apply Disjoint.symm
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
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)
⊢ ∃ (u : Set ι), u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
have hsU : 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
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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 ι), u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
have rcases : ∀ (u : Set ι) (hucount : u.Countable) (husub : s ⊆ ⋃ i ∈ u, U i), ∃ (u : Set ι), u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
Tactic: rcases hs.elim_countable_subcover U hUo hsU with ⟨u, ⟨hucount, husub⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
⊢ ∃ (u : Set ι), u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
have right : s ∩ ⋂ i ∈ u, t i = ∅
Tactic: use u, hucount
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
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
⊢ s ∩ ⋂ i ∈ u, t i = ∅
have husub₁ : Disjoint (⋃ i ∈ u, U i)ᶜ s
Tactic: rw [← disjoint_compl_left_iff_subset] at husub
Cleared hypotheses: husub
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
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
⊢ s ∩ ⋂ i ∈ u, t i = ∅
have husub₁ : Disjoint (⋂ i ∈ u, t i) s
Tactic: simp only [U, Pi.compl_apply, compl_iUnion, compl_compl] at husub
Cleared hypotheses: husub
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
⊢ (s ∩ ⋂ (i : ι), t i).Nonempty
have contrapose! : ∀ (hst : s ∩ ⋂ (i : ι), t i = ∅), ∃ (u : Set ι), ∀ (_ : u.Countable), s ∩ ⋂ i ∈ u, t i = ∅
Tactic: contrapose! hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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 ι), ∀ (_ : u.Countable), s ∩ ⋂ i ∈ u, t i = ∅
have rcases : ∀ (u : Set ι), u.Countable → ∀ (husub : 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⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
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
⊢ ∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c i
have hc₃ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))
Tactic: simp only [Subtype.forall', biUnion_eq_iUnion] at hc₁ hc₂
Cleared hypotheses: hc₁, hc₂
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
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 : ι))
⊢ ∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c i
have hc₄ : s ⊆ ⋃ (x : (↑b : Type u_1)), c (↑x : ι)
Tactic: simp only [Subtype.forall', biUnion_eq_iUnion] at hc₁ hc₂
Cleared hypotheses: hc₁, hc₂
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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 : ι)
⊢ ∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c i
have rcases : ∀ (d : Set (↑b : Type u_1)) (hd : d.Countable ∧ s ⊆ ⋃ i ∈ d, 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⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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 : ι)
⊢ ∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c i
have refine : s ⊆ ⋃ i ∈ Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' d, c i
Tactic: refine ⟨Subtype.val '' d, by simp, Countable.image hd.1 Subtype.val, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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 ⊆ ⋃ i ∈ Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' d, c i
have rw : s ⊆ ⋃ y ∈ d, c (↑y : ι)
Tactic: rw [biUnion_image]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
⊢ f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f
have 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
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
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
⊢ ∃ (ι : Type u) (U : ι → Set X),
    (∀ (i : ι), IsOpen[inst] (U i)) ∧ s ⊆ ⋃ (i : ι), U i ∧ ∀ (t : Set ι) (_ : t.Countable), ¬s ⊆ ⋃ i ∈ t, U i
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
⊢ ∃ (ι : Type u) (U : ι → Set X),
    (∀ (i : ι), IsOpen[inst] (U i)) ∧ s ⊆ ⋃ (i : ι), U i ∧ ∀ (t : Set ι) (_ : t.Countable), ¬s ⊆ ⋃ i ∈ t, U i
have 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
Tactic: choose fsub U hU hUf using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
have refine : ∀ (t : Set (↑s : Type u)) (_ : 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 ⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
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
⊢ False
have uinf : ⋃ i ∈ t, U i ∈ f.sets
Tactic: have uinf := f.sets_of_superset (le_principal_iff.1 fsub) h
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
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
⊢ False
have uninf : ⋂ i ∈ t, (U i)ᶜ ∈ f
Tactic: have uninf : ⋂ i ∈ t, (U i)ᶜ ∈ f := (countable_bInter_mem ht).mpr (fun _ _ ↦ hUf _)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
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
⊢ False
have uninf₁ : (⋃ i ∈ t, U i)ᶜ ∈ f
Tactic: rw [← compl_iUnion₂] at uninf
Cleared hypotheses: uninf
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
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
⊢ False
have uninf₁ : (⋃ i ∈ t, U i)ᶜᶜ ∉ f
Tactic: have uninf := compl_notMem uninf
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
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
have uninf₁ : ⋃ i ∈ t, U i ∉ f
Tactic: simp only [compl_compl] at uninf
Cleared hypotheses: uninf
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
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 ι), t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
have hsU₁ : s ⊓ ⋂ (i : ι), (U i)ᶜ = ⊥
Tactic: rw [← disjoint_compl_right_iff_subset, compl_iUnion, disjoint_iff] at hsU
Cleared hypotheses: hsU
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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 ι), t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
have rcases : ∀ (t : Set ι) (ht : 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⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
have refine : t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
Tactic: refine ⟨t, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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.Countable ∧ s ⊆ ⋃ i ∈ t, U i
have rwa : t.Countable ∧ Disjoint s (⋃ i ∈ t, U i)ᶜ
Tactic: rwa [← disjoint_compl_right_iff_subset, compl_iUnion₂, disjoint_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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)ᶜ
⊢ t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
have rwa₁ : t.Countable ∧ Disjoint s (⋂ i ∈ t, (U i)ᶜ)
Tactic: rwa [← disjoint_compl_right_iff_subset, compl_iUnion₂, disjoint_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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)ᶜ)
⊢ t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
have rwa₂ : t.Countable ∧ s ⊓ ⋂ i ∈ t, (U i)ᶜ = ⊥
Tactic: rwa [← disjoint_compl_right_iff_subset, compl_iUnion₂, disjoint_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
⊢ IsLindelof.{u} (X := X) (⋃ i ∈ s, f i)
have 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)
Tactic: apply isLindelof_of_countable_subcover
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
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)
⊢ ∃ (t : Set i), t.Countable ∧ Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ i_1 ∈ t, U i_1)
have hiU : ∀ 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
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
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
⊢ ∃ (t : Set i), t.Countable ∧ Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ i_1 ∈ t, U i_1)
have iSets : ∀ (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)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
⊢ ∃ (t : Set i), t.Countable ∧ Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ i_1 ∈ t, U i_1)
have 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)
Tactic: choose! r hr using iSets
Cleared hypotheses: iSets
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
⊢ ∃ (t : Set i), t.Countable ∧ Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ i_1 ∈ t, U i_1)
have 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)
Tactic: use ⋃ i ∈ s, r i