awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
h_meas : Measurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2
⊢ Eq (α := (p : ι × α) → β) (fun (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2)
    ((fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2) ∘ fun (p : ι × α) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯, p.2))

Tactic:
have :
    (fun p : ι × α => u (t_sf n p.fst) p.snd) =
      (fun p : ↥(t_sf n).range × α => u p.fst p.snd) ∘ fun p : ι × α =>
        (⟨t_sf n p.fst, SimpleFunc.mem_range_self _ _⟩, p.snd) :=
    rfl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
h_meas : Measurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2
this :
  Eq (α := (p : ι × α) → β) (fun (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2)
    ((fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2) ∘ fun (p : ι × α) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯, p.2))
simp_rw :
  Measurable (α := ι × α) (β := β)
    ((fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2) ∘ fun (p : ι × α) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯, p.2))
⊢ Measurable (U n)

Tactic:
simp_rw [U, this]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
h_meas : Measurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2
this :
  Eq (α := (p : ι × α) → β) (fun (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2)
    ((fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2) ∘ fun (p : ι × α) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯, p.2))
⊢ Measurable (α := ι × α) (β := β)
    ((fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2) ∘ fun (p : ι × α) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯, p.2))

Tactic:
h_meas.comp (Measurable.prodMk ?_ measurable_snd)

Premises used: Measurable.comp, Measurable.prodMk, measurable_snd
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
h_meas : Measurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2
this :
  Eq (α := (p : ι × α) → β) (fun (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2)
    ((fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2) ∘ fun (p : ι × α) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯, p.2))
refine :
  Measurable (β := ↥(t_sf n).range) fun (p : ι × α) ↦
    Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯
⊢ Measurable (α := ι × α) (β := β)
    ((fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2) ∘ fun (p : ι × α) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯, p.2))

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

Premises used: Measurable.comp, Measurable.prodMk, measurable_snd
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
h_meas : Measurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2
this :
  Eq (α := (p : ι × α) → β) (fun (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2)
    ((fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2) ∘ fun (p : ι × α) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯, p.2))
⊢ Measurable (β := ↥(t_sf n).range) fun (p : ι × α) ↦
    Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯

Tactic:
((t_sf n).measurable.comp measurable_fst).subtype_mk

Premises used: Measurable.comp, Measurable.subtype_mk, MeasureTheory.SimpleFunc.measurable, measurable_fst
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
h_meas : Measurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2
this :
  Eq (α := (p : ι × α) → β) (fun (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2)
    ((fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2) ∘ fun (p : ι × α) ↦
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯, p.2))
⊢ Measurable (β := ↥(t_sf n).range) fun (p : ι × α) ↦
    Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) ⋯

Tactic:
exact ((t_sf n).measurable.comp measurable_fst).subtype_mk

Premises used: Measurable.comp, Measurable.subtype_mk, MeasureTheory.SimpleFunc.measurable, measurable_fst
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
⊢ let this := borel β;
  BorelSpace β

Tactic:
borelize β
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ StronglyMeasurable.{u_7, u_7} (α := ι) id

Tactic:
have h_str_meas : StronglyMeasurable (id : ι → ι) := stronglyMeasurable_id
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
h_str_meas : StronglyMeasurable.{u_7, u_7} (α := ι) id
⊢ ∃ (t : ℕ → ι →ₛ ι), ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))

Tactic:
⟨h_str_meas.approx, fun j x => ?_⟩

Premises used: MeasureTheory.StronglyMeasurable.approx, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
h_str_meas : StronglyMeasurable.{u_7, u_7} (α := ι) id
refine : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((h_str_meas.approx n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
⊢ ∃ (t : ℕ → ι →ₛ ι), ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))

Tactic:
refine ⟨h_str_meas.approx, fun j x => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
h_str_meas : StronglyMeasurable.{u_7, u_7} (α := ι) id
j : ι
x : α
⊢ Tendsto (fun (n : ℕ) ↦ u ((h_str_meas.approx n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))

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

Premises used: Continuous.tendsto, MeasureTheory.StronglyMeasurable.tendsto_approx, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
h_str_meas : StronglyMeasurable.{u_7, u_7} (α := ι) id
j : ι
x : α
⊢ Tendsto (fun (n : ℕ) ↦ u ((h_str_meas.approx n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))

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

Premises used: Continuous.tendsto, MeasureTheory.StronglyMeasurable.tendsto_approx, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
obtain :
  ∀ (t_sf : ℕ → ι →ₛ ι)
    (ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))),
    StronglyMeasurable (uncurry u)
⊢ StronglyMeasurable (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)
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
rw : ∀ (x : ι × α), Tendsto (fun (i : ℕ) ↦ U i x) atTop (𝓝 (u x.1 x.2))
⊢ Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)

Tactic:
rw [tendsto_pi_nhds]

Premises used: tendsto_pi_nhds
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
⊢ ∀ (x : ι × α), Tendsto (fun (i : ℕ) ↦ U i x) atTop (𝓝 (u x.1 x.2))

Tactic:
fun p => ht_sf p.fst p.snd

Premises used: Prod.fst, Prod.snd
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
⊢ ∀ (x : ι × α), Tendsto (fun (i : ℕ) ↦ U i x) atTop (𝓝 (u x.1 x.2))

Tactic:
exact fun p => ht_sf p.fst p.snd
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
⊢ Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)

Tactic:
have h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd) := by
    rw [tendsto_pi_nhds]
    exact fun p => ht_sf p.fst p.snd
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
⊢ StronglyMeasurable (uncurry u)

Tactic:
stronglyMeasurable_of_tendsto _ (fun n => ?_) h_tendsto

Premises used: stronglyMeasurable_of_tendsto
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
refine : ∀ (n : ℕ), StronglyMeasurable (U n)
⊢ StronglyMeasurable (uncurry u)

Tactic:
refine stronglyMeasurable_of_tendsto _ (fun n => ?_) h_tendsto

Premises used: stronglyMeasurable_of_tendsto
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
⊢ StronglyMeasurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2

Tactic:
stronglyMeasurable_iff_measurable_separable.2 ⟨?_, ?_⟩

Premises used: Iff.mpr, stronglyMeasurable_iff_measurable_separable, And.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
refine_1 : Measurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2
refine_2 : IsSeparable.{u_6} (α := β) (range fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2)
⊢ StronglyMeasurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2

Tactic:
refine stronglyMeasurable_iff_measurable_separable.2 ⟨?_, ?_⟩

Premises used: Iff.mpr, stronglyMeasurable_iff_measurable_separable, And.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace ι
inst_1 : MetrizableSpace ι
inst_2 : MeasurableSpace ι
inst_3 : SecondCountableTopology ι
inst_4 : OpensMeasurableSpace ι
inst_5 : TopologicalSpace β
inst_6 : PseudoMetrizableSpace β
inst_7 : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst, inst_5] fun (i : ι) ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
U : (n : ℕ) → (p : ι × α) → β := fun (n : ℕ) (p : ι × α) ↦ u ((t_sf n : (a : ι) → ι) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun (p : ι × α) ↦ u p.1 p.2)
n : ℕ
⊢ Eq (α := (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) → β)
    (fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2)
    ((fun (p : Prod.{u_5, u_7} α ↥(t_sf n).range) ↦ u (↑p.2 : ι) p.1) ∘ Prod.swap)

Tactic:
have :
        (fun p : ↥(t_sf n).range × α => u (↑p.fst) p.snd) =
          (fun p : α × (t_sf n).range => u (↑p.snd) p.fst) ∘ Prod.swap :=
        rfl