awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed[inst] t
f : Filter X
hnf : f.NeBot
inst_1 : CountableInterFilter f
hstf : f ≤ 𝓟 (s ∩ t)
⊢ ∃ x ∈ s ∩ t, ClusterPt x f
have hstf₁ : f ≤ 𝓟 s ∧ f ≤ 𝓟 t
Tactic: rw [← inf_principal, le_inf_iff] at hstf
Cleared hypotheses: hstf
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed[inst] t
f : Filter X
hnf : f.NeBot
inst_1 : CountableInterFilter f
hstf : f ≤ 𝓟 s ∧ f ≤ 𝓟 t
⊢ ∃ x ∈ s ∩ t, ClusterPt x f
have obtain : ∀ (x : X) (hsx : x ∈ s) (hx : ClusterPt x f), ∃ x ∈ s ∩ t, ClusterPt x f
Tactic: obtain ⟨x, hsx, hx⟩ : ∃ x ∈ s, ClusterPt x f := hs hstf.1
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed[inst] t
f : Filter X
hnf : f.NeBot
inst_1 : CountableInterFilter f
hstf : f ≤ 𝓟 s ∧ f ≤ 𝓟 t
x : X
hsx : x ∈ s
hx : ClusterPt x f
⊢ ∃ x ∈ s ∩ t, ClusterPt x f
have hxt : x ∈ t
Tactic: have hxt : x ∈ t := ht.mem_of_nhdsWithin_neBot <| hx.mono hstf.2
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
inst_2 : CountableInterFilter l
ls : l ≤ 𝓟 (f '' s)
⊢ ∃ x ∈ f '' s, ClusterPt x l
have this : (comap f l ⊓ 𝓟 s).NeBot
Tactic: have : NeBot (l.comap f ⊓ 𝓟 s) :=
    comap_inf_principal_neBot_of_image_mem lne (le_principal_iff.1 ls)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
inst_2 : CountableInterFilter l
ls : l ≤ 𝓟 (f '' s)
this : (comap f l ⊓ 𝓟 s).NeBot
⊢ ∃ x ∈ f '' s, ClusterPt x l
have obtain : ∀ (x : X) (hxs : x ∈ s) (hx : ClusterPt x (comap f l ⊓ 𝓟 s)), ∃ x ∈ f '' s, ClusterPt x l
Tactic: obtain ⟨x, hxs, hx⟩ : ∃ x ∈ s, ClusterPt x (l.comap f ⊓ 𝓟 s) := @hs _ this _ inf_le_right
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
inst_2 : CountableInterFilter l
ls : l ≤ 𝓟 (f '' s)
this : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
⊢ ∃ x ∈ f '' s, ClusterPt x l
have this₁ : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
Tactic: haveI := hx.neBot
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
inst_2 : CountableInterFilter l
ls : l ≤ 𝓟 (f '' s)
this_1 : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
⊢ ∃ x ∈ f '' s, ClusterPt x l
have right : ClusterPt (f x) l
Tactic: use f x, mem_image_of_mem f hxs
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
inst_2 : CountableInterFilter l
ls : l ≤ 𝓟 (f '' s)
this_1 : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
⊢ Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l)
have h : 𝓝 x ⊓ (comap f l ⊓ 𝓟 s) = 𝓝[s] x ⊓ comap f l
Tactic: convert! (hf x hxs).inf (@tendsto_comap _ _ f l) using 1
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
inst_2 : CountableInterFilter l
ls : l ≤ 𝓟 (f '' s)
this_1 : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
⊢ ClusterPt (f x) l
have this₁ : Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l)
Tactic: have : Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l) := by
    convert! (hf x hxs).inf (@tendsto_comap _ _ f l) using 1
    rw [nhdsWithin]
    ac_rfl
