awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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)
pos : ∀ (t : Finset ℕ) (ht : A ⊆ ⋃ i ∈ t, (U ∘ f) i), ∃ (t : Finset ι), A ⊆ ⋃ i ∈ t, U 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

Premises used: Function.comp, isCountablyCompact_iff_countable_open_cover, Iff.mp
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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 ℕ
ht : A ⊆ ⋃ i ∈ t, (U ∘ f) i
⊢ A ⊆ ⋃ i ∈ Finset.image f t, U i

Tactic:
simp_all
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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 ℕ
ht : A ⊆ ⋃ i ∈ t, (U ∘ f) i
⊢ ∃ (t : Finset ι), A ⊆ ⋃ i ∈ t, U i

Tactic:
exact ⟨t.image f, by simp_all⟩
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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 ℕ
ht : A ⊆ ⋃ i ∈ t, (U ∘ f) i
⊢ ∃ (t : Finset ι), A ⊆ ⋃ i ∈ t, U i

Tactic:
classical
    exact ⟨t.image f, by simp_all⟩
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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 : IsEmpty ι
⊢ A ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), U i

Tactic:
simp_all
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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 : IsEmpty ι
⊢ ∃ (t : Finset ι), A ⊆ ⋃ i ∈ t, U i

Tactic:
exact ⟨∅, by simp_all⟩
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
inst_1 : HereditarilyLindelofSpace E
hA : IsCountablyCompact A
⊢ IsCompact A

Tactic:
(HereditarilyLindelofSpace.isLindelof A).isCompact hA

Premises used: HereditarilyLindelofSpace.isLindelof, IsLindelof.isCompact
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A B : Set E
hA : IsCountablyCompact A
hB : IsCountablyCompact B
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
⊢ IsCountablyCompact (A ∪ B)

Tactic:
rw [isCountablyCompact_iff_countable_open_cover'] at hA hB ⊢

Premises used: isCountablyCompact_iff_countable_open_cover'
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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 ⊆ ⋃ k ∈ t₁, U k

Tactic:
hA U hUo (subset_union_left.trans hAU)

Premises used: HasSubset.Subset.trans, Set.subset_union_left
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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
obtain : ∀ (t₁ : Set ℕ) (ht₁ : t₁.Finite) (hA_sub : A ⊆ ⋃ k ∈ t₁, U k), ∃ (t : Set ℕ), t.Finite ∧ A ∪ B ⊆ ⋃ i ∈ t, U i
⊢ ∃ (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)

Premises used: HasSubset.Subset.trans, Set.subset_union_left, Nat, Set
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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 ∧ B ⊆ ⋃ k ∈ t₂, U k

Tactic:
hB U hUo (subset_union_right.trans hAU)

Premises used: Set.subset_union_right, HasSubset.Subset.trans
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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
obtain : ∀ (t₂ : Set ℕ) (ht₂ : t₂.Finite) (hB_sub : B ⊆ ⋃ k ∈ t₂, U k), ∃ (t : Set ℕ), t.Finite ∧ A ∪ B ⊆ ⋃ i ∈ t, U i
⊢ ∃ (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)

Premises used: Set.subset_union_right, HasSubset.Subset.trans, Nat, Set
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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
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
⊢ Eq.{u_2 + 1} (α := Set E) ((⋃ k ∈ t₁, U k) ∪ ⋃ k ∈ t₂, U k) (⋃ k ∈ t₁ ∪ t₂, U k)

Tactic:
ext
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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
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:
aesop
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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)

Tactic:
have h : (⋃ k ∈ t₁, U k) ∪ (⋃ k ∈ t₂, U k) = ⋃ k ∈ (t₁ ∪ t₂), U k := by ext; aesop
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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
h : Eq.{u_2 + 1} (α := Set E) ((⋃ k ∈ t₁, U k) ∪ ⋃ k ∈ t₂, U k) (⋃ k ∈ t₁ ∪ t₂, U k)
⊢ ∃ (t : Set ℕ), t.Finite ∧ A ∪ B ⊆ ⋃ i ∈ t, U i

