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
hs : IsCompact s
⊢ IsLindelof s
have tauto : ∀ ⦃f : Filter X⦄ [f.NeBot] [CountableInterFilter f], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsSigmaCompact s
⊢ IsLindelof s
have hs₁ : ∃ (K : ℕ → Set X), (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ (n : ℕ), K n = s
Tactic: rw [IsSigmaCompact] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : ∃ (K : ℕ → Set X), (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ (n : ℕ), K n = s
⊢ IsLindelof s
have rcases : ∀ (K : ℕ → Set X) (hc : ∀ (n : ℕ), IsCompact (K n)) (huniv : ⋃ (n : ℕ), K n = s), IsLindelof s
Tactic: rcases hs with ⟨K, ⟨hc, huniv⟩⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
K : ℕ → Set X
hc : ∀ (n : ℕ), IsCompact (K n)
huniv : ⋃ (n : ℕ), K n = s
⊢ IsLindelof s
have rw : IsLindelof.{u} (X := X) (⋃ (n : ℕ), K n)
Tactic: rw [← huniv]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
K : ℕ → Set X
hc : ∀ (n : ℕ), IsCompact (K n)
huniv : ⋃ (n : ℕ), K n = s
⊢ IsLindelof.{u} (X := X) (⋃ (n : ℕ), K n)
have hl : ∀ (n : ℕ), IsLindelof (K n)
Tactic: have hl : ∀ n, IsLindelof (K n) := fun n ↦ IsCompact.isLindelof (hc n)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : NonLindelofSpace X
⊢ (coLindelof X).NeBot
have refine : ∀ {s : Set X} (hs : IsLindelof s), sᶜ.Nonempty
Tactic: refine hasBasis_coLindelof.neBot_iff.2 fun {s} hs => ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s_1 t : Set X
inst_2 : NonLindelofSpace X
s : Set X
hs : IsLindelof s
⊢ sᶜ.Nonempty
have contrapose : ∀ (hs : ¬sᶜ.Nonempty), ¬IsLindelof s
Tactic: contrapose hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s_1 t : Set X
inst_2 : NonLindelofSpace X
s : Set X
hs : ¬sᶜ.Nonempty
⊢ ¬IsLindelof s
have hs₁ : s = univ
Tactic: rw [not_nonempty_iff_eq_empty, compl_empty_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s_1 t : Set X
inst_2 : NonLindelofSpace X
s : Set X
hs : s = univ
⊢ ¬IsLindelof s
have rw : ¬IsLindelof.{u} (X := X) univ
Tactic: rw [hs]
-- 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
hf : Continuous[inst, inst_1] f
⊢ comap f (coLindelof Y) ≤ coLindelof X
have rw : ∀ (i' : Set X), IsLindelof i' → ∃ (i : Set Y), IsLindelof i ∧ f ⁻¹' iᶜ ⊆ i'ᶜ
Tactic: rw [(hasBasis_coLindelof.comap f).le_basis_iff hasBasis_coLindelof]
-- 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
hf : Continuous[inst, inst_1] f
t : Set X
ht : IsLindelof t
⊢ ∃ (i : Set Y), IsLindelof i ∧ f ⁻¹' iᶜ ⊆ tᶜ
have refine : f ⁻¹' (f '' t)ᶜ ⊆ tᶜ
Tactic: refine ⟨f '' t, ht.image hf, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LindelofSpace X
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ IsLindelof (range f)
have rw : IsLindelof (f '' univ)
Tactic: rw [← image_univ]
-- 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
hf : IsInducing f
⊢ IsLindelof s ↔ IsLindelof (f '' s)
have refine : ∀ (hs : IsLindelof (f '' s)) (F : Filter X) (F_ne_bot : F.NeBot),
  CountableInterFilter F → ∀ (F_le : F ≤ 𝓟 s), ∃ x ∈ s, ClusterPt x F
Tactic: refine ⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot _ F_le => ?_⟩
-- 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
hf : IsInducing f
hs : IsLindelof (f '' s)
F : Filter X
F_ne_bot : F.NeBot
h : CountableInterFilter F
F_le : F ≤ 𝓟 s
⊢ ∃ x ∈ s, ClusterPt x F
have obtain : ∀ (x : X) (x_in : x ∈ s) (hx : ClusterPt (f x) (map f F)), ∃ x ∈ s, ClusterPt x F
Tactic: obtain ⟨_, ⟨x, x_in : x ∈ s, rfl⟩, hx : ClusterPt (f x) (map f F)⟩ :=
    hs ((map_mono F_le).trans_eq map_principal)
-- 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
hf : IsInducing f
hf' : IsClosed[inst_1] (range f)
K : Set Y
hK : IsLindelof K
⊢ IsLindelof (f ⁻¹' K)
have hK₁ : IsLindelof (K ∩ range f)
Tactic: replace hK := hK.inter_right hf'
Cleared hypotheses: hK
-- 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
hf : IsInducing f
hf' : IsClosed[inst_1] (range f)
K : Set Y
hK : IsLindelof (K ∩ range f)
⊢ IsLindelof (f ⁻¹' K)
have rwa : IsLindelof (f '' f ⁻¹' K)
Tactic: rwa [hf.isLindelof_iff, image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsLindelof s ↔ IsLindelof.{u} (X := (↑s : Type u)) univ
have rw : IsLindelof s ↔ IsLindelof.{u} (X := X) (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) univ)
Tactic: rw [Subtype.isLindelof_iff, image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw :
  IsLindelof s ↔ IsLindelof.{u} (X := X) (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) univ)
⊢ IsLindelof s ↔ IsLindelof.{u} (X := (↑s : Type u)) univ
have rw₁ : IsLindelof s ↔ IsLindelof.{u} (X := X) (range (ι := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)))
Tactic: rw [Subtype.isLindelof_iff, image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw :
  IsLindelof s ↔ IsLindelof.{u} (X := X) (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) univ)
rw₁ : IsLindelof s ↔ IsLindelof.{u} (X := X) (range (ι := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)))
⊢ IsLindelof s ↔ IsLindelof.{u} (X := (↑s : Type u)) univ
have rw₂ : IsLindelof s ↔ IsLindelof s
Tactic: rw [Subtype.isLindelof_iff, image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : LindelofSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsLindelof.{u} (X := X) univ
have rw : IsLindelof (range f)
Tactic: rw [hf.isInducing.isLindelof_iff, image_univ]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : LindelofSpace X
inst_3 : LindelofSpace Y
⊢ IsLindelof (X := X ⊕ Y) univ
have rw : IsLindelof (X := X ⊕ Y) (range Sum.inl ∪ range Sum.inr)
Tactic: rw [← range_inl_union_range_inr]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X_1 : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
X : ι → Type u_2
inst_2 : Countable ι
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LindelofSpace.{u_2} (X i)
⊢ IsLindelof (X := (i : ι) × X i) univ
have rw : IsLindelof (X := (i : ι) × X i) (⋃ (a : ι), range (Sigma.mk (β := fun (a : ι) ↦ X a) a))
Tactic: rw [Sigma.univ]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
r : X → X → Prop
inst_2 : LindelofSpace X
⊢ IsLindelof.{u} (X := Quot r) univ
have rw : IsLindelof (range (mk r))
Tactic: rw [← range_quot_mk]
-- 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
inst_2 : LindelofSpace X
hf : Continuous[inst, inst_1] f
hsur : Function.Surjective f
⊢ IsLindelof.{v} (X := Y) univ
have rw : IsLindelof (f '' univ)
Tactic: rw [← Set.image_univ_of_surjective hsur]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
s : Set X
⊢ IsLindelof s
have a : s ⊆ univ
Tactic: apply HereditarilyLindelofSpace.isHereditarilyLindelof_univ
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
H : ∀ (s : Set X), IsOpen[inst] s → IsLindelof s
⊢ HereditarilyLindelofSpace X
have refine : ∀ s ⊆ univ,
  ∀ {ι : Type u} (U : ι → Set X) (U_open : ∀ (i : ι), IsOpen[inst] (U i)) (hU : s ⊆ ⋃ (i : ι), U i),
    ∃ (t : Set ι), t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
Tactic: refine ⟨fun s _ ↦ isLindelof_of_countable_subcover fun U U_open hU ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
H : ∀ (s : Set X), IsOpen[inst] s → IsLindelof s
s : Set X
h : s ⊆ univ
ι : Type u
U : ι → Set X
U_open : ∀ (i : ι), IsOpen[inst] (U i)
hU : s ⊆ ⋃ (i : ι), U i
⊢ ∃ (t : Set ι), t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
have obtain : ∀ (t : Set ι) (t_count : t.Countable) (ht : Subset.{u} (α := Set X) (⋃ (i : ι), U i) (⋃ i ∈ t, U i)),
  ∃ (t : Set ι), t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
Tactic: obtain ⟨t, t_count, ht⟩ := H (⋃ i, U i) (isOpen_iUnion U_open)
    |>.elim_countable_subcover U U_open subset_rfl
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t_1 : Set X
inst_2 : SecondCountableTopology X
t : Set X
h : t ⊆ univ
x : Filter X
⊢ ∀ [x.NeBot] [CountableInterFilter x], x ≤ 𝓟 t → ∃ x_1 ∈ t, ClusterPt x_1 x
have a : ∀ {ι : Type u} (U : ι → Set X),
  (∀ (i : ι), IsOpen[inst] (U i)) → t ⊆ ⋃ (i : ι), U i → ∃ (t_2 : Set ι), t_2.Countable ∧ t ⊆ ⋃ i ∈ t_2, U i
Tactic: apply isLindelof_iff_countable_subcover.mpr
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
Goal:
X : Type u
Y : Type v
ι_1 : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t_1 : Set X
inst_2 : SecondCountableTopology X
t : Set X
h : t ⊆ univ
x : Filter X
ι : Type u
U : ι → Set X
hι : ∀ (i : ι), IsOpen[inst] (U i)
hcover : t ⊆ ⋃ (i : ι), U i
⊢ ∃ (t_2 : Set ι), t_2.Countable ∧ t ⊆ ⋃ i ∈ t_2, U i
have this : ∃ (T : Set ι), T.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ i ∈ T, U i) (⋃ (i : ι), U i)
Tactic: have := @isOpen_iUnion_countable X _ _ ι U hι
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
Y : Type v
ι_1 : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t_1 : Set X
inst_2 : SecondCountableTopology X
t : Set X
h : t ⊆ univ
x : Filter X
ι : Type u
U : ι → Set X
hι : ∀ (i : ι), IsOpen[inst] (U i)
hcover : t ⊆ ⋃ (i : ι), U i
this : ∃ (T : Set ι), T.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ i ∈ T, U i) (⋃ (i : ι), U i)
⊢ ∃ (t_2 : Set ι), t_2.Countable ∧ t ⊆ ⋃ i ∈ t_2, U i
have a : ∀ (t_2 : Set ι) (htc : t_2.Countable) (htu : Eq.{u + 1} (α := Set X) (⋃ i ∈ t_2, U i) (⋃ (i : ι), U i)),
  ∃ (t_3 : Set ι), t_3.Countable ∧ t ⊆ ⋃ i ∈ t_3, U i
Tactic: rcases this with ⟨t, ⟨htc, htu⟩⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
Y : Type v
ι_1 : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t_1 : Set X
inst_2 : SecondCountableTopology X
t_2 : Set X
h : t_2 ⊆ univ
x : Filter X
ι : Type u
U : ι → Set X
hι : ∀ (i : ι), IsOpen[inst] (U i)
hcover : t_2 ⊆ ⋃ (i : ι), U i
t : Set ι
htc : t.Countable
htu : Eq.{u + 1} (α := Set X) (⋃ i ∈ t, U i) (⋃ (i : ι), U i)
⊢ ∃ (t : Set ι), t.Countable ∧ t_2 ⊆ ⋃ i ∈ t, U i
have right : t_2 ⊆ ⋃ i ∈ t, U i
Tactic: use t, htc
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (U i)
⊢ ∃ (t : Set ι), t.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ i ∈ t, U i) (⋃ (i : ι), U i)
have this : IsLindelof.{u} (X := X) (⋃ (i : ι), U i)
Tactic: have : IsLindelof (⋃ i, U i) := HereditarilyLindelofSpace.isLindelof (⋃ i, U i)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (U i)
this : IsLindelof.{u} (X := X) (⋃ (i : ι), U i)
⊢ ∃ (t : Set ι), t.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ i ∈ t, U i) (⋃ (i : ι), U i)
have rcases : ∀ (t : Set ι) (htc : t.Countable) (htu : Subset.{u} (α := Set X) (⋃ (i : ι), U i) (⋃ i ∈ t, U i)),
  ∃ (t : Set ι), t.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ i ∈ t, U i) (⋃ (i : ι), U i)
Tactic: rcases this.elim_countable_subcover U h (Eq.subset rfl) with ⟨t, ⟨htc, htu⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (U i)
this : IsLindelof.{u} (X := X) (⋃ (i : ι), U i)
t : Set ι
htc : t.Countable
htu : Subset.{u} (α := Set X) (⋃ (i : ι), U i) (⋃ i ∈ t, U i)
⊢ ∃ (t : Set ι), t.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ i ∈ t, U i) (⋃ (i : ι), U i)
have right : Eq.{u + 1} (α := Set X) (⋃ i ∈ t, U i) (⋃ (i : ι), U i)
Tactic: use t, htc
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (U i)
⊢ ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)
have obtain : ∀ (t : Set ι) (htc : t.Countable) (htu : Eq.{u + 1} (α := Set X) (⋃ i ∈ t, U i) (⋃ (i : ι), U i)),
  ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)
