awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
⊢ IsSigmaCompact s → IsSigmaCompact (f '' s)

Tactic:
fun h ↦ h.image hf.continuous

Premises used: IsSigmaCompact.image, Topology.IsInducing.continuous
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
⊢ IsSigmaCompact s → IsSigmaCompact (f '' s)

Tactic:
exact fun h ↦ h.image hf.continuous
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ (n : ℕ), L n = f '' s
⊢ IsSigmaCompact s

Tactic:
⟨fun n ↦ f ⁻¹' (L n) ∩ s, ?_, ?_⟩

Premises used: IsSigmaCompact, Inter.inter, Set.preimage, And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ (n : ℕ), L n = f '' s
mpr : ∀ (n : ℕ), IsCompact.{u_1} (X := X) ((fun (n : ℕ) ↦ f ⁻¹' L n ∩ s) n)
mpr₁ : ⋃ (n : ℕ), (fun (n : ℕ) ↦ f ⁻¹' L n ∩ s) n = s
⊢ IsSigmaCompact s

Tactic:
refine ⟨fun n ↦ f ⁻¹' (L n) ∩ s, ?_, ?_⟩
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ (n : ℕ), L n = f '' s
n : ℕ
rw : L n ⊆ f '' s
⊢ f '' (f ⁻¹' L n ∩ s) = L n

Tactic:
rw [image_preimage_inter, inter_eq_left.mpr]

Premises used: Set.inter_eq_left, Iff.mpr, Set.image_preimage_inter
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ (n : ℕ), L n = f '' s
n : ℕ
⊢ L n ⊆ f '' s

Tactic:
(subset_iUnion _ n).trans hcov.le

Premises used: HasSubset.Subset.trans, Eq.le, Set.subset_iUnion
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ (n : ℕ), L n = f '' s
n : ℕ
⊢ L n ⊆ f '' s

Tactic:
exact (subset_iUnion _ n).trans hcov.le

Premises used: HasSubset.Subset.trans, Eq.le, Set.subset_iUnion
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ (n : ℕ), L n = f '' s
n : ℕ
⊢ f '' (f ⁻¹' L n ∩ s) = L n

Tactic:
have : f '' (f ⁻¹' (L n) ∩ s) = L n := by
        rw [image_preimage_inter, inter_eq_left.mpr]
        exact (subset_iUnion _ n).trans hcov.le
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ (n : ℕ), L n = f '' s
n : ℕ
this : f '' (f ⁻¹' L n ∩ s) = L n
⊢ IsCompact.{u_1} (X := X) ((fun (n : ℕ) ↦ f ⁻¹' L n ∩ s) n)

Tactic:
apply hf.isCompact_iff.mpr (this.symm ▸ (hcomp n))

Premises used: Iff.mpr, Topology.IsInducing.isCompact_iff
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ (n : ℕ), L n = f '' s
rw : ⋃ (n : ℕ), f ⁻¹' L n ∩ s = (⋃ (i : ℕ), f ⁻¹' L i) ∩ s
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), f ⁻¹' L n ∩ s) (⋃ (i : ℕ), f ⁻¹' L i ∩ s)
⊢ ⋃ (n : ℕ), f ⁻¹' L n ∩ s = (f ⁻¹' ⋃ (n : ℕ), L n) ∩ s

Tactic:
rw [preimage_iUnion, iUnion_inter]

Premises used: Set.iUnion_inter, Set.preimage_iUnion
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ (n : ℕ), L n = f '' s
rw rw₁ : f ⁻¹' f '' s ∩ s = f ⁻¹' f '' s ∩ s
⊢ (f ⁻¹' ⋃ (n : ℕ), L n) ∩ s = f ⁻¹' f '' s ∩ s

Tactic:
rw [hcov]
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ (n : ℕ), L n = f '' s
⊢ f ⁻¹' f '' s ∩ s = s

Tactic:
inter_eq_right.mpr (subset_preimage_image _ _)

Premises used: Iff.mpr, Set.inter_eq_right, Set.subset_preimage_image
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ (n : ℕ), L n = f '' s
calc : ⋃ (n : ℕ), f ⁻¹' L n ∩ s = (f ⁻¹' ⋃ (n : ℕ), L n) ∩ s
calc₁ : (f ⁻¹' ⋃ (n : ℕ), L n) ∩ s = f ⁻¹' f '' s ∩ s
⊢ ⋃ (n : ℕ), (fun (n : ℕ) ↦ f ⁻¹' L n ∩ s) n = s

Tactic:
calc ⋃ n, f ⁻¹' L n ∩ s
        _ = f ⁻¹' (⋃ n, L n) ∩ s := by rw [preimage_iUnion, iUnion_inter]
        _ = f ⁻¹' (f '' s) ∩ s := by rw [hcov]
        _ = s := inter_eq_right.mpr (subset_preimage_image _ _)

Premises used: Iff.mpr, Set.inter_eq_right, Set.image, Set.iUnion, Set.subset_preimage_image
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsEmbedding f
⊢ IsSigmaCompact s ↔ IsSigmaCompact (f '' s)

Tactic:
hf.isInducing.isSigmaCompact_iff

Premises used: Topology.IsInducing.isSigmaCompact_iff, Topology.IsEmbedding.isInducing
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
p : X → Prop
s : Set { a : X // p a }
⊢ IsSigmaCompact s ↔ IsSigmaCompact (val (p := fun (a : X) ↦ p a) '' s)

Tactic:
IsEmbedding.subtypeVal.isSigmaCompact_iff

Premises used: Topology.IsEmbedding.isSigmaCompact_iff, Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsSigmaCompact.{u_1} (X := X) univ ↔ SigmaCompactSpace X

Tactic:
⟨fun h => ⟨h⟩, fun h => h.1⟩

Premises used: SigmaCompactSpace.isSigmaCompact_univ, SigmaCompactSpace.mk, Iff.intro
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
h : SigmaCompactSpace X
⊢ IsSigmaCompact.{u_1} (X := X) univ

Tactic:
isSigmaCompact_univ_iff.mpr h

Premises used: Iff.mpr, isSigmaCompact_univ_iff
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
rw :
  IsSigmaCompact.{u_1} (X := X) univ ↔
    ∃ (K : ℕ → Set X), (∀ (n : ℕ), IsCompact (K n)) ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), K n) univ
rw₁ rw₂ :
  (∃ (K : ℕ → Set X), (∀ (n : ℕ), IsCompact (K n)) ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), K n) univ) ↔
    ∃ (K : ℕ → Set X), (∀ (n : ℕ), IsCompact (K n)) ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), K n) univ
⊢ SigmaCompactSpace X ↔
    ∃ (K : ℕ → Set X), (∀ (n : ℕ), IsCompact (K n)) ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), K n) univ

