awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, (↑f : Filter Y) ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : map Prod.fst (↑f : Filter (X × Y)) ≤ 𝓝 x
y : Y
ty : y ∈ t
hy : map Prod.snd (↑f : Filter (X × Y)) ≤ 𝓝 y
rw :
  ∀ (hx : (↑f : Filter (X × Y)) ≤ comap Prod.fst (𝓝 x)) (y : Y) (ty : y ∈ t)
    (hy : (↑f : Filter (X × Y)) ≤ comap Prod.snd (𝓝 y)), ∃ x ∈ s ×ˢ t, (↑f : Filter (X × Y)) ≤ 𝓝 x
⊢ ∃ x ∈ s ×ˢ t, (↑f : Filter (X × Y)) ≤ 𝓝 x

Tactic:
rw [map_le_iff_le_comap] at hx hy

Premises used: Filter.map_le_iff_le_comap
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, (↑f : Filter Y) ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : (↑f : Filter (X × Y)) ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : (↑f : Filter (X × Y)) ≤ comap Prod.snd (𝓝 y)
⊢ ∃ x ∈ s ×ˢ t, (↑f : Filter (X × Y)) ≤ 𝓝 x

Tactic:
⟨⟨x, y⟩, ⟨sx, ty⟩, ?_⟩

Premises used: Prod.mk, And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, (↑f : Filter Y) ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : (↑f : Filter (X × Y)) ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : (↑f : Filter (X × Y)) ≤ comap Prod.snd (𝓝 y)
refine : (↑f : Filter (X × Y)) ≤ 𝓝 (x, y)
⊢ ∃ x ∈ s ×ˢ t, (↑f : Filter (X × Y)) ≤ 𝓝 x

Tactic:
refine ⟨⟨x, y⟩, ⟨sx, ty⟩, ?_⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, (↑f : Filter Y) ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : (↑f : Filter (X × Y)) ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : (↑f : Filter (X × Y)) ≤ comap Prod.snd (𝓝 y)
rw : (↑f : Filter (X × Y)) ≤ 𝓝 x ×ˢ 𝓝 y
⊢ (↑f : Filter (X × Y)) ≤ 𝓝 (x, y)

Tactic:
rw [nhds_prod_eq]

Premises used: nhds_prod_eq
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, (↑f : Filter Y) ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : (↑f : Filter (X × Y)) ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : (↑f : Filter (X × Y)) ≤ comap Prod.snd (𝓝 y)
⊢ (↑f : Filter (X × Y)) ≤ 𝓝 x ×ˢ 𝓝 y

Tactic:
le_inf hx hy

Premises used: Set.Mem, le_inf
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, (↑f : Filter Y) ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : (↑f : Filter (X × Y)) ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : (↑f : Filter (X × Y)) ≤ comap Prod.snd (𝓝 y)
⊢ (↑f : Filter (X × Y)) ≤ 𝓝 x ×ˢ 𝓝 y

Tactic:
exact le_inf hx hy

Premises used: le_inf
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f_1 : X → Y
inst_2 : IndiscreteTopology X
f : Filter X
hf : f.NeBot
⊢ f ≤ 𝓟 univ → ∃ (x : X), Membership.mem (γ := Set X) univ x ∧ ClusterPt x f

Tactic:
simp [clusterPt_of_indiscreteTopology, nonempty_of_neBot f]

Premises used: Filter.nonempty_of_neBot, clusterPt_of_indiscreteTopology
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : CompactSpace X
⊢ CompactSpace (ULift.{v, u} X)

Tactic:
IsClosedEmbedding.uliftDown.compactSpace

Premises used: Topology.IsClosedEmbedding.compactSpace, Topology.IsClosedEmbedding.uliftDown
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
rw : IsCompact (SProd.sprod (α := Set X) (β := Set Y) univ univ)
⊢ IsCompact (X := X × Y) univ

Tactic:
rw [← univ_prod_univ]

Premises used: Set.univ_prod_univ
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
⊢ IsCompact (SProd.sprod (α := Set X) (β := Set Y) univ univ)

Tactic:
isCompact_univ.prod isCompact_univ

Premises used: IsCompact.prod, isCompact_univ
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
⊢ IsCompact (SProd.sprod (α := Set X) (β := Set Y) univ univ)

Tactic:
exact isCompact_univ.prod isCompact_univ

Premises used: IsCompact.prod, isCompact_univ
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
rw : IsCompact (X := X ⊕ Y) (range Sum.inl ∪ range Sum.inr)
⊢ IsCompact (X := X ⊕ Y) univ

