awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
hl : IsLindelof A
ι : Type u_2
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hAU : A ⊆ ⋃ (i : ι), U i
⊢ ∃ (t : Finset ι), A ⊆ ⋃ i ∈ t, U i
have pos : ∀ (h : Nonempty ι), ∃ (t : Finset ι), A ⊆ ⋃ i ∈ t, U i
Tactic: by_cases! h : Nonempty ι
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
hl : IsLindelof A
ι : Type u_2
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hAU : A ⊆ ⋃ (i : ι), U i
pos : ∀ (h : Nonempty ι), ∃ (t : Finset ι), A ⊆ ⋃ i ∈ t, U i
⊢ ∃ (t : Finset ι), A ⊆ ⋃ i ∈ t, U i
have neg : ∀ (h : IsEmpty ι), ∃ (t : Finset ι), A ⊆ ⋃ i ∈ t, U i
Tactic: by_cases! h : Nonempty ι
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
hl : IsLindelof A
ι : Type u_2
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hAU : A ⊆ ⋃ (i : ι), U i
h : Nonempty ι
⊢ ∃ (t : Finset ι), A ⊆ ⋃ i ∈ t, U i
have pos : ∀ (f : ℕ → ι) (hf : A ⊆ ⋃ (n : ℕ), U (f n)), ∃ (t : Finset ι), A ⊆ ⋃ i ∈ t, U i
Tactic: obtain ⟨f, hf⟩ := hl.indexed_countable_subcover U hUo hAU
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
hl : IsLindelof A
ι : Type u_2
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hAU : A ⊆ ⋃ (i : ι), U i
h : Nonempty ι
f : ℕ → ι
hf : A ⊆ ⋃ (n : ℕ), U (f n)
⊢ ∃ (t : Finset ι), A ⊆ ⋃ i ∈ t, U i
have pos : ∀ (t : Finset ℕ) (ht : A ⊆ ⋃ i ∈ t, (U ∘ f) i), ∃ (t : Finset ι), A ⊆ ⋃ i ∈ t, U i
Tactic: obtain ⟨t, ht⟩ := isCountablyCompact_iff_countable_open_cover.1 hA (U ∘ f)
      (fun n => hUo (f n)) hf
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
A B : Set E
hA : IsCountablyCompact A
hB : IsCountablyCompact B
⊢ IsCountablyCompact (A ∪ B)
have rw : ∀
  (hA :
    ∀ (U : ℕ → Set E),
      (∀ (i : ℕ), IsOpen[inst] (U i)) → A ⊆ ⋃ (i : ℕ), U i → ∃ (t : Set ℕ), t.Finite ∧ A ⊆ ⋃ i ∈ t, U i)
  (hB :
    ∀ (U : ℕ → Set E),
      (∀ (i : ℕ), IsOpen[inst] (U i)) → B ⊆ ⋃ (i : ℕ), U i → ∃ (t : Set ℕ), t.Finite ∧ B ⊆ ⋃ i ∈ t, U i)
  (U : ℕ → Set E),
  (∀ (i : ℕ), IsOpen[inst] (U i)) → A ∪ B ⊆ ⋃ (i : ℕ), U i → ∃ (t : Set ℕ), t.Finite ∧ A ∪ B ⊆ ⋃ i ∈ t, U i
Tactic: rw [isCountablyCompact_iff_countable_open_cover'] at hA hB ⊢
Cleared hypotheses: hA, hB
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
A B : Set E
hA :
  ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst] (U i)) → A ⊆ ⋃ (i : ℕ), U i → ∃ (t : Set ℕ), t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
hB :
  ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst] (U i)) → B ⊆ ⋃ (i : ℕ), U i → ∃ (t : Set ℕ), t.Finite ∧ B ⊆ ⋃ i ∈ t, U i
