awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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)
have h : Set.Countable.{u} (α := i) (⋃ i_1 ∈ s, r i_1)
Tactic: constructor
-- 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
h : Set.Countable.{u} (α := i) (⋃ i_1 ∈ s, r 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)
have 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)
Tactic: constructor
-- 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
⊢ Set.Countable.{u} (α := i) (⋃ i_1 ∈ s, r i_1)
have h : ∀ (a : ι) (ha : a ∈ s), (r a).Countable
Tactic: refine (Countable.biUnion_iff hs).mpr ?h.left.a
-- 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
⊢ 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)
have h : ∀ (i_1 : ι) (j : i_1 ∈ s), f i_1 ⊆ ⋃ (i_2 : i), ⋃ (_ : Membership.mem (γ := Set i) (⋃ i_3 ∈ s, r i_3) i_2), U i_2
Tactic: refine iUnion₂_subset ?h.right.h
-- 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_1 : Type u
U : i_1 → Set X
hU : ∀ (i : i_1), IsOpen[inst] (U i)
hUcover : Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ (i : i_1), U i)
hiU : ∀ i ∈ s, f i ⊆ ⋃ (i : i_1), U i
r : (i : ι) → Set i_1
hr : ∀ (i : ι) (is : i ∈ s), (r i).Countable ∧ f i ⊆ ⋃ i_2 ∈ r i, U i_2
i : ι
is : i ∈ s
⊢ f i ⊆ ⋃ (i : i_1), ⋃ (_ : Membership.mem (γ := Set i_1) (⋃ i ∈ s, r i) i), U i
have h : f i ⊆ ⋃ 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 (goal)
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
hf : S.Countable
hc : ∀ s ∈ S, IsLindelof s
⊢ IsLindelof (⋃₀ S)
have rw : IsLindelof.{u} (X := X) (⋃ i ∈ S, i)
Tactic: rw [sUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
hf : S.Finite
hc : ∀ s ∈ S, IsLindelof s
⊢ IsLindelof (⋃₀ S)
have rw : IsLindelof.{u} (X := X) (⋃ i ∈ S, i)
Tactic: rw [sUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : DiscreteTopology X
hs : IsLindelof s
⊢ s.Countable
have this : ∀ (x : X), {x} ∈ 𝓝 x
Tactic: have : ∀ x : X, ({x} : Set X) ∈ 𝓝 x := by simp [nhds_discrete]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : DiscreteTopology X
hs : IsLindelof s
this : ∀ (x : X), {x} ∈ 𝓝 x
⊢ s.Countable
have rcases : ∀ (t : Set X) (ht : t.Countable), (∀ x ∈ t, x ∈ s) → ∀ (hssubt : s ⊆ ⋃ x ∈ t, {x}), s.Countable
Tactic: rcases hs.elim_nhds_subcover (fun x => {x}) fun x _ => this x with ⟨t, ht, _, hssubt⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : DiscreteTopology X
hs : IsLindelof s
this : ∀ (x : X), {x} ∈ 𝓝 x
t : Set X
ht : t.Countable
left : ∀ x ∈ t, x ∈ s
hssubt : s ⊆ ⋃ x ∈ t, {x}
⊢ s.Countable
have hssubt₁ : s ⊆ t
Tactic: rw [biUnion_of_singleton] at hssubt
Cleared hypotheses: hssubt
-- 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 : IsLindelof t
⊢ IsLindelof (s ∪ t)
have rw : IsLindelof.{u} (X := X) (⋃ (b : Bool), bif b then s else t)
Tactic: rw [union_eq_iUnion]
-- 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 : IsLindelof t
b : Bool
⊢ IsLindelof (bif b then s else t)
have false : IsLindelof (bif false then s else t)
Tactic: cases b
Cleared hypotheses: b
-- 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 : IsLindelof t
b : Bool
false : IsLindelof (bif Bool.false then s else t)
⊢ IsLindelof (bif b then s else t)
have true : IsLindelof (bif true then s else t)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
U : Set X
⊢ IsLindelof U ∧ IsOpen[inst] U ↔ ∃ (s : Set ι), s.Countable ∧ U = ⋃ i ∈ s, b i
have mp : IsLindelof U ∧ IsOpen[inst] U → ∃ (s : Set ι), s.Countable ∧ U = ⋃ i ∈ s, b i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
U : Set X
mp : IsLindelof U ∧ IsOpen[inst] U → ∃ (s : Set ι), s.Countable ∧ U = ⋃ i ∈ s, b i
⊢ IsLindelof U ∧ IsOpen[inst] U ↔ ∃ (s : Set ι), s.Countable ∧ U = ⋃ i ∈ s, b i
have mpr : (∃ (s : Set ι), s.Countable ∧ U = ⋃ i ∈ s, b i) → IsLindelof U ∧ IsOpen[inst] U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
U : Set X
h₁ : IsLindelof U
h₂ : IsOpen[inst] U
⊢ ∃ (s : Set ι), s.Countable ∧ U = ⋃ i ∈ s, b i
have mp : ∀ (Y : Type u) (f : Y → Set X) (hf : ∀ (i : Y), f i ∈ range b) (h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), f i))
  (h₂ : IsOpen[inst] (⋃ (i : Y), f i)),
  ∃ (s : Set ι), s.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ (i : Y), f i) (⋃ i ∈ s, b i)