Tactic:
⟨t₁ ∪ t₂, ht₁.union ht₂, h ▸ union_subset_union hA_sub hB_sub⟩

Premises used: Set.Finite.union, Set.union_subset_union, Eq.rec, And.intro, Exists.intro, Union.union
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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
h : Eq.{u_2 + 1} (α := Set E) ((⋃ k ∈ t₁, U k) ∪ ⋃ k ∈ t₂, U k) (⋃ k ∈ t₁ ∪ t₂, U k)
⊢ ∃ (t : Set ℕ), t.Finite ∧ A ∪ B ⊆ ⋃ i ∈ t, U i

Tactic:
exact ⟨t₁ ∪ t₂, ht₁.union ht₂, h ▸ union_subset_union hA_sub hB_sub⟩
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
f : ι → Set E
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsCountablyCompact (f i)
⊢ IsCountablyCompact.{u_2} (E := E) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), f i)

Tactic:
simpa using isCountablyCompact_empty

Premises used: isCountablyCompact_empty
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
f : ι → Set E
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:
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))

Premises used: Finset.mem_insert_self, IsCountablyCompact.union, Finset.biUnion_insert, Finset.mem_insert_of_mem
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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)
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.insert a s, IsCountablyCompact (f i)),
    IsCountablyCompact.{u_2} (E := E) (⋃ i ∈ Insert.insert a s, f i)
⊢ IsCountablyCompact.{u_2} (E := E) (⋃ i ∈ 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))

Premises used: Insert.insert, Finset.biUnion_insert, isCountablyCompact_empty
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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)
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.insert a s, IsCountablyCompact (f i)),
    IsCountablyCompact.{u_2} (E := E) (⋃ i ∈ Insert.insert a s, f i)
⊢ IsCountablyCompact.{u_2} (E := E) (⋃ i ∈ 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))

Premises used: Insert.insert, Finset.biUnion_insert, isCountablyCompact_empty
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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)
⊢ Eq.{u_2 + 1} (α := Set E) (⋃ i ∈ s, f i) (⋃ i ∈ s', f i)

Tactic:
simp [s']
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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)
⊢ 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']
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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)
h1 : Eq.{u_2 + 1} (α := Set E) (⋃ i ∈ s, f i) (⋃ i ∈ s', f i)
⊢ IsCountablyCompact.{u_2} (E := E) (⋃ i ∈ s, f i)

Tactic:
h1 ▸ Finset.isCountablyCompact_biUnion s' (fun i hi => hf i ((hs.mem_toFinset).mp hi))

Premises used: Set.Finite.mem_toFinset, Eq.rec, Finset.isCountablyCompact_biUnion, Iff.mp, Eq.symm
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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)
h1 : Eq.{u_2 + 1} (α := Set E) (⋃ i ∈ s, f i) (⋃ i ∈ s', f i)
⊢ IsCountablyCompact.{u_2} (E := E) (⋃ i ∈ s, f i)

Tactic:
exact h1 ▸ Finset.isCountablyCompact_biUnion s' (fun i hi => hf i ((hs.mem_toFinset).mp hi))
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
S : Set (Set E)
hf : S.Finite
hc : ∀ s ∈ S, IsCountablyCompact s
rw : IsCountablyCompact.{u_2} (E := E) (⋃ i ∈ S, i)
⊢ IsCountablyCompact (⋃₀ S)

Tactic:
rw [sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
S : Set (Set E)
hf : S.Finite
hc : ∀ s ∈ S, IsCountablyCompact s
⊢ IsCountablyCompact.{u_2} (E := E) (⋃ i ∈ S, i)

Tactic:
hf.isCountablyCompact_biUnion hc

Premises used: Set.Finite.isCountablyCompact_biUnion
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
S : Set (Set E)
hf : S.Finite
hc : ∀ s ∈ S, IsCountablyCompact s
⊢ IsCountablyCompact.{u_2} (E := E) (⋃ i ∈ S, i)

Tactic:
exact hf.isCountablyCompact_biUnion hc

Premises used: Set.Finite.isCountablyCompact_biUnion
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
ι : Sort u_4
f : ι → Set E
inst_1 : Finite ι
h : ∀ (i : ι), IsCountablyCompact (f i)
⊢ IsCountablyCompact.{u_2} (E := E) (⋃ (i : ι), f i)

Tactic:
(finite_range f).isCountablyCompact_sUnion <| forall_mem_range.2 h

Premises used: Iff.mpr, Set.forall_mem_range, Set.Mem, iSup, setOf, Set.finite_range, Set.Finite.isCountablyCompact_sUnion, Set.iUnion
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
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)))) ↦ ℝ))))
⊢ 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