Tactic:
rw [← isSigmaCompact_univ_iff, IsSigmaCompact]

Premises used: IsSigmaCompact, isSigmaCompact_univ_iff
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
h : SigmaCompactSpace X
⊢ ∃ (K : ℕ → Set X), (∀ (n : ℕ), IsCompact (K n)) ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), K n) univ

Tactic:
SigmaCompactSpace_iff_exists_compact_covering.mp h

Premises used: SigmaCompactSpace_iff_exists_compact_covering, Iff.mp
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
inst_2 : SigmaCompactSpace X
⊢ IsSigmaCompact (range f)

Tactic:
image_univ ▸ isSigmaCompact_univ.image hf

Premises used: Set.image_univ, isSigmaCompact_univ, Eq.rec, IsSigmaCompact.image
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw :
  IsSigmaCompact s ↔
    IsSigmaCompact.{u_1} (X := X) (image (α := { a : X // a ∈ s }) (Subtype.val (p := fun (a : X) ↦ a ∈ s)) univ)
rw₁ :
  IsSigmaCompact s ↔
    IsSigmaCompact.{u_1} (X := X) (range (ι := { a : X // a ∈ s }) (Subtype.val (p := fun (a : X) ↦ a ∈ s)))
rw₂ rw₃ : IsSigmaCompact s ↔ IsSigmaCompact s
⊢ IsSigmaCompact s ↔ IsSigmaCompact.{u_1} (X := (↑s : Type u_1)) univ

Tactic:
rw [Subtype.isSigmaCompact_iff, image_univ, Subtype.range_coe]

Premises used: Set.image_univ, Subtype.range_coe, Subtype.isSigmaCompact_iff
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsSigmaCompact s ↔ SigmaCompactSpace.{u_1} (↑s : Type u_1)

Tactic:
isSigmaCompact_iff_isSigmaCompact_univ.trans isSigmaCompact_univ_iff

Premises used: isSigmaCompact_iff_isSigmaCompact_univ, Iff.trans, isSigmaCompact_univ_iff
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : CompactSpace X
⊢ SigmaCompactSpace X

Tactic:
⟨⟨fun _ => univ, fun _ => isCompact_univ, iUnion_const _⟩⟩

Premises used: CompactSpace.isCompact_univ, Set.univ, SigmaCompactSpace.mk, Set.iUnion_const, And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
Hc : S.Countable
Hcomp : ∀ s ∈ S, IsCompact s
HU : ⋃₀ S = univ
⊢ SigmaCompactSpace X

Tactic:
⟨(exists_seq_cover_iff_countable ⟨_, isCompact_empty⟩).2 ⟨S, Hc, Hcomp, HU⟩⟩

Premises used: Iff.mpr, SigmaCompactSpace.mk, Set.exists_seq_cover_iff_countable, And.intro, Exists.intro, isCompact_empty
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : LocallyCompactSpace X
inst_3 : SecondCountableTopology X
choose : ∀ (K : (x : X) → Set X) (hKc : ∀ (x : X), IsCompact (K x)) (hxK : ∀ (x : X), K x ∈ 𝓝 x), SigmaCompactSpace X
⊢ SigmaCompactSpace X

Tactic:
choose K hKc hxK using fun x : X => exists_compact_mem_nhds x

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : LocallyCompactSpace X
inst_3 : SecondCountableTopology X
K : (x : X) → Set X
hKc : ∀ (x : X), IsCompact (K x)
hxK : ∀ (x : X), K x ∈ 𝓝 x
rcases : ∀ (s : Set X) (hsc : s.Countable) (hsU : Eq.{u_1 + 1} (α := Set X) (⋃ x ∈ s, K x) univ), SigmaCompactSpace X
⊢ SigmaCompactSpace X

Tactic:
rcases countable_cover_nhds hxK with ⟨s, hsc, hsU⟩

Premises used: TopologicalSpace.countable_cover_nhds
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s_1 t : Set X
inst_2 : LocallyCompactSpace X
inst_3 : SecondCountableTopology X
K : (x : X) → Set X
hKc : ∀ (x : X), IsCompact (K x)
hxK : ∀ (x : X), K x ∈ 𝓝 x
s : Set X
hsc : s.Countable
hsU : Eq.{u_1 + 1} (α := Set X) (⋃ x ∈ s, K x) univ
⊢ SigmaCompactSpace X

Tactic:
SigmaCompactSpace.of_countable _ (hsc.image K) (forall_mem_image.2 fun x _ => hKc x) ?_

Premises used: Iff.mpr, Set.Countable.image, Set.forall_mem_image, SigmaCompactSpace.of_countable
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s_1 t : Set X
inst_2 : LocallyCompactSpace X
inst_3 : SecondCountableTopology X
K : (x : X) → Set X
hKc : ∀ (x : X), IsCompact (K x)
hxK : ∀ (x : X), K x ∈ 𝓝 x
s : Set X
hsc : s.Countable
hsU : Eq.{u_1 + 1} (α := Set X) (⋃ x ∈ s, K x) univ
refine : ⋃₀ (K '' s) = univ
⊢ SigmaCompactSpace X

Tactic:
refine SigmaCompactSpace.of_countable _ (hsc.image K) (forall_mem_image.2 fun x _ => hKc x) ?_

Premises used: Iff.mpr, Set.Countable.image, Set.forall_mem_image, SigmaCompactSpace.of_countable
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s_1 t : Set X
inst_2 : LocallyCompactSpace X
inst_3 : SecondCountableTopology X
K : (x : X) → Set X
hKc : ∀ (x : X), IsCompact (K x)
hxK : ∀ (x : X), K x ∈ 𝓝 x
s : Set X
hsc : s.Countable
hsU rwa rwa₁ rwa₂ rwa₃ : Eq.{u_1 + 1} (α := Set X) (⋃ a ∈ s, K a) univ
⊢ ⋃₀ (K '' s) = univ

Tactic:
rwa [sUnion_image]

Premises used: Set.sUnion_image
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
n : ℕ
⊢ IsCompact (compactCovering X n)

Tactic:
isCompact_accumulate (Classical.choose_spec SigmaCompactSpace.exists_compact_covering).1 n

Premises used: compactCovering, Classical.choose_spec, And.left, SigmaCompactSpace.exists_compact_covering, isCompact_accumulate
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
rw :
  Eq.{u_1 + 1} (α := Set X)
    (⋃ (x : ℕ),
      Exists.choose (p := fun (K : ℕ → Set X) ↦
        (∀ (n : ℕ), IsCompact (K n)) ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), K n) univ) ⋯ x)
    univ
⊢ Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), compactCovering X n) univ

Tactic:
rw [compactCovering, iUnion_accumulate]

Premises used: compactCovering, Set.iUnion_accumulate
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
⊢ Eq.{u_1 + 1} (α := Set X)
    (⋃ (x : ℕ),
      Exists.choose (p := fun (K : ℕ → Set X) ↦
        (∀ (n : ℕ), IsCompact (K n)) ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), K n) univ) ⋯ x)
    univ

