-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.prod {t : Set Y} (hs : IsCompact s) (ht : IsCompact t) :
    IsCompact (s ×ˢ t)

Proof state:
case intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : ↑f ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : ↑f ≤ comap Prod.snd (𝓝 y)
⊢ ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x

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

Result:
case intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : ↑f ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : ↑f ≤ comap Prod.snd (𝓝 y)
⊢ ↑f ≤ 𝓝 (x, y)

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
⊢ ∀ (f : Ultrafilter (X × Y)), s ×ˢ t ∈ f → ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x

Tactic:
intro f hfs

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
⊢ ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x

Proof state:
case intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : map Prod.fst ↑f ≤ 𝓝 x
⊢ ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x

Tactic:
obtain ⟨y : Y, ty : y ∈ t, hy : map Prod.snd f.1 ≤ 𝓝 y⟩ :=
  ht (f.map Prod.snd) (mem_map.2 <| mem_of_superset hfs fun x => And.right)

Result:
case intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : map Prod.fst ↑f ≤ 𝓝 x
y : Y
ty : y ∈ t
hy : map Prod.snd ↑f ≤ 𝓝 y
⊢ ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x

Proof state:
case intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : ↑f ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : ↑f ≤ comap Prod.snd (𝓝 y)
⊢ ↑f ≤ 𝓝 (x, y)

Tactic:
rw [nhds_prod_eq]

Result:
case intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : ↑f ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : ↑f ≤ comap Prod.snd (𝓝 y)
⊢ ↑f ≤ 𝓝 x ×ˢ 𝓝 y

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (s ×ˢ t)

Tactic:
rw [isCompact_iff_ultrafilter_le_nhds'] at hs ht ⊢

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
⊢ ∀ (f : Ultrafilter (X × Y)), s ×ˢ t ∈ f → ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x

Proof state:
case intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : map Prod.fst ↑f ≤ 𝓝 x
y : Y
ty : y ∈ t
hy : map Prod.snd ↑f ≤ 𝓝 y
⊢ ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x

Tactic:
rw [map_le_iff_le_comap] at hx hy

Result:
case intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : ↑f ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : ↑f ≤ comap Prod.snd (𝓝 y)
⊢ ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
⊢ ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x

Tactic:
obtain ⟨x : X, sx : x ∈ s, hx : map Prod.fst f.1 ≤ 𝓝 x⟩ :=
  hs (f.map Prod.fst) (mem_map.2 <| mem_of_superset hfs fun x => And.left)

Result:
case intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : map Prod.fst ↑f ≤ 𝓝 x
⊢ ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x

Proof state:
case intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : ↑f ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : ↑f ≤ comap Prod.snd (𝓝 y)
⊢ ↑f ≤ 𝓝 x ×ˢ 𝓝 y

Tactic:
exact le_inf hx hy

Result:
no goals