-- Mathlib/Topology/Compactness/Compact.lean
theorem isCompact_pi_infinite {s : ∀ i, Set (X i)} :
    (∀ i, IsCompact (s i)) → IsCompact { x : ∀ i, X i | ∀ i, x i ∈ s i }

Proof state:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
⊢ (∀ (i : ι), IsCompact (s i)) → IsCompact {x | ∀ (i : ι), x i ∈ s i}

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

Result:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
⊢ (∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ ↑f → ∃ x ∈ s i, ↑f ≤ 𝓝 x) →
    ∀ (f : Ultrafilter ((i : ι) → X i)),
      {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f → ∃ x ∈ {x | ∀ (i : ι), x i ∈ s i}, ∀ (i : ι), Tendsto (eval i) (↑f) (𝓝 (x i))

Proof state:
ι : 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 → ∃ x ∈ s i, ↑f ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f
⊢ ∀ (i : ι), ∃ x ∈ s i, Tendsto (eval i) (↑f) (𝓝 x)

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

Result:
ι : 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 → ∃ x ∈ s i, ↑f ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f
i : ι
⊢ eval i ⁻¹' s i ∈ ↑f

Proof state:
ι : 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 → ∃ x ∈ s i, ↑f ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f
i : ι
⊢ eval i ⁻¹' s i ∈ ↑f

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

Result:
no goals

Proof state:
ι : 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 → ∃ x ∈ s i, ↑f ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f
x : (i : ι) → X i
hx : ∀ (i : ι), x i ∈ s i ∧ Tendsto (eval i) (↑f) (𝓝 (x i))
⊢ ∃ x ∈ {x | ∀ (i : ι), x i ∈ s i}, ∀ (i : ι), Tendsto (eval i) (↑f) (𝓝 (x i))

Tactic:
exact ⟨x, fun i => (hx i).left, fun i => (hx i).right⟩

Result:
no goals

Proof state:
ι : 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 → ∃ x ∈ s i, ↑f ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f
this : ∀ (i : ι), ∃ x ∈ s i, Tendsto (eval i) (↑f) (𝓝 x)
⊢ ∃ x ∈ {x | ∀ (i : ι), x i ∈ s i}, ∀ (i : ι), Tendsto (eval i) (↑f) (𝓝 (x i))

Tactic:
choose x hx using this

Result:
ι : 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 → ∃ x ∈ s i, ↑f ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f
x : (i : ι) → X i
hx : ∀ (i : ι), x i ∈ s i ∧ Tendsto (eval i) (↑f) (𝓝 (x i))
⊢ ∃ x ∈ {x | ∀ (i : ι), x i ∈ s i}, ∀ (i : ι), Tendsto (eval i) (↑f) (𝓝 (x i))

Proof state:
ι : 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 → ∃ x ∈ s i, ↑f ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f
⊢ ∃ x ∈ {x | ∀ (i : ι), x i ∈ s i}, ∀ (i : ι), Tendsto (eval i) (↑f) (𝓝 (x i))

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

Result:
ι : 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 → ∃ x ∈ s i, ↑f ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f
this : ∀ (i : ι), ∃ x ∈ s i, Tendsto (eval i) (↑f) (𝓝 x)
⊢ ∃ x ∈ {x | ∀ (i : ι), x i ∈ s i}, ∀ (i : ι), Tendsto (eval i) (↑f) (𝓝 (x i))

Proof state:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
⊢ (∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ ↑f → ∃ x ∈ s i, ↑f ≤ 𝓝 x) →
    ∀ (f : Ultrafilter ((i : ι) → X i)),
      {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f → ∃ x ∈ {x | ∀ (i : ι), x i ∈ s i}, ∀ (i : ι), Tendsto (eval i) (↑f) (𝓝 (x i))

Tactic:
intro h f hfs

Result:
ι : 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 → ∃ x ∈ s i, ↑f ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f
⊢ ∃ x ∈ {x | ∀ (i : ι), x i ∈ s i}, ∀ (i : ι), Tendsto (eval i) (↑f) (𝓝 (x i))