Tactic: obtain ⟨t, htc, htu⟩ := eq_open_union_countable U h
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (U i)
t : Set ι
htc : t.Countable
htu : Eq.{u + 1} (α := Set X) (⋃ i ∈ t, U i) (⋃ (i : ι), U i)
⊢ ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)
have inl : ∀ (htc : Set.Countable.{u_2} (α := ι) ∅)
  (htu : Eq.{u + 1} (α := Set X) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ i), U i) (⋃ (i : ι), U i)),
  ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)
Tactic: rcases eq_empty_or_nonempty t with rfl | t_ne
Cleared hypotheses: t, htc, htu
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (U i)
t : Set ι
htc : t.Countable
htu : Eq.{u + 1} (α := Set X) (⋃ i ∈ t, U i) (⋃ (i : ι), U i)
inl :
  ∀ (htc : Set.Countable.{u_2} (α := ι) ∅)
    (htu : Eq.{u + 1} (α := Set X) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ i), U i) (⋃ (i : ι), U i)),
    ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)
⊢ ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)
have inr : ∀ (t_ne : t.Nonempty), ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)
Tactic: rcases eq_empty_or_nonempty t with rfl | t_ne
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (U i)
htc : Set.Countable.{u_2} (α := ι) ∅
htu : Eq.{u + 1} (α := Set X) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ i), U i) (⋃ (i : ι), U i)
⊢ ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)
have htu₁ : ∀ (i : ι), U i = ∅
Tactic: simp_rw [mem_empty_iff_false, iUnion_false, iUnion_empty, eq_comm (a := ∅), iUnion_eq_empty]
      at htu