U : ℕ → Set E
hUo : ∀ (i : ℕ), IsOpen[inst] (U i)
hAU : A ∪ B ⊆ ⋃ (i : ℕ), U i
⊢ ∃ (t : Set ℕ), t.Finite ∧ A ∪ B ⊆ ⋃ i ∈ t, U i
have obtain : ∀ (t₁ : Set ℕ) (ht₁ : t₁.Finite) (hA_sub : A ⊆ ⋃ k ∈ t₁, U k), ∃ (t : Set ℕ), t.Finite ∧ A ∪ B ⊆ ⋃ i ∈ t, U i
Tactic: obtain ⟨t₁, ht₁, hA_sub⟩ : ∃ (t₁ : Set ℕ), t₁.Finite ∧ A ⊆ ⋃ k ∈ t₁, U k :=
    hA U hUo (subset_union_left.trans hAU)
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
A B : Set E
hA :
  ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst] (U i)) → A ⊆ ⋃ (i : ℕ), U i → ∃ (t : Set ℕ), t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
hB :
  ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst] (U i)) → B ⊆ ⋃ (i : ℕ), U i → ∃ (t : Set ℕ), t.Finite ∧ B ⊆ ⋃ i ∈ t, U i
U : ℕ → Set E
hUo : ∀ (i : ℕ), IsOpen[inst] (U i)
hAU : A ∪ B ⊆ ⋃ (i : ℕ), U i
t₁ : Set ℕ
ht₁ : t₁.Finite
hA_sub : A ⊆ ⋃ k ∈ t₁, U k
⊢ ∃ (t : Set ℕ), t.Finite ∧ A ∪ B ⊆ ⋃ i ∈ t, U i
have obtain : ∀ (t₂ : Set ℕ) (ht₂ : t₂.Finite) (hB_sub : B ⊆ ⋃ k ∈ t₂, U k), ∃ (t : Set ℕ), t.Finite ∧ A ∪ B ⊆ ⋃ i ∈ t, U i
Tactic: obtain ⟨t₂, ht₂, hB_sub⟩ : ∃ (t₂ : Set ℕ), t₂.Finite ∧ B ⊆ ⋃ k ∈ t₂, U k :=
    hB U hUo (subset_union_right.trans hAU)
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
A B : Set E
hA :
  ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst] (U i)) → A ⊆ ⋃ (i : ℕ), U i → ∃ (t : Set ℕ), t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
hB :
  ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst] (U i)) → B ⊆ ⋃ (i : ℕ), U i → ∃ (t : Set ℕ), t.Finite ∧ B ⊆ ⋃ i ∈ t, U i
U : ℕ → Set E
hUo : ∀ (i : ℕ), IsOpen[inst] (U i)
hAU : A ∪ B ⊆ ⋃ (i : ℕ), U i
t₁ : Set ℕ
ht₁ : t₁.Finite
hA_sub : A ⊆ ⋃ k ∈ t₁, U k
t₂ : Set ℕ
ht₂ : t₂.Finite
hB_sub : B ⊆ ⋃ k ∈ t₂, U k
⊢ Eq.{u_2 + 1} (α := Set E) ((⋃ k ∈ t₁, U k) ∪ ⋃ k ∈ t₂, U k) (⋃ k ∈ t₁ ∪ t₂, U k)
have h : ∀ (x : E),
  Membership.mem (γ := Set E) ((⋃ k ∈ t₁, U k) ∪ ⋃ k ∈ t₂, U k) x ↔ Membership.mem (γ := Set E) (⋃ k ∈ t₁ ∪ t₂, U k) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (hypothesis)
Goal:
E : Type u_2
inst : TopologicalSpace E
A B : Set E
hA :
  ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst] (U i)) → A ⊆ ⋃ (i : ℕ), U i → ∃ (t : Set ℕ), t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
hB :
  ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst] (U i)) → B ⊆ ⋃ (i : ℕ), U i → ∃ (t : Set ℕ), t.Finite ∧ B ⊆ ⋃ i ∈ t, U i