Tactic:
(Classical.choose_spec SigmaCompactSpace.exists_compact_covering).2

Premises used: Classical.choose_spec, And.right, SigmaCompactSpace.exists_compact_covering
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
⊢ Eq.{u_1 + 1} (α := Set X)
    (⋃ (x : ℕ),
      Exists.choose (p := fun (K : ℕ → Set X) ↦
        (∀ (n : ℕ), IsCompact (K n)) ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), K n) univ) ⋯ x)
    univ

Tactic:
exact (Classical.choose_spec SigmaCompactSpace.exists_compact_covering).2

Premises used: Classical.choose_spec, And.right, SigmaCompactSpace.exists_compact_covering
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
⊢ Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), closure[inst] (compactCovering X n)) univ

Tactic:
eq_top_mono (iUnion_mono fun _ ↦ subset_closure) (iUnion_compactCovering X)

Premises used: subset_closure, iUnion_compactCovering, eq_top_mono, Set.iUnion_mono
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
m n : ℕ
h : m ≤ n
⊢ compactCovering X m ⊆ compactCovering X n

Tactic:
monotone_accumulate h

Premises used: compactCovering, Set.monotone_accumulate
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
x : X
⊢ ∃ (n : ℕ), x ∈ compactCovering X n

Tactic:
iUnion_eq_univ_iff.mp (iUnion_compactCovering X) x