Tactic: obtain ⟨Y, f, rfl, hf⟩ := hb.open_eq_iUnion h₂
Cleared hypotheses: U, h₁, h₂
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f : Y → Set X
hf : ∀ (i : Y), f i ∈ range b
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), f i)
h₂ : IsOpen[inst] (⋃ (i : Y), f i)
⊢ ∃ (s : Set ι), s.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ (i : Y), f i) (⋃ i ∈ s, b i)
have mp : ∀ (f' : (i : Y) → ι) (hf' : ∀ (i : Y), b (f' i) = f i),
  ∃ (s : Set ι), s.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ (i : Y), f i) (⋃ i ∈ s, b i)
Tactic: choose f' hf' using hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f : Y → Set X
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), f i)
h₂ : IsOpen[inst] (⋃ (i : Y), f i)
f' : (i : Y) → ι
hf' : ∀ (i : Y), b (f' i) = f i
⊢ ∃ (s : Set ι), s.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ (i : Y), f i) (⋃ i ∈ s, b i)
have this : b ∘ f' = f
Tactic: have : b ∘ f' = f := funext hf'
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f : Y → Set X
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), f i)
h₂ : IsOpen[inst] (⋃ (i : Y), f i)
f' : (i : Y) → ι
hf' : ∀ (i : Y), b (f' i) = f i
this : b ∘ f' = f
⊢ ∃ (s : Set ι), s.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ (i : Y), f i) (⋃ i ∈ s, b i)
have mp : ∀ (h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)) (h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i))
  (hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i),
  ∃ (s : Set ι), s.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ s, b i)