Tactic:
rw [← range_inl_union_range_inr]

Premises used: Set.range_inl_union_range_inr
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
⊢ IsCompact (X := X ⊕ Y) (range Sum.inl ∪ range Sum.inr)

Tactic:
(isCompact_range continuous_inl).union (isCompact_range continuous_inr)

Premises used: continuous_inl, continuous_inr, isCompact_range, IsCompact.union
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
⊢ IsCompact (X := X ⊕ Y) (range Sum.inl ∪ range Sum.inr)

Tactic:
exact (isCompact_range continuous_inl).union (isCompact_range continuous_inr)

Premises used: continuous_inl, continuous_inr, isCompact_range, IsCompact.union
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X_1 : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
f : X_1 → Y
X : ι → Type u_2
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_2} (X i)
⊢ CompactSpace ((i : ι) × X i)

Tactic:
⟨?_⟩

Premises used: CompactSpace.mk
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X_1 : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
f : X_1 → Y
X : ι → Type u_2
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_2} (X i)
refine : IsCompact (X := (i : ι) × X i) univ
⊢ CompactSpace ((i : ι) × X i)

Tactic:
refine ⟨?_⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X_1 : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
f : X_1 → Y
X : ι → Type u_2
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_2} (X i)
rw : IsCompact (X := (i : ι) × X i) (⋃ (a : ι), range (Sigma.mk (β := fun (a : ι) ↦ X a) a))
⊢ IsCompact (X := (i : ι) × X i) univ

Tactic:
rw [Sigma.univ]

Premises used: Set.Sigma.univ
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X_1 : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
f : X_1 → Y
X : ι → Type u_2
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_2} (X i)
⊢ IsCompact (X := (i : ι) × X i) (⋃ (a : ι), range (Sigma.mk (β := fun (a : ι) ↦ X a) a))

Tactic:
isCompact_iUnion fun i => isCompact_range continuous_sigmaMk

Premises used: continuous_sigmaMk, isCompact_range, isCompact_iUnion
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X_1 : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
f : X_1 → Y
X : ι → Type u_2
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_2} (X i)
⊢ IsCompact (X := (i : ι) × X i) (⋃ (a : ι), range (Sigma.mk (β := fun (a : ι) ↦ X a) a))

Tactic:
exact isCompact_iUnion fun i => isCompact_range continuous_sigmaMk

Premises used: continuous_sigmaMk, isCompact_range, isCompact_iUnion
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ι
t : (i : ι) → Set (X i)
hs : s.Finite
ht : ∀ i ∈ s, IsCompact (t i)
rw : IsCompact (X := (i : ι) × X i) (⋃ i ∈ s, Sigma.mk (β := X) i '' t i)
⊢ IsCompact (s.sigma (α := X) t)

Tactic:
rw [Set.sigma_eq_biUnion]

Premises used: Set.sigma_eq_biUnion
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ι
t : (i : ι) → Set (X i)
hs : s.Finite
ht : ∀ i ∈ s, IsCompact (t i)
⊢ IsCompact (X := (i : ι) × X i) (⋃ i ∈ s, Sigma.mk (β := X) i '' t i)

Tactic:
hs.isCompact_biUnion fun i hi ↦ (ht i hi).image continuous_sigmaMk

Premises used: continuous_sigmaMk, Set.Finite.isCompact_biUnion, IsCompact.image
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ι
t : (i : ι) → Set (X i)
hs : s.Finite
ht : ∀ i ∈ s, IsCompact (t i)
⊢ IsCompact (X := (i : ι) × X i) (⋃ i ∈ s, Sigma.mk (β := X) i '' t i)

Tactic:
exact hs.isCompact_biUnion fun i hi ↦ (ht i hi).image continuous_sigmaMk