U : ℕ → Set E
hUo : ∀ (i : ℕ), IsOpen[inst] (U i)
hAU : A ∪ B ⊆ ⋃ (i : ℕ), U i
t₁ : Set ℕ
ht₁ : t₁.Finite
hA_sub : A ⊆ ⋃ k ∈ t₁, U k
t₂ : Set ℕ
ht₂ : t₂.Finite
hB_sub : B ⊆ ⋃ k ∈ t₂, U k
⊢ ∃ (t : Set ℕ), t.Finite ∧ A ∪ B ⊆ ⋃ i ∈ t, U i
have h : Eq.{u_2 + 1} (α := Set E) ((⋃ k ∈ t₁, U k) ∪ ⋃ k ∈ t₂, U k) (⋃ k ∈ t₁ ∪ t₂, U k)
Tactic: have h : (⋃ k ∈ t₁, U k) ∪ (⋃ k ∈ t₂, U k) = ⋃ k ∈ (t₁ ∪ t₂), U k := by ext; aesop
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
s : Finset ι
f : ι → Set E
hf : ∀ i ∈ s, IsCountablyCompact (f i)
⊢ IsCountablyCompact.{u_2} (E := E) (⋃ i ∈ s, f i)
have empty : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsCountablyCompact (f i)),
  IsCountablyCompact.{u_2} (E := E) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), f i)
Tactic: induction s using Finset.induction_on with
  | empty => simpa using isCountablyCompact_empty
  | @insert a s ha ih => simpa [Finset.biUnion_insert] using
    (hf a (Finset.mem_insert_self a s)).union <| ih (fun i hi => hf i (Finset.mem_insert_of_mem hi))
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
s : Finset ι
f : ι → Set E
hf : ∀ i ∈ s, IsCountablyCompact (f i)
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsCountablyCompact (f i)),
    IsCountablyCompact.{u_2} (E := E) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), f i)
⊢ IsCountablyCompact.{u_2} (E := E) (⋃ i ∈ s, f i)
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (ih : ∀ (hf : ∀ i ∈ s, IsCountablyCompact (f i)), IsCountablyCompact.{u_2} (E := E) (⋃ i ∈ s, f i))
  (hf : ∀ i ∈ insert a s, IsCountablyCompact (f i)), IsCountablyCompact.{u_2} (E := E) (⋃ i ∈ insert a s, f i)
Tactic: induction s using Finset.induction_on with
  | empty => simpa using isCountablyCompact_empty
  | @insert a s ha ih => simpa [Finset.biUnion_insert] using
    (hf a (Finset.mem_insert_self a s)).union <| ih (fun i hi => hf i (Finset.mem_insert_of_mem hi))
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
s : Finset ι
f : ι → Set E
hf : ∀ i ∈ s, IsCountablyCompact (f i)
⊢ IsCountablyCompact.{u_2} (E := E) (⋃ i ∈ s, f i)
have empty : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsCountablyCompact (f i)),
  IsCountablyCompact.{u_2} (E := E) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), f i)
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simpa using isCountablyCompact_empty
  | @insert a s ha ih => simpa [Finset.biUnion_insert] using
    (hf a (Finset.mem_insert_self a s)).union <| ih (fun i hi => hf i (Finset.mem_insert_of_mem hi))
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
s : Finset ι
f : ι → Set E
hf : ∀ i ∈ s, IsCountablyCompact (f i)
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsCountablyCompact (f i)),
    IsCountablyCompact.{u_2} (E := E) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), f i)