Premises used: Set.iUnion_eq_univ_iff, iUnion_compactCovering, Iff.mp
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : SigmaCompactSpace X
inst_3 : SigmaCompactSpace Y
⊢ Eq (α := Set (X × Y)) (⋃ (n : ℕ), (fun (n : ℕ) ↦ compactCovering X n ×ˢ compactCovering Y n) n) univ

Tactic:
simp only [iUnion_prod_of_monotone (compactCovering_subset X) (compactCovering_subset Y),
        iUnion_compactCovering, univ_prod_univ]

Premises used: Set.iUnion_prod_of_monotone, iUnion_compactCovering, Set.univ_prod_univ, compactCovering_subset
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
inst_2 : SigmaCompactSpace X_1
inst_3 : Finite ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
⊢ SigmaCompactSpace ((i : ι) → X i)

Tactic:
⟨⟨fun n => Set.pi univ fun i => compactCovering (X i) n,
    fun n => isCompact_univ_pi fun i => isCompact_compactCovering (X i) _, ?_⟩⟩

Premises used: compactCovering, Set.univ, isCompact_univ_pi, SigmaCompactSpace.mk, isCompact_compactCovering, And.intro, Exists.intro, Set.pi
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
inst_2 : SigmaCompactSpace X_1
inst_3 : Finite ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
refine :
  Eq (α := Set ((i : ι) → X i))
    (⋃ (n : ℕ), (fun (n : ℕ) ↦ (Set.pi (α := X) univ fun (i : ι) ↦ compactCovering (X i) n : Set ((i : ι) → X i))) n)
    univ
⊢ SigmaCompactSpace ((i : ι) → X i)

Tactic:
refine ⟨⟨fun n => Set.pi univ fun i => compactCovering (X i) n,
    fun n => isCompact_univ_pi fun i => isCompact_compactCovering (X i) _, ?_⟩⟩
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
inst_2 : SigmaCompactSpace X_1
inst_3 : Finite ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
rw : Eq (α := Set ((i : ι) → X i)) (Set.pi (α := X) univ fun (i : ι) ↦ ⋃ (j : ℕ), compactCovering (X i) j) univ
rw₁ : ∀ (i : ι), Monotone.{0, u_4} (β := Set (X i)) (compactCovering (X i))
⊢ Eq (α := Set ((i : ι) → X i))
    (⋃ (n : ℕ), (fun (n : ℕ) ↦ (Set.pi (α := X) univ fun (i : ι) ↦ compactCovering (X i) n : Set ((i : ι) → X i))) n)
    univ

Tactic:
rw [iUnion_univ_pi_of_monotone]

Premises used: Set.iUnion_univ_pi_of_monotone
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
inst_2 : SigmaCompactSpace X_1
inst_3 : Finite ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
⊢ Eq (α := Set ((i : ι) → X i)) (Set.pi (α := X) univ fun (i : ι) ↦ ⋃ (j : ℕ), compactCovering (X i) j) univ

Tactic:
simp only [iUnion_compactCovering, pi_univ]