Cleared hypotheses: htu
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (U i)
t : Set ι
htc : t.Countable
htu : Eq.{u + 1} (α := Set X) (⋃ i ∈ t, U i) (⋃ (i : ι), U i)
t_ne : t.Nonempty
⊢ ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)
have inr : ∀ (k : ℕ → ι) (htc : (range k).Countable) (htu : Eq.{u + 1} (α := Set X) (⋃ i ∈ range k, U i) (⋃ (i : ι), U i))
  (t_ne : (range k).Nonempty), ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)
Tactic: obtain ⟨k, rfl⟩ := htc.exists_eq_range t_ne
Cleared hypotheses: t, htc, htu, t_ne
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (U i)
k : ℕ → ι
htc : (range k).Countable
htu : Eq.{u + 1} (α := Set X) (⋃ i ∈ range k, U i) (⋃ (i : ι), U i)
t_ne : (range k).Nonempty
⊢ ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)
have h₁ : Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)
Tactic: use k
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (U i)
k : ℕ → ι
htc : (range k).Countable
htu : Eq.{u + 1} (α := Set X) (⋃ i ∈ range k, U i) (⋃ (i : ι), U i)
t_ne : (range k).Nonempty
⊢ Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)
have h₁ : ∀ (htu : Eq.{u + 1} (α := Set X) (⋃ (y : ℕ), U (k y)) (⋃ (i : ι), U i)) (t_ne : (range k).Nonempty),
  Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)