-- 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
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
s_1 t : Set X
hst : s_1 ⊆ t
⊢ (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s_1 ⊆ ⋃ i ∈ r, U i
have this : ∀ (r : Set ι) (hrcountable : r.Countable) (hsub : t ⊆ ⋃ i ∈ r, U i), ∃ (r : Set ι), r.Countable ∧ s_1 ⊆ ⋃ i ∈ r, U i
Tactic: ⟨r, ⟨hrcountable, hsub⟩⟩
-- 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
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
⊢ ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
have hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
Tactic: have hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r : Set ι, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i)
      → (∃ r : Set ι, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) := by
    intro _ _ hst ⟨r, ⟨hrcountable, hsub⟩⟩
    exact ⟨r, hrcountable, Subset.trans hst hsub⟩
-- 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
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
S : Set (Set X)
hS : S.Countable
hsr : ∀ s ∈ S, ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
⊢ ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
have choose! : ∀ (r : (s : Set X) → Set ι) (hr : ∀ s ∈ S, (r s).Countable ∧ s ⊆ ⋃ i ∈ r s, U i),
  ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
Tactic: choose! r hr using hsr
Cleared hypotheses: hsr
-- 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
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
S : Set (Set X)
hS : S.Countable
r : (s : Set X) → Set ι
hr : ∀ s ∈ S, (r s).Countable ∧ s ⊆ ⋃ i ∈ r s, U i
⊢ ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
have refine : ⋃₀ S ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) (⋃ s ∈ S, r s) i), U i
Tactic: refine ⟨⋃ s ∈ S, r s, hS.biUnion_iff.mpr (fun s hs ↦ (hr s hs).1), ?_⟩
-- 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
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
S : Set (Set X)
hS : S.Countable
r : (s : Set X) → Set ι
hr : ∀ s ∈ S, (r s).Countable ∧ s ⊆ ⋃ i ∈ r s, U i
⊢ ⋃₀ S ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) (⋃ s ∈ S, r s) i), U i
have h : ∀ t' ∈ S, t' ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) (⋃ s ∈ S, r s) i), U i
Tactic: refine sUnion_subset ?h.right.h
-- 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
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
S : Set (Set X)
hS : S.Countable
r : (s : Set X) → Set ι
hr : ∀ s ∈ S, (r s).Countable ∧ s ⊆ ⋃ i ∈ r s, U i
⊢ ∀ t' ∈ S, t' ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) (⋃ s ∈ S, r s) i), U i
have h : ∀ t' ∈ S, t' ⊆ ⋃ y ∈ S, ⋃ x ∈ r y, U x
Tactic: simp only [mem_iUnion, exists_prop, iUnion_exists, biUnion_and']
-- 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
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
⊢ ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
have hcountable_union : ∀ (S : Set (Set X)),
  S.Countable →
    (∀ s ∈ S, ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
Tactic: have hcountable_union : ∀ (S : Set (Set X)), S.Countable
      → (∀ s ∈ S, ∃ r : Set ι, r.Countable ∧ (s ⊆ ⋃ i ∈ r, U i))
      → ∃ r : Set ι, r.Countable ∧ (⋃₀ S ⊆ ⋃ i ∈ r, U i) := by
    intro S hS hsr
    choose! r hr using hsr
    refine ⟨⋃ s ∈ S, r s, hS.biUnion_iff.mpr (fun s hs ↦ (hr s hs).1), ?_⟩
    refine sUnion_subset ?h.right.h
    simp only [mem_iUnion, exists_prop, iUnion_exists, biUnion_and']
    exact fun i is x hx ↦ mem_biUnion is ((hr i is).2 hx)
-- 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
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
hcountable_union :
  ∀ (S : Set (Set X)),
    S.Countable →
      (∀ s ∈ S, ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
x : X
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i
have let : ∀ (i : ι) (hi : x ∈ U i), ∃ t ∈ 𝓝[s] x, ∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i
Tactic: let ⟨i, hi⟩ := mem_iUnion.1 (hsU hx)
-- 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
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
hcountable_union :
  ∀ (S : Set (Set X)),
    S.Countable →
      (∀ s ∈ S, ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
x : X
hx : x ∈ s
i : ι
hi : x ∈ U i
⊢ ∃ t ∈ 𝓝[s] x, ∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i
have refine : U i ⊆ ⋃ (i_1 : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i} i_1), U i_1
Tactic: refine ⟨U i, mem_nhdsWithin_of_mem_nhds ((hUo i).mem_nhds hi), {i}, by simp, ?_⟩
-- 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
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
hcountable_union :
  ∀ (S : Set (Set X)),
    S.Countable →
      (∀ s ∈ S, ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
x : X
hx : x ∈ s
i : ι
hi : x ∈ U i
⊢ U i ⊆ ⋃ (i_1 : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i} i_1), U i_1
have simp : U i ⊆ U i
Tactic: simp only [mem_singleton_iff, iUnion_iUnion_eq_left]
-- 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
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
hcountable_union :
  ∀ (S : Set (Set X)),
    S.Countable →
      (∀ s ∈ S, ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
⊢ ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
have h_nhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i
Tactic: have h_nhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ r : Set ι, r.Countable ∧ (t ⊆ ⋃ i ∈ r, U i) := by
    intro x hx
    let ⟨i, hi⟩ := mem_iUnion.1 (hsU hx)
    refine ⟨U i, mem_nhdsWithin_of_mem_nhds ((hUo i).mem_nhds hi), {i}, by simp, ?_⟩
    simp only [mem_singleton_iff, iUnion_iUnion_eq_left]
    exact Subset.refl _
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
⊢ ∃ (t : Set (↑s : Type u)), t.Countable ∧ s ⊆ ⋃ x ∈ t, U (↑x : X) ⋯
have this : ∃ (r : Set (↑s : Type u)), r.Countable ∧ s ⊆ ⋃ i ∈ r, (fun (x : (↑s : Type u)) ↦ interior (U (↑x : X) sorry)) i
Tactic: have := hs.elim_countable_subcover (fun x : s ↦ interior (U x x.2)) (fun _ ↦ isOpen_interior)
    fun x hx ↦
      mem_iUnion.2 ⟨⟨x, hx⟩, mem_interior_iff_mem_nhds.2 <| hU _ _⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
this : ∃ (r : Set (↑s : Type u)), r.Countable ∧ s ⊆ ⋃ i ∈ r, (fun (x : (↑s : Type u)) ↦ interior (U (↑x : X) ⋯)) i
⊢ ∃ (t : Set (↑s : Type u)), t.Countable ∧ s ⊆ ⋃ x ∈ t, U (↑x : X) ⋯
have rcases : ∀ (r : Set (↑s : Type u)) (hr : r.Countable) (hs : s ⊆ ⋃ i ∈ r, (fun (x : (↑s : Type u)) ↦ interior (U (↑x : X) sorry)) i),
  ∃ (t : Set (↑s : Type u)), t.Countable ∧ s ⊆ ⋃ x ∈ t, U (↑x : X) sorry
Tactic: rcases this with ⟨r, ⟨hr, hs⟩⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
⊢ ∃ (t : Set (↑s : Type u)), t.Countable ∧ s ⊆ ⋃ x ∈ t, U (↑x : X) ⋯
have right : s ⊆ ⋃ x ∈ r, U (↑x : X) sorry
Tactic: use r, hr
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
⊢ s ⊆ ⋃ x ∈ r, U (↑x : X) ⋯
have right : Subset.{u} (α := Set X) (⋃ i ∈ r, (fun (x : (↑s : Type u)) ↦ interior (U (↑x : X) sorry)) i) (⋃ x ∈ r, U (↑x : X) sorry)
Tactic: apply Subset.trans hs
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
⊢ Subset.{u} (α := Set X) (⋃ i ∈ r, (fun (x : (↑s : Type u)) ↦ interior (U (↑x : X) ⋯)) i) (⋃ x ∈ r, U (↑x : X) ⋯)
have right : ∀ (i : (↑s : Type u)) (j : i ∈ r),
  Subset.{u} (α := Set X) ((fun (x : (↑s : Type u)) ↦ interior (U (↑x : X) sorry)) i) (⋃ x ∈ r, U (↑x : X) sorry)
Tactic: apply iUnion₂_subset
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
⊢ Subset.{u} (α := Set X) ((fun (x : (↑s : Type u)) ↦ interior (U (↑x : X) ⋯)) i) (⋃ x ∈ r, U (↑x : X) ⋯)
have right : U (↑i : X) sorry ⊆ ⋃ x ∈ r, U (↑x : X) sorry
Tactic: apply Subset.trans interior_subset
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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 X), t.Countable ∧ (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x
have 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
Tactic: let ⟨t, ⟨htc, htsub⟩⟩ := hs.elim_nhds_subcover' (fun x _ ↦ U x) hU
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
have 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
Tactic: refine ⟨↑t, Countable.image htc Subtype.val, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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 ∈ Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t, x ∈ s) ∧
    s ⊆ ⋃ x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t, U x
have left : ∀ x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t, x ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
⊢ (∀ 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
have right : s ⊆ ⋃ x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t, U x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
⊢ x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t → x ∈ s
have left : ∀ (x_1 : x ∈ s) (h : Subtype.mk (p := fun (a : X) ↦ a ∈ s) x sorry ∈ t), x ∈ s
Tactic: simp only [mem_image, Subtype.exists, exists_and_right, exists_eq_right, forall_exists_index]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
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)
⊢ s ⊆ ⋃ x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t, U x
have this : 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
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
⊢ ∃ (f : ℕ → ι), s ⊆ ⋃ (n : ℕ), U (f n)
have obtain : ∀ (c : Set ι) (c_count : c.Countable) (c_cov : s ⊆ ⋃ i ∈ c, U i), ∃ (f : ℕ → ι), s ⊆ ⋃ (n : ℕ), U (f n)
Tactic: obtain ⟨c, ⟨c_count, c_cov⟩⟩ := hs.elim_countable_subcover U hUo hsU
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
⊢ ∃ (f : ℕ → ι), s ⊆ ⋃ (n : ℕ), U (f n)
have inl : ∀ (c_count : Set.Countable.{v} (α := ι) ∅) (c_cov : s ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ i), U i),
  ∃ (f : ℕ → ι), s ⊆ ⋃ (n : ℕ), U (f n)
Tactic: rcases c.eq_empty_or_nonempty with rfl | c_nonempty
Cleared hypotheses: c, c_count, c_cov
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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)
⊢ ∃ (f : ℕ → ι), s ⊆ ⋃ (n : ℕ), U (f n)
have inr : ∀ (c_nonempty : c.Nonempty), ∃ (f : ℕ → ι), s ⊆ ⋃ (n : ℕ), U (f n)
Tactic: rcases c.eq_empty_or_nonempty with rfl | c_nonempty
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
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
⊢ ∃ (f : ℕ → ι), s ⊆ ⋃ (n : ℕ), U (f n)
have c_cov₁ : s ⊆ ∅
Tactic: simp only [mem_empty_iff_false, iUnion_of_empty, iUnion_empty] at c_cov
Cleared hypotheses: c_cov
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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 : ℕ → ι), s ⊆ ⋃ (n : ℕ), U (f n)
have inr : ∀ (f : ℕ → (↑c : Type v)) (f_surj : Function.Surjective f), ∃ (f : ℕ → ι), s ⊆ ⋃ (n : ℕ), U (f n)
Tactic: obtain ⟨f, f_surj⟩ := (Set.countable_iff_exists_surjective c_nonempty).mp c_count
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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)
have inr : ∀ i ∈ c, U i ⊆ ⋃ (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))⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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
⊢ U x ⊆ ⋃ (n : ℕ), U (↑(f n) : ι)
have inr : ∀ (n : ℕ) (hn : f n = Subtype.mk (p := fun (x : ι) ↦ x ∈ c) x hx), U x ⊆ ⋃ (n : ℕ), U (↑(f n) : ι)
Tactic: obtain ⟨n, hn⟩ := f_surj ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
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 = U (↑(f n) : ι)
have rw : U x = U (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ c) x hx) : ι)
Tactic: rw [hn]
-- 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
⊢ Disjoint (𝓝ˢ s) l ↔ ∀ x ∈ s, Disjoint (𝓝 x) l
have refine : ∀ (H : ∀ x ∈ s, Disjoint (𝓝 x) l), Disjoint (𝓝ˢ s) l
Tactic: refine ⟨fun h x hx ↦ h.mono_left <| nhds_le_nhdsSet hx, fun H ↦ ?_⟩