Tactic: subst this
Cleared hypotheses: f, h₁, h₂, hf', this
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : (i : Y) → ι
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)
h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
⊢ ∃ (s : Set ι), s.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ s, b i)
have mp : ∀ (t : Set Y) (ht : t.Countable ∧ Subset.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ t, (b ∘ f') i)),
  ∃ (s : Set ι), s.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ s, b i)
Tactic: obtain ⟨t, ht⟩ :=
      h₁.elim_countable_subcover (b ∘ f') (fun i => hb.isOpen (Set.mem_range_self _)) Subset.rfl
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : (i : Y) → ι
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)
h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ Subset.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ t, (b ∘ f') i)
⊢ ∃ (s : Set ι), s.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ s, b i)
have mp : LE.le.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ f' '' t, b i)
Tactic: refine ⟨t.image f', Countable.image (ht.1) f', le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : (i : Y) → ι
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)
h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ Subset.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ t, (b ∘ f') i)
mp : LE.le.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ f' '' t, b i)
⊢ ∃ (s : Set ι), s.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ s, b i)
have mp₁ : LE.le.{u} (α := Set X) (⋃ i ∈ f' '' t, b i) (⋃ (i : Y), (b ∘ f') i)
Tactic: refine ⟨t.image f', Countable.image (ht.1) f', le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : (i : Y) → ι
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)
h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ Subset.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ t, (b ∘ f') i)
⊢ LE.le.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ f' '' t, b i)
have mp : Subset.{u} (α := Set X) (⋃ i ∈ t, (b ∘ f') i) (⋃ i ∈ f' '' t, b i)
Tactic: refine Set.Subset.trans ht.2 ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : (i : Y) → ι
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)
h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ Subset.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ t, (b ∘ f') i)
⊢ Subset.{u} (α := Set X) (⋃ i ∈ t, (b ∘ f') i) (⋃ i ∈ f' '' t, b i)
have mp : ∀ (i : Y) (i_1 : i ∈ t), (b ∘ f') i ⊆ ⋃ i ∈ f' '' t, b i
Tactic: simp only [Set.iUnion_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : (i : Y) → ι
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)
h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ Subset.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ t, (b ∘ f') i)
i : Y
hi : i ∈ t
⊢ (b ∘ f') i ⊆ ⋃ i ∈ f' '' t, b i
have mp : (b ∘ f') i ⊆ ⋃ (x : { x : ι // x ∈ f' '' t }), b (↑x : ι)
Tactic: rw [← Set.iUnion_subtype (fun x : ι => x ∈ t.image f') fun i => b i.1]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : (i : Y) → ι
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)
h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ Subset.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ t, (b ∘ f') i)
⊢ LE.le.{u} (α := Set X) (⋃ i ∈ f' '' t, b i) (⋃ (i : Y), (b ∘ f') i)
have mp : ∀ (i : ι) (j : i ∈ f' '' t), b i ⊆ ⋃ (i : Y), (b ∘ f') i
Tactic: apply Set.iUnion₂_subset
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : (i : Y) → ι
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)
h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ Subset.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ t, (b ∘ f') i)
i : ι
hi : i ∈ f' '' t
⊢ b i ⊆ ⋃ (i : Y), (b ∘ f') i
have mp : ∀ (j : Y) (hi : f' j ∈ f' '' t), b (f' j) ⊆ ⋃ (i : Y), (b ∘ f') i
Tactic: obtain ⟨j, -, rfl⟩ := (mem_image ..).mp hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
s : Set ι
hs : s.Countable
⊢ IsLindelof.{u} (X := X) (⋃ i ∈ s, b i) ∧ IsOpen[inst] (⋃ i ∈ s, b i)
have mpr : IsLindelof.{u} (X := X) (⋃ i ∈ s, b i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
s : Set ι
hs : s.Countable
mpr : IsLindelof.{u} (X := X) (⋃ i ∈ s, b i)
⊢ IsLindelof.{u} (X := X) (⋃ i ∈ s, b i) ∧ IsOpen[inst] (⋃ i ∈ s, b i)
have mpr₁ : IsOpen[inst] (⋃ i ∈ s, b i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
hle : l ≤ 𝓟 (insert y (range f))
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
have pos : ∀ (hy : ClusterPt y l), ∃ x ∈ insert y (range f), ClusterPt x l
Tactic: by_cases hy : ClusterPt y l
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
hle : l ≤ 𝓟 (insert y (range f))
pos : ∀ (hy : ClusterPt y l), ∃ x ∈ insert y (range f), ClusterPt x l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
have neg : ∀ (hy : ¬ClusterPt y l), ∃ x ∈ insert y (range f), ClusterPt x l
Tactic: by_cases hy : ClusterPt y l
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
hle : l ≤ 𝓟 (insert y (range f))
hy : ¬ClusterPt y l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
have hy₁ : ∃ (x : Set Y) (_ : x ∈ 𝓝 y) (x_1 : Set Y) (_ : x_1 ∈ l), Disjoint x x_1
Tactic: simp only [clusterPt_iff_nonempty, not_forall, ← not_disjoint_iff_nonempty_inter, not_not] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
hle : l ≤ 𝓟 (insert y (range f))
hy : ∃ (x : Set Y) (_ : x ∈ 𝓝 y) (x_1 : Set Y) (_ : x_1 ∈ l), Disjoint x x_1
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
have neg : ∀ (s : Set Y) (hsy : s ∈ 𝓝 y) (t : Set Y) (htl : t ∈ l) (hd : Disjoint s t), ∃ x ∈ insert y (range f), ClusterPt x l
Tactic: rcases hy with ⟨s, hsy, t, htl, hd⟩
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
have neg : ∀ (K : Set X) (hKc : IsLindelof K) (hKs : Kᶜ ⊆ f ⁻¹' s), ∃ x ∈ insert y (range f), ClusterPt x l
Tactic: rcases mem_coLindelof.1 (hf hsy) with ⟨K, hKc, hKs⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsLindelof K
hKs : Kᶜ ⊆ f ⁻¹' s
⊢ f '' K ∈ l
have h : ∀ (y_1 : Y) (hyt : y_1 ∈ t) (hyf : y_1 ∈ insert y (range f)), y_1 ∈ f '' K
Tactic: filter_upwards [htl, le_principal_iff.1 hle] with y hyt hyf
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y_1 : Y
hf : Tendsto f (coLindelof X) (𝓝 y_1)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
hle : l ≤ 𝓟 (insert y_1 (range f))
s : Set Y
hsy : s ∈ 𝓝 y_1
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsLindelof K
hKs : Kᶜ ⊆ f ⁻¹' s
y : Y
hyt : y ∈ t
hyf : y ∈ insert y_1 (range f)
⊢ y ∈ f '' K
have h : ∀ (hf : Tendsto f (coLindelof X) (𝓝 y)) (hle : l ≤ 𝓟 (insert y (range f))) (hsy : s ∈ 𝓝 y), y ∈ f '' K
Tactic: rcases hyf with (rfl | ⟨x, rfl⟩)
Cleared hypotheses: y_1, hf, hle, hsy, hyf
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y_1 : Y
hf : Tendsto f (coLindelof X) (𝓝 y_1)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
hle : l ≤ 𝓟 (insert y_1 (range f))
s : Set Y
hsy : s ∈ 𝓝 y_1
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsLindelof K
hKs : Kᶜ ⊆ f ⁻¹' s
y : Y
hyt : y ∈ t
hyf : y ∈ insert y_1 (range f)
h : ∀ (hf : Tendsto f (coLindelof X) (𝓝 y)) (hle : l ≤ 𝓟 (insert y (range f))) (hsy : s ∈ 𝓝 y), y ∈ f '' K
⊢ y ∈ f '' K
have h₁ : ∀ (x : X) (hyt : f x ∈ t), f x ∈ f '' K
Tactic: rcases hyf with (rfl | ⟨x, rfl⟩)
Cleared hypotheses: y, hyt, hyf
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsLindelof K
hKs : Kᶜ ⊆ f ⁻¹' s
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
have this : f '' K ∈ l
Tactic: have : f '' K ∈ l := by
    filter_upwards [htl, le_principal_iff.1 hle] with y hyt hyf
    rcases hyf with (rfl | ⟨x, rfl⟩)
    exacts [(hd.le_bot ⟨mem_of_mem_nhds hsy, hyt⟩).elim,
      mem_image_of_mem _ (not_not.1 fun hxK => hd.le_bot ⟨hKs hxK, hyt⟩)]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
inst_2 : CountableInterFilter l
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsLindelof K
hKs : Kᶜ ⊆ f ⁻¹' s
this : f '' K ∈ l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
have neg : ∀ (y_1 : Y) (hy : y_1 ∈ f '' K) (hyl : ClusterPt y_1 l), ∃ x ∈ insert y (range f), ClusterPt x l
Tactic: rcases hKc.image hfc (le_principal_iff.2 this) with ⟨y, hy, hyl⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
⊢ (coclosedLindelof X).HasBasis (fun (s : Set X) ↦ IsClosed[inst] s ∧ IsLindelof s) compl
have simp : HasBasis (⨅ (s : Set X), ⨅ (_ : IsClosed[inst] s ∧ IsLindelof s), 𝓟 sᶜ)
  (fun (s : Set X) ↦ IsClosed[inst] s ∧ IsLindelof s) compl
Tactic: simp only [Filter.coclosedLindelof, iInf_and']
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
⊢ HasBasis (⨅ (s : Set X), ⨅ (_ : IsClosed[inst] s ∧ IsLindelof s), 𝓟 sᶜ)
    (fun (s : Set X) ↦ IsClosed[inst] s ∧ IsLindelof s) compl
have refine : ∀ (i : Set X),
  IsClosed[inst] i ∧ IsLindelof i →
    ∀ (j : Set X),
      IsClosed[inst] j ∧ IsLindelof j → ∃ (k : Set X), (IsClosed[inst] k ∧ IsLindelof k) ∧ kᶜ ⊆ iᶜ ∧ kᶜ ⊆ jᶜ
Tactic: refine hasBasis_biInf_principal' ?_ ⟨∅, isClosed_empty, isLindelof_empty⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : LindelofSpace X
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
⊢ ∃ (t : Set X), t.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ x ∈ t, U x) univ
have obtain : ∀ (t : Set X) (tc : t.Countable) (s : Subset.{u} (α := Set X) univ (⋃ x ∈ t, U x)),
  ∃ (t : Set X), t.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ x ∈ t, U x) univ
Tactic: obtain ⟨t, tc, -, s⟩ := IsLindelof.elim_nhds_subcover isLindelof_univ U fun x _ => hU x
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : LindelofSpace X
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
t : Set X
tc : t.Countable
s : Subset.{u} (α := Set X) univ (⋃ x ∈ t, U x)
⊢ ∃ (t : Set X), t.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ x ∈ t, U x) univ
have right : Eq.{u + 1} (α := Set X) (⋃ x ∈ t, U x) univ
Tactic: use t, tc