-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem measurable_uncurry_of_continuous_of_measurable {α β ι : Type*} [TopologicalSpace ι]
    [MetrizableSpace ι] [MeasurableSpace ι] [SecondCountableTopology ι] [OpensMeasurableSpace ι]
    {mβ : MeasurableSpace β} [TopologicalSpace β] [PseudoMetrizableSpace β] [BorelSpace β]
    {m : MeasurableSpace α} {u : ι → α → β} (hu_cont : ∀ x, Continuous fun i => u i x)
    (h : ∀ i, Measurable (u i)) : Measurable (Function.uncurry u)

Proof state:
case intro
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.1 p.2)
n : ℕ
h_meas : Measurable fun p => u (↑p.1) p.2
this : (fun p => u ((t_sf n) p.1) p.2) = (fun p => u (↑p.1) p.2) ∘ fun p => (⟨(t_sf n) p.1, ⋯⟩, p.2)
⊢ Measurable (U n)

Tactic:
simp_rw [U, this]

Result:
case intro
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.1 p.2)
n : ℕ
h_meas : Measurable fun p => u (↑p.1) p.2
this : (fun p => u ((t_sf n) p.1) p.2) = (fun p => u (↑p.1) p.2) ∘ fun p => (⟨(t_sf n) p.1, ⋯⟩, p.2)
⊢ Measurable ((fun p => u (↑p.1) p.2) ∘ fun p => (⟨(t_sf n) p.1, ⋯⟩, p.2))

Proof state:
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.1 p.2)
n : ℕ
this : (fun p => u (↑p.1) p.2) = (fun p => u (↑p.2) p.1) ∘ Prod.swap
⊢ Measurable fun p => u (↑p.2) p.1

Tactic:
exact measurable_from_prod_countable fun j => h j

Result:
no goals

Proof state:
case intro
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.1 p.2)
n : ℕ
h_meas : Measurable fun p => u (↑p.1) p.2
this : (fun p => u ((t_sf n) p.1) p.2) = (fun p => u (↑p.1) p.2) ∘ fun p => (⟨(t_sf n) p.1, ⋯⟩, p.2)
⊢ Measurable ((fun p => u (↑p.1) p.2) ∘ fun p => (⟨(t_sf n) p.1, ⋯⟩, p.2))

Tactic:
refine h_meas.comp (Measurable.prod_mk ?_ measurable_snd)

Result:
case intro
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.1 p.2)
n : ℕ
h_meas : Measurable fun p => u (↑p.1) p.2
this : (fun p => u ((t_sf n) p.1) p.2) = (fun p => u (↑p.1) p.2) ∘ fun p => (⟨(t_sf n) p.1, ⋯⟩, p.2)
⊢ Measurable fun p => ⟨(t_sf n) p.1, ⋯⟩

Proof state:
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
h_str_meas : StronglyMeasurable id
j : ι
x : α
⊢ Tendsto (fun n => u ((h_str_meas.approx n) j) x) atTop (𝓝 (u j x))

Tactic:
exact ((hu_cont x).tendsto j).comp (h_str_meas.tendsto_approx j)

Result:
no goals

Proof state:
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
⊢ Measurable (uncurry u)

Tactic:
obtain ⟨t_sf, ht_sf⟩ :
  ∃ t : ℕ → SimpleFunc ι ι, ∀ j x, Tendsto (fun n => u (t n j) x) atTop (𝓝 <| u j x) := by
  have h_str_meas : StronglyMeasurable (id : ι → ι) := stronglyMeasurable_id
  refine ⟨h_str_meas.approx, fun j x => ?_⟩
  exact ((hu_cont x).tendsto j).comp (h_str_meas.tendsto_approx j)

Result:
case intro
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u ((t_sf n) j) x) atTop (𝓝 (u j x))
⊢ Measurable (uncurry u)