Tactic: rwa [biUnion_range] at htu
Cleared hypotheses: htu, t_ne
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (C i)
t : Set ι
| Eq.{u + 1} (α := Set X) (⋂ i ∈ t, C i) (⋂ (i : ι), C i)
have rw : Eq.{u + 1} (α := Set X) (⋂ i ∈ t, C i)ᶜ (⋂ (i : ι), C i)ᶜ
Tactic: rw [← compl_inj_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (C i)
t : Set ι
| Eq.{u + 1} (α := Set X) (⋂ i ∈ t, C i)ᶜ (⋂ (i : ι), C i)ᶜ
have simp : Eq.{u + 1} (α := Set X) (⋃ i ∈ t, (C i)ᶜ) (⋃ (i : ι), (C i)ᶜ)
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (C i)
t : Set ι
| Eq.{u + 1} (α := Set X) (⋂ i ∈ t, C i) (⋂ (i : ι), C i)
have rw : Eq.{u + 1} (α := Set X) (⋃ i ∈ t, (C i)ᶜ) (⋃ (i : ι), (C i)ᶜ)
Tactic: rw [← compl_inj_iff]; simp
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (C i)
⊢ ∃ (t : Set ι), t.Countable ∧ Eq.{u + 1} (α := Set X) (⋂ i ∈ t, C i) (⋂ (i : ι), C i)
have conv : ∃ (t : Set ι), t.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ i ∈ t, (C i)ᶜ) (⋃ (i : ι), (C i)ᶜ)
Tactic: conv in _ = _ => rw [← compl_inj_iff]; simp
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (C i)
k : ℕ → ι
| Eq.{u + 1} (α := Set X) (⋂ (n : ℕ), C (k n)) (⋂ (i : ι), C i)
have rw : Eq.{u + 1} (α := Set X) (⋂ (n : ℕ), C (k n))ᶜ (⋂ (i : ι), C i)ᶜ
Tactic: rw [← compl_inj_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (C i)
k : ℕ → ι
| Eq.{u + 1} (α := Set X) (⋂ (n : ℕ), C (k n))ᶜ (⋂ (i : ι), C i)ᶜ
have simp : Eq.{u + 1} (α := Set X) (⋃ (i : ℕ), (C (k i))ᶜ) (⋃ (i : ι), (C i)ᶜ)
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (C i)
k : ℕ → ι
| Eq.{u + 1} (α := Set X) (⋂ (n : ℕ), C (k n)) (⋂ (i : ι), C i)
have rw : Eq.{u + 1} (α := Set X) (⋃ (i : ℕ), (C (k i))ᶜ) (⋃ (i : ι), (C i)ᶜ)
Tactic: rw [← compl_inj_iff]; simp
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (C i)
⊢ ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋂ (n : ℕ), C (k n)) (⋂ (i : ι), C i)
have conv : ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (i : ℕ), (C (k i))ᶜ) (⋃ (i : ι), (C i)ᶜ)
Tactic: conv in _ = _ => rw [← compl_inj_iff]; simp
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
ι_1 : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
ι : Type u_4
inst_2 : Finite ι
X : ι → Type u_5
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_5} (X i)
f : (i : ι) → X i
⊢ ∃ (s : Set ((i : ι) → X i)), IsCompact s ∧ s ∈ 𝓝 f
have choose : ∀ (s : (i : ι) → Set (X i)) (hsc : ∀ (i : ι), IsCompact (s i)) (hs : ∀ (i : ι), s i ∈ 𝓝 (f i)),
  ∃ (s : Set ((i : ι) → X i)), IsCompact s ∧ s ∈ 𝓝 f