Premises used: iUnion_compactCovering, Set.pi_univ
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
inst_2 : SigmaCompactSpace X_1
inst_3 : Finite ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
⊢ ∀ (i : ι), Monotone.{0, u_4} (β := Set (X i)) (compactCovering (X i))

Tactic:
fun i => compactCovering_subset (X i)

Premises used: Monotone, compactCovering_subset
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
inst_2 : SigmaCompactSpace X_1
inst_3 : Finite ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
⊢ ∀ (i : ι), Monotone.{0, u_4} (β := Set (X i)) (compactCovering (X i))

Tactic:
exact fun i => compactCovering_subset (X i)

Premises used: compactCovering_subset
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : SigmaCompactSpace X
inst_3 : SigmaCompactSpace Y
⊢ Eq (α := Set (X ⊕ Y)) (⋃ (n : ℕ), (fun (n : ℕ) ↦ Sum.inl '' compactCovering X n ∪ Sum.inr '' compactCovering Y n) n)
    univ

Tactic:
simp only [iUnion_union_distrib, ← image_iUnion, iUnion_compactCovering, image_univ,
        range_inl_union_range_inr]

Premises used: Set.image_univ, Set.iUnion_union_distrib, iUnion_compactCovering, Set.range_inl_union_range_inr, Set.image_iUnion
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
inst_2 : SigmaCompactSpace X_1
inst_3 : Countable ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
inl : IsEmpty ι → SigmaCompactSpace ((i : ι) × X i)
inr : Nonempty ι → SigmaCompactSpace ((i : ι) × X i)
⊢ SigmaCompactSpace ((i : ι) × X i)

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
inst_2 : SigmaCompactSpace X_1
inst_3 : Countable ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
h : IsEmpty ι
⊢ SigmaCompactSpace ((i : ι) × X i)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
inst_2 : SigmaCompactSpace X_1
inst_3 : Countable ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
h : Nonempty ι
inr : ∀ (f : ℕ → ι) (hf : Function.Surjective f), SigmaCompactSpace ((i : ι) × X i)
⊢ SigmaCompactSpace ((i : ι) × X i)

Tactic:
rcases exists_surjective_nat ι with ⟨f, hf⟩

Premises used: exists_surjective_nat
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
inst_2 : SigmaCompactSpace X_1
inst_3 : Countable ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
h : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
⊢ SigmaCompactSpace ((i : ι) × X i)

Tactic:
⟨⟨fun n => ⋃ k ≤ n, Sigma.mk (f k) '' compactCovering (X (f k)) n, fun n => ?_, ?_⟩⟩

Premises used: compactCovering, SigmaCompactSpace.mk, And.intro, Exists.intro, Set.image, Sigma.mk, Set.iUnion
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
inst_2 : SigmaCompactSpace X_1
inst_3 : Countable ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
h : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
inr :
  ∀ (n : ℕ),
    IsCompact (X := (i : ι) × X i)
      ((fun (n : ℕ) ↦
          (⋃ (k : ℕ), ⋃ (_ : k ≤ n), Sigma.mk (β := fun (i : ι) ↦ X i) (f k) '' compactCovering (X (f k)) n :
            Set ((i : ι) × X i)))
        n)
inr₁ :
  Eq (α := Set ((i : ι) × X i))
    (⋃ (n : ℕ),
      (fun (n : ℕ) ↦
          (⋃ (k : ℕ), ⋃ (_ : k ≤ n), Sigma.mk (β := fun (i : ι) ↦ X i) (f k) '' compactCovering (X (f k)) n :
            Set ((i : ι) × X i)))
        n)
    univ
⊢ SigmaCompactSpace ((i : ι) × X i)

Tactic:
refine ⟨⟨fun n => ⋃ k ≤ n, Sigma.mk (f k) '' compactCovering (X (f k)) n, fun n => ?_, ?_⟩⟩
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
inst_2 : SigmaCompactSpace X_1
inst_3 : Countable ι
X : ι → Type u_4
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaCompactSpace.{u_4} (X i)
h : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
n : ℕ
⊢ IsCompact (X := (i : ι) × X i)
    ((fun (n : ℕ) ↦
        (⋃ (k : ℕ), ⋃ (_ : k ≤ n), Sigma.mk (β := fun (i : ι) ↦ X i) (f k) '' compactCovering (X (f k)) n :
          Set ((i : ι) × X i)))
      n)

Tactic:
(finite_le_nat _).isCompact_biUnion fun k _ => ?_

Premises used: Set.Mem, setOf, Set.Finite.isCompact_biUnion, Set.finite_le_nat