⊢ IsCountablyCompact.{u_2} (E := E) (⋃ i ∈ s, f i)
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (ih : ∀ (hf : ∀ i ∈ s, IsCountablyCompact (f i)), IsCountablyCompact.{u_2} (E := E) (⋃ i ∈ s, f i))
  (hf : ∀ i ∈ insert a s, IsCountablyCompact (f i)), IsCountablyCompact.{u_2} (E := E) (⋃ i ∈ insert a s, f i)
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simpa using isCountablyCompact_empty
  | @insert a s ha ih => simpa [Finset.biUnion_insert] using
    (hf a (Finset.mem_insert_self a s)).union <| ih (fun i hi => hf i (Finset.mem_insert_of_mem hi))
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (hypothesis)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
s : Set ι
f : ι → Set E
hs : s.Finite
hf : ∀ i ∈ s, IsCountablyCompact (f i)
s' : Finset ι := hs.toFinset (s := s)
⊢ IsCountablyCompact.{u_2} (E := E) (⋃ i ∈ s, f i)
have h1 : Eq.{u_2 + 1} (α := Set E) (⋃ i ∈ s, f i) (⋃ i ∈ s', f i)
Tactic: have h1 : (⋃ i ∈ s, f i) = (⋃ i ∈ s', f i) := by simp [s']
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
S : Set (Set E)
hf : S.Finite
hc : ∀ s ∈ S, IsCountablyCompact s
⊢ IsCountablyCompact (⋃₀ S)
have rw : IsCountablyCompact.{u_2} (E := E) (⋃ i ∈ S, i)
Tactic: rw [sUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.Topology.Compactness.DeltaGeneratedSpace (goal)
Goal:
X : Type u_1
tX : TopologicalSpace X
⊢ deltaGenerated X =
    coinduced
      (fun (x : (f : (n : ℕ) × C(Fin n → ℝ, X)) × (Fin (f.fst (β := fun (n : ℕ) ↦ C(Fin n → ℝ, X))) → ℝ)) ↦
        (x.fst (β := fun (f : (n : ℕ) × C(Fin n → ℝ, X)) ↦ Fin (f.fst (β := fun (n : ℕ) ↦ C(Fin n → ℝ, X))) → ℝ).snd
              (β := fun (n : ℕ) ↦ C(Fin n → ℝ, X)) :
            (a : Fin x.fst.fst → ℝ) → X)
          (x.snd (β := fun (f : (n : ℕ) × C(Fin n → ℝ, X)) ↦ Fin (f.fst (β := fun (n : ℕ) ↦ C(Fin n → ℝ, X))) → ℝ)))
      inferInstance
have rw : Eq.{u_1 + 1} (α := TopologicalSpace X)
  (⨆ (f : (n : ℕ) × C(Fin n → ℝ, X)),
    coinduced (X := Fin (f.fst (β := fun (n : ℕ) ↦ C(Fin n → ℝ, X))) → ℝ)
      (⇑(f.snd (β := fun (n : ℕ) ↦ C(Fin n → ℝ, X))) : (a : Fin f.fst → ℝ) → X) inferInstance)
  (⨆ (i : (n : ℕ) × C(Fin n → ℝ, X)),
    coinduced
      (fun (x : (f : (n : ℕ) × C(Fin n → ℝ, X)) × (Fin (f.fst (β := fun (n : ℕ) ↦ C(Fin n → ℝ, X))) → ℝ)) ↦
        (x.fst (β := fun (f : (n : ℕ) × C(Fin n → ℝ, X)) ↦ Fin (f.fst (β := fun (n : ℕ) ↦ C(Fin n → ℝ, X))) → ℝ).snd
              (β := fun (n : ℕ) ↦ C(Fin n → ℝ, X)) :
            (a : Fin x.fst.fst → ℝ) → X)
          (x.snd (β := fun (f : (n : ℕ) × C(Fin n → ℝ, X)) ↦ Fin (f.fst (β := fun (n : ℕ) ↦ C(Fin n → ℝ, X))) → ℝ)))
      (coinduced
        (Sigma.mk (β := fun (f : (n : ℕ) × C(Fin n → ℝ, X)) ↦ Fin (f.fst (β := fun (n : ℕ) ↦ C(Fin n → ℝ, X))) → ℝ) i)
        (Pi.topologicalSpace (Y := fun (a : Fin (i.fst (β := fun (n : ℕ) ↦ C(Fin n → ℝ, X)))) ↦ ℝ))))
Tactic: rw [deltaGenerated, instTopologicalSpaceSigma, coinduced_iSup]
-- Lean 4 proof step from Mathlib.Topology.Compactness.DeltaGeneratedSpace (goal)
Goal:
X : Type u_1
tX : TopologicalSpace X
u : Set X
simp_rw :
  IsOpen[⨆ (f : (n : ℕ) × C(Fin n → ℝ, X)), coinduced (⇑f.snd : (a : Fin f.fst → ℝ) → X) inferInstance] u ↔
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)
⊢ IsOpen[deltaGenerated X] u ↔
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)
have simp_rw₁ : (∀ (i : (n : ℕ) × C(Fin n → ℝ, X)), IsOpen[coinduced (⇑i.snd : (a : Fin i.fst → ℝ) → X) inferInstance] u) ↔
  ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)
