-- Mathlib/Topology/Maps/Proper/Basic.lean
/-- Any product of proper maps is proper. -/
lemma IsProperMap.pi_map {X Y : ι → Type*} [∀ i, TopologicalSpace (X i)]
    [∀ i, TopologicalSpace (Y i)] {f : (i : ι) → X i → Y i} (h : ∀ i, IsProperMap (f i)) :
    IsProperMap (fun (x : ∀ i, X i) i ↦ f i (x i))

Proof state:
case left
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ Continuous fun x i => f i (x i)

Tactic:
exact continuous_pi fun i ↦ (h i).1.comp (continuous_apply i)

Result:
no goals

Proof state:
case right
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y)
this : ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval i) 𝒰)) (𝓝 (y i))
x : (i : ι) → X i
hxy : ∀ (i : ι), f i (x i) = y i
hx : ∀ (i : ι), ↑(Ultrafilter.map (eval i) 𝒰) ≤ 𝓝 (x i)
⊢ ∃ x, (fun i => f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x

Tactic:
refine ⟨x, funext hxy, ?_⟩

Result:
case right
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y)
this : ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval i) 𝒰)) (𝓝 (y i))
x : (i : ι) → X i
hxy : ∀ (i : ι), f i (x i) = y i
hx : ∀ (i : ι), ↑(Ultrafilter.map (eval i) 𝒰) ≤ 𝓝 (x i)
⊢ ↑𝒰 ≤ 𝓝 x

Proof state:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y)
⊢ ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval i) 𝒰)) (𝓝 (y i))

Tactic:
simpa [tendsto_pi_nhds] using hy

Result:
no goals

Proof state:
case right
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y)
this : ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval i) 𝒰)) (𝓝 (y i))
x : (i : ι) → X i
hxy : ∀ (i : ι), f i (x i) = y i
hx : ∀ (i : ι), ↑(Ultrafilter.map (eval i) 𝒰) ≤ 𝓝 (x i)
⊢ ↑𝒰 ≤ 𝓝 x

Tactic:
rwa [nhds_pi, le_pi]

Result:
no goals

Proof state:
case right
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ ∀ ⦃𝒰 : Ultrafilter ((i : ι) → X i)⦄ ⦃y : (i : ι) → Y i⦄,
    Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y) → ∃ x, (fun i => f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x

Tactic:
intro 𝒰 y hy

Result:
case right
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y)
⊢ ∃ x, (fun i => f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x

Proof state:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ (Continuous fun x i => f i (x i)) ∧
    ∀ ⦃𝒰 : Ultrafilter ((i : ι) → X i)⦄ ⦃y : (i : ι) → Y i⦄,
      Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y) → ∃ x, (fun i => f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x

Tactic:
constructor

Result:
case left
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ Continuous fun x i => f i (x i)

case right
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ ∀ ⦃𝒰 : Ultrafilter ((i : ι) → X i)⦄ ⦃y : (i : ι) → Y i⦄,
    Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y) → ∃ x, (fun i => f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x

Proof state:
case right
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y)
⊢ ∃ x, (fun i => f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x

Tactic:
have : ∀ i, Tendsto (f i) (Ultrafilter.map (eval i) 𝒰) (𝓝 (y i)) := by
  simpa [tendsto_pi_nhds] using hy

Result:
case right
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y)
this : ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval i) 𝒰)) (𝓝 (y i))
⊢ ∃ x, (fun i => f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x

Proof state:
case right
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y)
this : ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval i) 𝒰)) (𝓝 (y i))
⊢ ∃ x, (fun i => f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x

Tactic:
choose x hxy hx using fun i ↦ (h i).2 (this i)

Result:
case right
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y)
this : ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval i) 𝒰)) (𝓝 (y i))
x : (i : ι) → X i
hxy : ∀ (i : ι), f i (x i) = y i
hx : ∀ (i : ι), ↑(Ultrafilter.map (eval i) 𝒰) ≤ 𝓝 (x i)
⊢ ∃ x, (fun i => f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x