Tactic: choose s hsc hs using fun i ↦ exists_compact_mem_nhds (f i)
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
⊢ ∀ (x : Y), ∃ (s : Set Y), IsCompact s ∧ s ∈ 𝓝 x
have refine : ∀ (x : X), ∃ (s : Set Y), IsCompact s ∧ s ∈ 𝓝 (f x)
Tactic: refine hf.surjective.forall.2 fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
x : X
⊢ ∃ (s : Set Y), IsCompact s ∧ s ∈ 𝓝 (f x)
have rcases : ∀ (K : Set X) (hKc : IsCompact K) (hKx : K ∈ 𝓝 x), ∃ (s : Set Y), IsCompact s ∧ s ∈ 𝓝 (f x)
Tactic: rcases exists_compact_mem_nhds x with ⟨K, hKc, hKx⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
⊢ ∃ (K' : Set X), IsCompact K' ∧ K ⊆ interior K'
have choose : ∀ (s : (x : X) → Set X) (hc : ∀ (x : X), IsCompact (s x)) (hmem : ∀ (x : X), s x ∈ 𝓝 x),
  ∃ (K' : Set X), IsCompact K' ∧ K ⊆ interior K'
Tactic: choose s hc hmem using fun x : X ↦ exists_compact_mem_nhds x