Tactic: simp_rw +instances [deltaGenerated, isOpen_iSup_iff, isOpen_coinduced, Sigma.forall]
-- Lean 4 proof step from Mathlib.Topology.Compactness.DeltaGeneratedSpace (goal)
Goal:
X : Type u_1
tX : TopologicalSpace X
u : Set X
simp_rw :
  IsOpen[⨆ (f : (n : ℕ) × C(Fin n → ℝ, X)), coinduced (⇑f.snd : (a : Fin f.fst → ℝ) → X) inferInstance] u ↔
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)
simp_rw₁ :
  (∀ (i : (n : ℕ) × C(Fin n → ℝ, X)), IsOpen[coinduced (⇑i.snd : (a : Fin i.fst → ℝ) → X) inferInstance] u) ↔
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)
⊢ IsOpen[deltaGenerated X] u ↔
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)
have simp_rw₂ : (∀ (i : (n : ℕ) × C(Fin n → ℝ, X)),
    IsOpen (X := Fin (i.fst (β := fun (n : ℕ) ↦ C(Fin n → ℝ, X))) → ℝ)
      ((⇑(i.snd (β := fun (n : ℕ) ↦ C(Fin n → ℝ, X))) : (a : Fin i.fst → ℝ) → X) ⁻¹' u)) ↔
  ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)
Tactic: simp_rw +instances [deltaGenerated, isOpen_iSup_iff, isOpen_coinduced, Sigma.forall]
-- Lean 4 proof step from Mathlib.Topology.Compactness.DeltaGeneratedSpace (goal)
Goal:
X : Type u_1
tX : TopologicalSpace X
n : ℕ
f : (Fin n → ℝ) → X
⊢ Continuous[_, deltaGenerated X] f ↔ Continuous[_, tX] f
have simp_rw : coinduced f (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤ deltaGenerated X ↔
  coinduced f (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤ tX
Tactic: simp_rw [continuous_iff_coinduced_le]
-- Lean 4 proof step from Mathlib.Topology.Compactness.DeltaGeneratedSpace (goal)
Goal:
X : Type u_1
tX : TopologicalSpace X
n : ℕ
f : (Fin n → ℝ) → X
⊢ coinduced f (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤ deltaGenerated X ↔
    coinduced f (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤ tX
have refine : ∀ (h : coinduced f (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤ tX),
  coinduced f (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤ deltaGenerated X
Tactic: refine ⟨fun h ↦ h.trans deltaGenerated_le, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.DeltaGeneratedSpace (goal)
Goal:
X : Type u_1
tX : TopologicalSpace X
⊢ deltaGenerated X = deltaGenerated X
have a : ∀ (u : Set X), IsOpen[deltaGenerated X] u ↔ IsOpen[deltaGenerated X] u
Tactic: ext u
-- Lean 4 proof step from Mathlib.Topology.Compactness.DeltaGeneratedSpace (goal)
Goal:
X : Type u_1
tX : TopologicalSpace X
u : Set X
⊢ IsOpen[deltaGenerated X] u ↔ IsOpen[deltaGenerated X] u
have a : (∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)) ↔
  ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)
Tactic: simp_rw [isOpen_deltaGenerated_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.DeltaGeneratedSpace (goal)
Goal:
X : Type u_1
tX : TopologicalSpace X
u : Set X
⊢ (∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)) ↔
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)
have a : ∀ (n : ℕ),
  (∀ (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)) ↔
    ∀ (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)
Tactic: refine forall_congr' fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.DeltaGeneratedSpace (goal)
Goal:
X : Type u_1
tX : TopologicalSpace X
u : Set X
n : ℕ
⊢ (∀ (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)) ↔
    ∀ (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)
have a : ∀ (h : ∀ (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)) (p : C(Fin n → ℝ, X)),
  Continuous[_, deltaGenerated X] (⇑p : (a : Fin n → ℝ) → X)
Tactic: refine ⟨fun h p ↦ h <| @ContinuousMap.mk _ _ _ (_) p ?_, fun h p ↦ h ⟨p, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.DeltaGeneratedSpace (goal)
Goal:
X : Type u_1
tX : TopologicalSpace X
u : Set X
n : ℕ
a :
  ∀ (h : ∀ (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)) (p : C(Fin n → ℝ, X)),
    Continuous[_, deltaGenerated X] (⇑p : (a : Fin n → ℝ) → X)
⊢ (∀ (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)) ↔
    ∀ (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)
have a₁ : ∀ (h : ∀ (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)) (p : C(Fin n → ℝ, X)),
  Continuous[_, tX] (⇑p : (a : Fin n → ℝ) → X)
Tactic: refine ⟨fun h p ↦ h <| @ContinuousMap.mk _ _ _ (_) p ?_, fun h p ↦ h ⟨p, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.DeltaGeneratedSpace (goal)
Goal:
X : Type u_1
tX : TopologicalSpace X
inst : DeltaGeneratedSpace X
u : Set X
⊢ IsOpen[tX] u ↔ ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)
have nth_rewrite : IsOpen[deltaGenerated X] u ↔ ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)
Tactic: nth_rewrite 1 [eq_deltaGenerated (X := X)]
-- Lean 4 proof step from Mathlib.Topology.Compactness.DeltaGeneratedSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : DeltaGeneratedSpace X
f : X → Y
⊢ Continuous[tX, tY] f ↔ ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), Continuous[_, tY] (f ∘ (⇑p : (a : Fin n → ℝ) → X))
have simp_rw : coinduced f tX ≤ tY ↔
  ∀ (n : ℕ) (p : C(Fin n → ℝ, X)),
    coinduced (X := Fin n → ℝ) (f ∘ (⇑p : (a : Fin n → ℝ) → X)) (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤ tY
Tactic: simp_rw [continuous_iff_coinduced_le]
-- Lean 4 proof step from Mathlib.Topology.Compactness.DeltaGeneratedSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : DeltaGeneratedSpace X
f : X → Y
⊢ coinduced f tX ≤ tY ↔
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)),
      coinduced (X := Fin n → ℝ) (f ∘ (⇑p : (a : Fin n → ℝ) → X)) (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤ tY
have nth_rewrite : coinduced f
      (⨆ (f : (n : ℕ) × C(Fin n → ℝ, X)),
        coinduced (X := Fin (f.fst (β := fun (n : ℕ) ↦ C(Fin n → ℝ, X))) → ℝ)
          (⇑(f.snd (β := fun (n : ℕ) ↦ C(Fin n → ℝ, X))) : (a : Fin f.fst → ℝ) → X) inferInstance) ≤
    tY ↔
  ∀ (n : ℕ) (p : C(Fin n → ℝ, X)),
    coinduced (X := Fin n → ℝ) (f ∘ (⇑p : (a : Fin n → ℝ) → X)) (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤ tY
Tactic: nth_rewrite 1 [eq_deltaGenerated (X := X), deltaGenerated]
-- Lean 4 proof step from Mathlib.Topology.Compactness.DeltaGeneratedSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : DeltaGeneratedSpace X
f : X → Y
⊢ Continuous[tX, deltaGenerated Y] f ↔ Continuous[tX, tY] f
have simp_rw : (∀ (n : ℕ) (p : C(Fin n → ℝ, X)), Continuous[_, deltaGenerated Y] (f ∘ (⇑p : (a : Fin n → ℝ) → X))) ↔
  ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), Continuous[_, tY] (f ∘ (⇑p : (a : Fin n → ℝ) → X))
Tactic: simp_rw [DeltaGeneratedSpace.continuous_iff, continuous_euclidean_to_deltaGenerated]
-- Lean 4 proof step from Mathlib.Topology.Compactness.DeltaGeneratedSpace (goal)
Goal:
X : Type u_3
t : TopologicalSpace X
x : TopologicalSpace X := deltaGenerated X
⊢ DeltaGeneratedSpace X
have le_deltaGenerated : deltaGenerated X ≤ deltaGenerated X
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Compactness.DeltaGeneratedSpace (goal)
Goal:
X : Type u_3
t : TopologicalSpace X
x : TopologicalSpace X := deltaGenerated X
⊢ deltaGenerated X ≤ deltaGenerated X
have le_deltaGenerated : deltaGenerated X ≤ deltaGenerated X
Tactic: rw [@deltaGenerated_deltaGenerated_eq X t]
-- Lean 4 proof step from Mathlib.Topology.Compactness.DeltaGeneratedSpace (goal)
Goal:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h : t₁ ≤ t₂
⊢ deltaGenerated X ≤ deltaGenerated X
have rw : Continuous[deltaGenerated X, t₂] id
Tactic: rw [← continuous_id_iff_le, @continuous_to_deltaGenerated _ _
    (@deltaGenerated X t₁) t₂ deltaGeneratedSpace_deltaGenerated id]
-- Lean 4 proof step from Mathlib.Topology.Compactness.DeltaGeneratedSpace (goal)
Goal:
X : Type u_1
tX : TopologicalSpace X
⊢ Continuous[instTopologicalSpaceOf, tX] counit
have rw : coinduced counit instTopologicalSpaceOf ≤ tX
Tactic: rw [continuous_iff_coinduced_le]
-- Lean 4 proof step from Mathlib.Topology.Compactness.DeltaGeneratedSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : DeltaGeneratedSpace X
⊢ LocPathConnectedSpace X
have rw : LocPathConnectedSpace X
Tactic: rw [eq_deltaGenerated (X := X), deltaGenerated_eq_coinduced]
-- Lean 4 proof step from Mathlib.Topology.Compactness.DeltaGeneratedSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : DeltaGeneratedSpace X
⊢ SequentialSpace X
have rw : SequentialSpace X
Tactic: rw [eq_deltaGenerated (X := X)]
-- Lean 4 proof step from Mathlib.Topology.Compactness.DeltaGeneratedSpace (goal)
Goal:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : DeltaGeneratedSpace X
h₂ : DeltaGeneratedSpace X
⊢ DeltaGeneratedSpace X
have rw : DeltaGeneratedSpace X
Tactic: rw [sup_eq_iSup]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst_1 : CountableInterFilter f
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.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst_1 : CountableInterFilter f
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.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst_1 : CountableInterFilter f
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.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst_1 : CountableInterFilter f
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
⊢ sᶜ ∈ 𝓝 x ⊓ f
have rw : ∃ i ∈ 𝓝 x ⊓ 𝓟 s, (id i)ᶜ ∈ f
Tactic: rw [← disjoint_principal_right, disjoint_right_comm, (basis_sets _).disjoint_iff_left]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Lindelof (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
p : Set X → Prop
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := ofCountableUnion {t : Set X | p t} hcountable_union ⋯
⊢ 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.Lindelof (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
p : Set X → Prop
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := ofCountableUnion {t : Set X | p t} hcountable_union ⋯
this : sᶜ ∈ f
⊢ p s
have rwa : p sᶜᶜ
Tactic: rwa [← compl_compl s]