Tactic:
rw [deltaGenerated, instTopologicalSpaceSigma, coinduced_iSup]

Premises used: TopologicalSpace.deltaGenerated, instTopologicalSpaceSigma, coinduced_iSup
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
⊢ 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:
rfl
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
⊢ deltaGenerated X ≤ tX

Tactic:
iSup_le_iff.mpr fun f ↦ f.2.continuous.coinduced_le

Premises used: Iff.mpr, ContinuousMap.continuous, iSup_le_iff, Sigma.snd, Continuous.coinduced_le
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
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)
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)
⊢ IsOpen[deltaGenerated 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]

Premises used: Sigma.forall, TopologicalSpace.deltaGenerated, isOpen_iSup_iff, isOpen_coinduced
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
n : ℕ
f : (Fin n → ℝ) → X
simp_rw :
  coinduced f (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤ deltaGenerated X ↔
    coinduced f (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤ tX
⊢ Continuous[_, deltaGenerated X] f ↔ Continuous[_, tX] f

Tactic:
simp_rw [continuous_iff_coinduced_le]

Premises used: continuous_iff_coinduced_le
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
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

Tactic:
⟨fun h ↦ h.trans deltaGenerated_le, fun h ↦ ?_⟩

Premises used: deltaGenerated_le, Iff.intro, LE.le.trans
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
n : ℕ
f : (Fin n → ℝ) → X
refine :
  ∀ (h : coinduced f (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤ tX),
    coinduced f (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤ deltaGenerated X
⊢ coinduced f (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤ deltaGenerated X ↔
    coinduced f (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤ tX

Tactic:
refine ⟨fun h ↦ h.trans deltaGenerated_le, fun h ↦ ?_⟩
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
n : ℕ
f : (Fin n → ℝ) → X
h : coinduced f (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤ tX
⊢ coinduced f (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤
    ⨆ (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

Tactic:
le_iSup_of_le (i := ⟨n, f, continuous_iff_coinduced_le.mpr h⟩) le_rfl

Premises used: Iff.mpr, le_rfl, ContinuousMap.mk, le_iSup_of_le, Sigma.mk, continuous_iff_coinduced_le
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
n : ℕ
f : (Fin n → ℝ) → X
h : coinduced f (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤ tX
⊢ coinduced f (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤
    ⨆ (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

Tactic:
exact le_iSup_of_le (i := ⟨n, f, continuous_iff_coinduced_le.mpr h⟩) le_rfl

Premises used: le_rfl, le_iSup_of_le
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
a : ∀ (u : Set X), IsOpen[deltaGenerated X] u ↔ IsOpen[deltaGenerated X] u
⊢ deltaGenerated X = deltaGenerated X

Tactic:
ext u
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
u : Set X
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)
⊢ IsOpen[deltaGenerated X] u ↔ IsOpen[deltaGenerated X] u

Tactic:
simp_rw [isOpen_deltaGenerated_iff]

Premises used: isOpen_deltaGenerated_iff