Premises used: continuous_sigmaMk, Set.Finite.isCompact_biUnion, IsCompact.image
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
x : (i : ι) × X i
hx : x ∈ u
⊢ Membership.mem (γ := Set ((i : ι) × X i))
    (⋃ (i : ι),
      (fun (i : ι) ↦ (Sigma.mk (β := fun (i : ι) ↦ X i) i '' Sigma.mk (β := X) i ⁻¹' univ : Set ((i : ι) × X i))) i)
    x

Tactic:
simp
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
obtain :
  ∀ (s : Finset ι) (hs : u ⊆ ⋃ i ∈ s, Sigma.mk (β := fun (i : ι) ↦ X i) i '' Sigma.mk (β := X) i ⁻¹' univ),
    ∃ (s : Set ι) (t : (i : ι) → Set (X i)), s.Finite ∧ (∀ (i : ι), IsCompact (t i)) ∧ s.sigma (α := X) t = u
⊢ ∃ (s : Set ι) (t : (i : ι) → Set (X i)), s.Finite ∧ (∀ (i : ι), IsCompact (t i)) ∧ s.sigma (α := X) t = u

Tactic:
obtain ⟨s, hs⟩ := hu.elim_finite_subcover (fun i : ι ↦ Sigma.mk i '' Sigma.mk i ⁻¹' Set.univ)
    (fun i ↦ isOpenMap_sigmaMk _ <| isOpen_univ.preimage continuous_sigmaMk)
    fun x hx ↦ (by simp)

Premises used: Set.univ, continuous_sigmaMk, isOpen_univ, IsCompact.elim_finite_subcover, Set.preimage, isOpenMap_sigmaMk, Set.image, Sigma.mk, IsOpen.preimage
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk (β := fun (i : ι) ↦ X i) i '' Sigma.mk (β := X) i ⁻¹' univ
left : ∀ (i : ι), IsCompact (Sigma.mk (β := X) i ⁻¹' u)
right : ((↑s : Set ι).sigma (α := X) fun (i : ι) ↦ Sigma.mk (β := X) i ⁻¹' u) = u
⊢ ∃ (s : Set ι) (t : (i : ι) → Set (X i)), s.Finite ∧ (∀ (i : ι), IsCompact (t i)) ∧ s.sigma (α := X) t = u

Tactic:
use s, fun i ↦ Sigma.mk i ⁻¹' u, s.finite_toSet, fun i ↦ ?_, ?_

Premises used: Set.preimage, Finset.finite_toSet, Sigma.mk
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk (β := fun (i : ι) ↦ X i) i '' Sigma.mk (β := X) i ⁻¹' univ
i : ι
⊢ IsCompact (Sigma.mk (β := X) i ⁻¹' u)

Tactic:
Topology.IsClosedEmbedding.sigmaMk.isCompact_preimage hu

Premises used: Topology.IsClosedEmbedding.sigmaMk, Topology.IsClosedEmbedding.isCompact_preimage
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk (β := fun (i : ι) ↦ X i) i '' Sigma.mk (β := X) i ⁻¹' univ
i : ι
⊢ IsCompact (Sigma.mk (β := X) i ⁻¹' u)

Tactic:
exact Topology.IsClosedEmbedding.sigmaMk.isCompact_preimage hu

Premises used: Topology.IsClosedEmbedding.sigmaMk, Topology.IsClosedEmbedding.isCompact_preimage
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk (β := fun (i : ι) ↦ X i) i '' Sigma.mk (β := X) i ⁻¹' univ
right :
  ∀ (x : (i : ι) × X i),
    Membership.mem (γ := Set ((i : ι) × X i)) ((↑s : Set ι).sigma (α := X) fun (i : ι) ↦ Sigma.mk (β := X) i ⁻¹' u) x ↔
      x ∈ u
⊢ ((↑s : Set ι).sigma (α := X) fun (i : ι) ↦ Sigma.mk (β := X) i ⁻¹' u) = u

Tactic:
ext x
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk (β := fun (i : ι) ↦ X i) i '' Sigma.mk (β := X) i ⁻¹' univ
x : (i : ι) × X i
right :
  Sigma.mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i)) ∈ u →
    x.fst (β := fun (i : ι) ↦ X i) ∈ s
⊢ Membership.mem (γ := Set ((i : ι) × X i)) ((↑s : Set ι).sigma (α := X) fun (i : ι) ↦ Sigma.mk (β := X) i ⁻¹' u) x ↔
    x ∈ u

Tactic:
simp only [Set.mem_sigma_iff, Finset.mem_coe, Set.mem_preimage, and_iff_right_iff_imp]

Premises used: Set.mem_sigma_iff, and_iff_right_iff_imp, Finset.mem_coe, Set.mem_preimage
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk (β := fun (i : ι) ↦ X i) i '' Sigma.mk (β := X) i ⁻¹' univ
x : (i : ι) × X i
hx : Sigma.mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i)) ∈ u
right :
  ∀ (i : ι)
    (hi :
      Membership.mem (γ := Set ((i : ι) × X i))
        (⋃ (_ : i ∈ s), Sigma.mk (β := fun (i : ι) ↦ X i) i '' Sigma.mk (β := X) i ⁻¹' univ)
        (Sigma.mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i)))),
    x.fst (β := fun (i : ι) ↦ X i) ∈ s
⊢ x.fst (β := fun (i : ι) ↦ X i) ∈ s

Tactic:
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp (hs hx)

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk (β := fun (i : ι) ↦ X i) i '' Sigma.mk (β := X) i ⁻¹' univ
x : (i : ι) × X i
hx : Sigma.mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i)) ∈ u
i : ι
hi :
  Membership.mem (γ := Set ((i : ι) × X i))
    (⋃ (_ : i ∈ s), Sigma.mk (β := fun (i : ι) ↦ X i) i '' Sigma.mk (β := X) i ⁻¹' univ)
    (Sigma.mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i)))
⊢ x.fst (β := fun (i : ι) ↦ X i) ∈ s

Tactic:
simp_all
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
a : (cocompact X).coprod (cocompact Y) ≤ cocompact (X × Y)
a₁ : cocompact (X × Y) ≤ (cocompact X).coprod (cocompact Y)
⊢ (cocompact X).coprod (cocompact Y) = cocompact (X × Y)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ (cocompact X).coprod (cocompact Y) ≤ cocompact (X × Y)

Tactic:
sup_le (comap_cocompact_le continuous_fst) (comap_cocompact_le continuous_snd)

Premises used: Set.Mem, Filter.comap_cocompact_le, continuous_snd, continuous_fst, sup_le
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ (cocompact X).coprod (cocompact Y) ≤ cocompact (X × Y)

Tactic:
exact sup_le (comap_cocompact_le continuous_fst) (comap_cocompact_le continuous_snd)

Premises used: Filter.comap_cocompact_le, continuous_snd, continuous_fst, sup_le
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ cocompact (X × Y) ≤ (cocompact X).coprod (cocompact Y)

Tactic:
(hasBasis_cocompact.coprod hasBasis_cocompact).ge_iff.2 fun K hK ↦ ?_

Premises used: Iff.mpr, Filter.HasBasis.ge_iff, Filter.hasBasis_cocompact, Filter.HasBasis.coprod
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
a :
  ∀ (K : Prod.{u, v} (Set X) (Set Y)) (hK : IsCompact K.1 ∧ IsCompact K.2),
    Membership.mem (γ := Filter (X × Y)) (cocompact (X × Y)) (Prod.fst ⁻¹' K.1ᶜ ∪ Prod.snd ⁻¹' K.2ᶜ)
⊢ cocompact (X × Y) ≤ (cocompact X).coprod (cocompact Y)

Tactic:
refine (hasBasis_cocompact.coprod hasBasis_cocompact).ge_iff.2 fun K hK ↦ ?_

Premises used: Iff.mpr, Filter.HasBasis.ge_iff, Filter.hasBasis_cocompact, Filter.HasBasis.coprod
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
K : Prod.{u, v} (Set X) (Set Y)
hK : IsCompact K.1 ∧ IsCompact K.2
a : Membership.mem (γ := Filter (X × Y)) (cocompact (X × Y)) (K.1 ×ˢ K.2)ᶜ
⊢ Membership.mem (γ := Filter (X × Y)) (cocompact (X × Y)) (Prod.fst ⁻¹' K.1ᶜ ∪ Prod.snd ⁻¹' K.2ᶜ)

Tactic:
rw [← univ_prod, ← prod_univ, ← compl_prod_eq_union]

Premises used: Set.univ_prod, Set.prod_univ, Set.compl_prod_eq_union
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
K : Prod.{u, v} (Set X) (Set Y)
hK : IsCompact K.1 ∧ IsCompact K.2
⊢ Membership.mem (γ := Filter (X × Y)) (cocompact (X × Y)) (K.1 ×ˢ K.2)ᶜ

Tactic:
(hK.1.prod hK.2).compl_mem_cocompact

Premises used: Set.Mem, IsCompact.prod, IsCompact.compl_mem_cocompact, setOf, And.right, And.left
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
K : Prod.{u, v} (Set X) (Set Y)
hK : IsCompact K.1 ∧ IsCompact K.2
⊢ Membership.mem (γ := Filter (X × Y)) (cocompact (X × Y)) (K.1 ×ˢ K.2)ᶜ

Tactic:
exact (hK.1.prod hK.2).compl_mem_cocompact

Premises used: IsCompact.prod, IsCompact.compl_mem_cocompact, And.right, And.left
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ NoncompactSpace (X × Y) ↔ NoncompactSpace X ∧ Nonempty Y ∨ Nonempty X ∧ NoncompactSpace Y

Tactic:
simp [← Filter.cocompact_neBot_iff, ← Filter.coprod_cocompact, Filter.coprod_neBot_iff]

Premises used: Filter.cocompact_neBot_iff, Filter.coprod_cocompact, Filter.coprod_neBot_iff
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : NoncompactSpace X
inst_3 : Nonempty Y
⊢ NoncompactSpace (X × Y)

Tactic:
Prod.noncompactSpace_iff.2 (Or.inl ⟨‹_›, ‹_›⟩)

Premises used: Iff.mpr, Prod.noncompactSpace_iff, And.intro, Or.inl
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : Nonempty X
inst_3 : NoncompactSpace Y
⊢ NoncompactSpace (X × Y)

Tactic:
Prod.noncompactSpace_iff.2 (Or.inr ⟨‹_›, ‹_›⟩)

Premises used: Iff.mpr, Prod.noncompactSpace_iff, And.intro, Or.inr
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
simp :
  (∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ (↑f : Filter (X i)) → ∃ x ∈ s i, (↑f : Filter (X i)) ≤ 𝓝 x) →
    ∀ (f : Ultrafilter ((i : ι) → X i)),
      {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} ∈ (↑f : Filter ((i : ι) → X i)) →
        ∃ (x : (i : ι) → X i),
          Membership.mem (γ := Set ((i : ι) → X i)) {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} x ∧
            ∀ (i : ι), Tendsto (eval (β := X) i) (↑f : Filter ((i : ι) → X i)) (𝓝 (x i))
⊢ (∀ (i : ι), IsCompact (s i)) → IsCompact (X := (i : ι) → X i) {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i}

Tactic:
simp only [isCompact_iff_ultrafilter_le_nhds, nhds_pi, le_pi, le_principal_iff]

Premises used: Filter.le_principal_iff, nhds_pi, isCompact_iff_ultrafilter_le_nhds, Filter.le_pi
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ (↑f : Filter (X i)) → ∃ x ∈ s i, (↑f : Filter (X i)) ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} ∈ (↑f : Filter ((i : ι) → X i))
⊢ ∀ (i : ι), ∃ x ∈ s i, Tendsto (eval (β := X) i) (↑f : Filter ((i : ι) → X i)) (𝓝 x)

Tactic:
fun i => h i (f.map _) (mem_map.2 ?_)

Premises used: Iff.mpr, Set.Mem, Function.eval, Filter.Tendsto, Ultrafilter.map, Filter.mem_map
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ (↑f : Filter (X i)) → ∃ x ∈ s i, (↑f : Filter (X i)) ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} ∈ (↑f : Filter ((i : ι) → X i))
refine : ∀ (i : ι), eval (β := X) i ⁻¹' s i ∈ (↑f : Filter ((i : ι) → X i))
⊢ ∀ (i : ι), ∃ x ∈ s i, Tendsto (eval (β := X) i) (↑f : Filter ((i : ι) → X i)) (𝓝 x)

Tactic:
refine fun i => h i (f.map _) (mem_map.2 ?_)

Premises used: Iff.mpr, Ultrafilter.map, Filter.mem_map
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ (↑f : Filter (X i)) → ∃ x ∈ s i, (↑f : Filter (X i)) ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} ∈ (↑f : Filter ((i : ι) → X i))
i : ι
⊢ eval (β := X) i ⁻¹' s i ∈ (↑f : Filter ((i : ι) → X i))

Tactic:
mem_of_superset hfs fun x hx => hx i

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ (↑f : Filter (X i)) → ∃ x ∈ s i, (↑f : Filter (X i)) ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} ∈ (↑f : Filter ((i : ι) → X i))
i : ι
⊢ eval (β := X) i ⁻¹' s i ∈ (↑f : Filter ((i : ι) → X i))

Tactic:
exact mem_of_superset hfs fun x hx => hx i

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ (↑f : Filter (X i)) → ∃ x ∈ s i, (↑f : Filter (X i)) ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} ∈ (↑f : Filter ((i : ι) → X i))
⊢ ∀ (i : ι), ∃ x ∈ s i, Tendsto (eval (β := X) i) (↑f : Filter ((i : ι) → X i)) (𝓝 x)

Tactic:
have : ∀ i : ι, ∃ x, x ∈ s i ∧ Tendsto (Function.eval i) f (𝓝 x) := by
    refine fun i => h i (f.map _) (mem_map.2 ?_)
    exact mem_of_superset hfs fun x hx => hx i