awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis.{u_1} (α := X) (range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X))
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X)
s : Set (↑b : Type u_1)
hs : s.Finite
hU : U = ⋃ i ∈ s, (↑i : Set X)
this : Finite.{u_1 + 1} (↑s : Type u_1)
x : Fintype (↑s : Type u_1) := Fintype.ofFinite (↑s : Type u_1)
⊢ ∃ (s : Finset (↑b : Type u_1)), U = ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ b) '' (↑s : Set (↑b : Type u_1)))
have h : U = ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ b) '' (↑s.toFinset : Set (↑b : Type u_1)))
Tactic: use s.toFinset
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set X
⊢ IsCompact U ∧ IsOpen U ↔ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
have mp : IsCompact U ∧ IsOpen U → ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set X
mp : IsCompact U ∧ IsOpen U → ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
⊢ IsCompact U ∧ IsOpen U ↔ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
have mpr : (∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i) → IsCompact U ∧ IsOpen U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : s.Finite
⊢ IsCompact.{u_1} (X := X) (⋃ i ∈ s, b i) ∧ IsOpen.{u_1} (X := X) (⋃ i ∈ s, b i)
have mpr : IsCompact.{u_1} (X := X) (⋃ i ∈ s, b i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : s.Finite
mpr : IsCompact.{u_1} (X := X) (⋃ i ∈ s, b i)
⊢ IsCompact.{u_1} (X := X) (⋃ i ∈ s, b i) ∧ IsOpen.{u_1} (X := X) (⋃ i ∈ s, b i)
have mpr₁ : IsOpen.{u_1} (X := X) (⋃ i ∈ s, b i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, sᶜ ∈ 𝓝 x ⊓ f
⊢ sᶜ ∈ f
have contrapose! : ∀ (hf : sᶜ ∉ f), ∃ x ∈ s, sᶜ ∉ 𝓝 x ⊓ f
Tactic: contrapose! hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : sᶜ ∉ f
⊢ ∃ x ∈ s, sᶜ ∉ 𝓝 x ⊓ f
have simp : ∀ (hf : (f ⊓ 𝓟 s).NeBot), ∃ x ∈ s, (𝓝 x ⊓ (f ⊓ 𝓟 s)).NeBot
Tactic: simp only [notMem_iff_inf_principal_compl, compl_compl, inf_assoc] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
⊢ sᶜ ∈ f
have refine : ∀ (x : X) (hx : x ∈ s), sᶜ ∈ 𝓝 x ⊓ f
Tactic: refine hs.compl_mem_sets fun x hx => ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
⊢ sᶜ ∈ 𝓝 x ⊓ f
have rcases : ∀ (t : Set X) (ht : t ∈ 𝓝[s] x) (hst : tᶜ ∈ f), sᶜ ∈ 𝓝 x ⊓ f
Tactic: rcases hf x hx with ⟨t, ht, hst⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝[s] x
hst : tᶜ ∈ f
⊢ sᶜ ∈ 𝓝 x ⊓ f
have ht₁ : {x : X | x ∈ s → x ∈ t} ∈ 𝓝 x
Tactic: replace ht := mem_inf_principal.1 ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
t : Set X
hst : tᶜ ∈ f
ht : {x : X | x ∈ s → x ∈ t} ∈ 𝓝 x
⊢ sᶜ ∈ 𝓝 x ⊓ f
have apply : {x : X | x ∈ s → x ∈ t} ∩ tᶜ ⊆ sᶜ
Tactic: apply mem_inf_of_inter ht hst
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
p : Set X → Prop
he : p ∅
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := comk p he ⋯ ⋯
⊢ p s
have this : sᶜ ∈ f
Tactic: have : sᶜ ∈ f := hs.compl_mem_sets_of_nhdsWithin (by simpa [f] using hnhds)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
p : Set X → Prop
he : p ∅
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := comk p he ⋯ ⋯
this : sᶜ ∈ f
⊢ p s
have rwa : p sᶜᶜ
Tactic: rwa [← compl_compl s]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
f : Filter X
hnf : f.NeBot
hstf : f ≤ 𝓟 (s ∩ 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 (le_trans hstf (le_principal_iff.2 inter_subset_left))
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
f : Filter X
hnf : f.NeBot
hstf : f ≤ 𝓟 (s ∩ t)
x : X
hsx : x ∈ s
hx : ClusterPt x f
⊢ ∃ x ∈ s ∩ t, ClusterPt x f
have this : x ∈ t
Tactic: have : x ∈ t := ht.mem_of_nhdsWithin_neBot <|
    hx.mono <| le_trans hstf (le_principal_iff.2 inter_subset_right)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
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.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
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.Compact (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
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.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
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.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
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.Compact (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
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.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsCompact s ↔ ∀ (f : Ultrafilter X), (↑f : Filter X) ≤ 𝓟 s → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x
have refine_1 : Monotone (β := Prop) fun (f : Filter X) ↦ ∃ x ∈ s, ClusterPt x f
Tactic: refine (forall_neBot_le_iff ?_).trans ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
refine_1 : Monotone (β := Prop) fun (f : Filter X) ↦ ∃ x ∈ s, ClusterPt x f
⊢ IsCompact s ↔ ∀ (f : Ultrafilter X), (↑f : Filter X) ≤ 𝓟 s → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x
have refine_2 : (∀ (f : Ultrafilter X), (↑f : Filter X) ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x (↑f : Filter X)) ↔
  ∀ (f : Ultrafilter X), (↑f : Filter X) ≤ 𝓟 s → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x
Tactic: refine (forall_neBot_le_iff ?_).trans ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
s' : Set X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x ∈ s'
⊢ l ≤ 𝓝ˢ s'
have refine : ∀ (f : Ultrafilter X) (hf : (↑f : Filter X) ≤ l), (↑f : Filter X) ≤ 𝓝ˢ s'
Tactic: refine le_iff_ultrafilter.2 fun f hf ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
s' : Set X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x ∈ s'
f : Ultrafilter X
hf : (↑f : Filter X) ≤ l
⊢ (↑f : Filter X) ≤ 𝓝ˢ s'
have rcases : ∀ (x : X) (hxs : x ∈ s) (hx : (↑f : Filter X) ≤ 𝓝 x), (↑f : Filter X) ≤ 𝓝ˢ s'
Tactic: rcases hs.ultrafilter_le_nhds' f (hf hmem) with ⟨x, hxs, hx⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
s' : Set X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x ∈ s'
f : Ultrafilter X
hf : (↑f : Filter X) ≤ l
x : X
hxs : x ∈ s
hx : (↑f : Filter X) ≤ 𝓝 x
⊢ (↑f : Filter X) ≤ 𝓝ˢ s'
have grw : 𝓝 x ≤ 𝓝ˢ s'
Tactic: grw [hx]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
s' : Set X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x ∈ s'
f : Ultrafilter X
hf : (↑f : Filter X) ≤ l
x : X
hxs : x ∈ s
hx : (↑f : Filter X) ≤ 𝓝 x
⊢ 𝓝 x ≤ 𝓝ˢ s'
have refine : x ∈ s'
Tactic: refine nhds_le_nhdsSet ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
y : X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x = y
⊢ l ≤ 𝓝 y
have rw : l ≤ 𝓝ˢ {y}
Tactic: rw [← nhdsSet_singleton]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
Y : Type u_2
l : Filter Y
y : X
f : Y → X
hs : IsCompact s
hmem : ∀ᶠ (x : Y) in l, f x ∈ s
h : ∀ x ∈ s, MapClusterPt x l f → x = y
⊢ Tendsto f l (𝓝 y)
have rw : Tendsto f l (𝓝ˢ {y})
Tactic: rw [← nhdsSet_singleton]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
⊢ ∃ (t : Finset (↑s : Type u)), ⋃ x ∈ t, U (↑x : X) ⋯ ∈ 𝓝ˢ s
have rcases : ∀ (t : Finset (↑s : Type u)) (hst : s ⊆ ⋃ i ∈ t, interior (U (↑i : X) sorry)),
  ∃ (t : Finset (↑s : Type u)), ⋃ x ∈ t, U (↑x : X) sorry ∈ 𝓝ˢ s
Tactic: rcases hs.elim_finite_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 _ _⟩ with ⟨t, hst⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset (↑s : Type u)
hst : s ⊆ ⋃ i ∈ t, interior (U (↑i : X) ⋯)
⊢ ∃ (t : Finset (↑s : Type u)), ⋃ x ∈ t, U (↑x : X) ⋯ ∈ 𝓝ˢ s
have refine : ∀ (x : X) (hx : x ∈ s), ⋃ x ∈ t, U (↑x : X) sorry ∈ 𝓝 x
Tactic: refine ⟨t, mem_nhdsSet_iff_forall.2 fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset (↑s : Type u)
hst : s ⊆ ⋃ i ∈ t, interior (U (↑i : X) ⋯)
x : X
hx : x ∈ s
⊢ ⋃ x ∈ t, U (↑x : X) ⋯ ∈ 𝓝 x
have rcases : ∀ (y : (↑s : Type u)) (hyt : y ∈ t) (hy : x ∈ interior (U (↑y : X) sorry)), ⋃ x ∈ t, U (↑x : X) sorry ∈ 𝓝 x
Tactic: rcases mem_iUnion₂.1 (hst hx) with ⟨y, hyt, hy⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset (↑s : Type u)
hst : s ⊆ ⋃ i ∈ t, interior (U (↑i : X) ⋯)
x : X
hx : x ∈ s
y : (↑s : Type u)
hyt : y ∈ t
hy : x ∈ interior (U (↑y : X) ⋯)
⊢ ⋃ x ∈ t, U (↑x : X) ⋯ ∈ 𝓝 x
have refine : U (↑y : X) sorry ∈ 𝓝 x
Tactic: refine mem_of_superset ?_ (subset_biUnion_of_mem hyt)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
⊢ ∃ (t : Finset X), (∀ x ∈ t, x ∈ s) ∧ ⋃ x ∈ t, U x ∈ 𝓝ˢ s
have let : ∀ (t : Finset (↑s : Type u)) (ht : ⋃ x ∈ t, U (↑x : X) ∈ 𝓝ˢ s), ∃ (t : Finset X), (∀ x ∈ t, x ∈ s) ∧ ⋃ x ∈ t, U x ∈ 𝓝ˢ s
Tactic: let ⟨t, ht⟩ := hs.elim_nhds_subcover_nhdsSet' (fun x _ => U x) hU
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝[s] x
⊢ ∃ (t : Finset (↑s : Type u)), s ⊆ ⋃ x ∈ t, U (↑x : X) ⋯
have choose : ∀ (V : (x : X) → (hx : x ∈ s) → Set X) (V_nhds : ∀ (x : X) (hx : x ∈ s), V x hx ∈ 𝓝 x)
  (hV : ∀ (x : X) (hx : x ∈ s), V x hx ∩ s ⊆ U x hx), ∃ (t : Finset (↑s : Type u)), s ⊆ ⋃ x ∈ t, U (↑x : X) sorry
Tactic: choose V V_nhds hV using fun x hx => mem_nhdsWithin_iff_exists_mem_nhds_inter.1 (hU x hx)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝[s] x
V : (x : X) → (hx : x ∈ s) → Set X
V_nhds : ∀ (x : X) (hx : x ∈ s), V x hx ∈ 𝓝 x
hV : ∀ (x : X) (hx : x ∈ s), V x hx ∩ s ⊆ U x hx
⊢ ∃ (t : Finset (↑s : Type u)), s ⊆ ⋃ x ∈ t, U (↑x : X) ⋯
have refine : ∀ (t : Finset (↑s : Type u)) (ht : s ⊆ ⋃ x ∈ t, V (↑x : X) sorry), s ⊆ ⋃ i ∈ t, V (↑i : X) sorry ∩ s
Tactic: refine (hs.elim_nhds_subcover' V V_nhds).imp fun t ht =>
    subset_trans ?_ (iUnion₂_mono fun x _ => hV x x.2)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝[s] x
⊢ ∃ (t : Finset X), (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x
have choose! : ∀ (V : (x : X) → Set X) (V_nhds : ∀ (x : X) (hx : x ∈ s), V x ∈ 𝓝 x) (hV : ∀ (x : X) (hx : x ∈ s), V x ∩ s ⊆ U x),
  ∃ (t : Finset X), (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x
Tactic: choose! V V_nhds hV using fun x hx => mem_nhdsWithin_iff_exists_mem_nhds_inter.1 (hU x hx)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝[s] x
V : (x : X) → Set X
V_nhds : ∀ (x : X) (hx : x ∈ s), V x ∈ 𝓝 x
hV : ∀ (x : X) (hx : x ∈ s), V x ∩ s ⊆ U x
⊢ ∃ (t : Finset X), (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x
have refine : ∀ (t : Finset X),
  (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, V x → ∀ (t_sub_s : ∀ x ∈ t, x ∈ s) (ht : s ⊆ ⋃ x ∈ t, V x), s ⊆ ⋃ i ∈ t, V i ∩ s
Tactic: refine (hs.elim_nhds_subcover V V_nhds).imp fun t ⟨t_sub_s, ht⟩ =>
    ⟨t_sub_s, subset_trans ?_ (iUnion₂_mono fun x hx => hV x (t_sub_s x hx))⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact 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 => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact 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.Compact (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact 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.Compact (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact 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.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact 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 : Finset X) (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, hts, hst⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact 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 : Finset X
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.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact 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 : Finset X
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₂, biInter_finset_mem]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsCompact s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst] (t i)
hst : ∀ (u : Finset ι), (s ∩ ⋂ i ∈ u, t i).Nonempty
⊢ (s ∩ ⋂ (i : ι), t i).Nonempty
have contrapose! : ∀ (hst : s ∩ ⋂ (i : ι), t i = ∅), ∃ (u : Finset ι), s ∩ ⋂ i ∈ u, t i = ∅
Tactic: contrapose! hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
t : Set (Set X)
ht : ∀ a ∈ t, IsClosed[inst] a
h : ∀ a ⊆ t, a.Finite → (s ∩ ⋂₀ a).Nonempty
⊢ (s ∩ ⋂₀ t).Nonempty
have rw : (s ∩ ⋂ (i : (↑t : Type u)), (↑i : Set X)).Nonempty
Tactic: rw [Set.sInter_eq_iInter]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
t : Set (Set X)
ht : ∀ a ∈ t, IsClosed[inst] a
h : ∀ a ⊆ t, a.Finite → (s ∩ ⋂₀ a).Nonempty
⊢ (s ∩ ⋂ (i : (↑t : Type u)), (↑i : Set X)).Nonempty
have refine : ∀ (a : Finset (↑t : Type u)), (s ∩ ⋂ i ∈ a, (↑i : Set X)).Nonempty
Tactic: refine hs.inter_iInter_nonempty _ (fun i ↦ ht _ i.2) fun a ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t
htn : ∀ (i : ι), (t i).Nonempty
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst] (t i)
i₀ : ι := hι.some
this : (t i₀ ∩ ⋂ (i : ι), t i).Nonempty
⊢ Set.Nonempty.{u} (α := X) (⋂ (i : ι), t i)
have rwa : ∀ (this : Set.Nonempty.{u} (α := X) (⋂ (i : ι), t i)), Set.Nonempty.{u} (α := X) (⋂ (i : ι), t i)
Tactic: rwa [inter_eq_right.mpr (iInter_subset _ i₀)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t
htn : ∀ (i : ι), (t i).Nonempty
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst] (t i)
i₀ : ι := hι.some
⊢ Set.Nonempty.{u} (α := X) (⋂ (i : ι), t i)
have suffices : (t i₀ ∩ ⋂ (i : ι), t i).Nonempty
Tactic: suffices (t i₀ ∩ ⋂ i, t i).Nonempty by
    rwa [inter_eq_right.mpr (iInter_subset _ i₀)] at this
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t
htn : ∀ (i : ι), (t i).Nonempty
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst] (t i)
i₀ : ι := hι.some
⊢ (t i₀ ∩ ⋂ (i : ι), t i).Nonempty
have simp : ∀ (htn : ∀ (i : ι), t i ≠ ∅), t i₀ ∩ ⋂ (i : ι), t i ≠ ∅
Tactic: simp only [nonempty_iff_ne_empty] at htn ⊢
Cleared hypotheses: htn
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst] (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), t i ≠ ∅
⊢ t i₀ ∩ ⋂ (i : ι), t i ≠ ∅
have apply : ¬∀ (hdt : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t), ∃ (i : ι), t i₀ ∩ t i = ∅
Tactic: apply mt ((htc i₀).elim_directed_family_closed t htcl)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst] (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), t i ≠ ∅
⊢ ¬∀ (hdt : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t), ∃ (i : ι), t i₀ ∩ t i = ∅
have push : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t ∧ ∀ (i : ι), (t i₀ ∩ t i).Nonempty
Tactic: push Not