awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst : TopologicalSpace β
inst_1 : Zero β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (support.{u_1, u_2} (M := β) (⇑(hf.approx n) : (a : α) → β) ∪
          support.{u_1, u_2} (M := β) (⇑(hg.approx n) : (a : α) → β)) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
exact measure_union_lt_top_iff.mpr ⟨hf.fin_support_approx n, hg.fin_support_approx n⟩

Premises used: Iff.mpr, MeasureTheory.measure_union_lt_top_iff, And.intro, MeasureTheory.FinStronglyMeasurable.fin_support_approx
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst : TopologicalSpace β
inst_1 : Zero β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
⊢ FinStronglyMeasurable (f ⊓ g) μ

Tactic:
⟨fun n => hf.approx n ⊓ hg.approx n, fun n => ?_, fun x =>
      (hf.tendsto_approx x).inf_nhds (hg.tendsto_approx x)⟩

Premises used: MeasureTheory.FinStronglyMeasurable.tendsto_approx, Filter.Tendsto.inf_nhds, MeasureTheory.FinStronglyMeasurable.approx, And.intro, Exists.intro, MeasureTheory.FinStronglyMeasurable, Min.min
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst : TopologicalSpace β
inst_1 : Zero β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (support.{u_1, u_2} (M := β) (⇑((fun (n : ℕ) ↦ hf.approx n ⊓ hg.approx n) n) : (a : α) → β)) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
⊢ FinStronglyMeasurable (f ⊓ g) μ

Tactic:
refine
    ⟨fun n => hf.approx n ⊓ hg.approx n, fun n => ?_, fun x =>
      (hf.tendsto_approx x).inf_nhds (hg.tendsto_approx x)⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst : TopologicalSpace β
inst_1 : Zero β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (support.{u_1, u_2} (M := β) (⇑((fun (n : ℕ) ↦ hf.approx n ⊓ hg.approx n) n) : (a : α) → β)) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
(measure_mono (support_inf _ _)).trans_lt ?_

Premises used: Function.support_inf, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst : TopologicalSpace β
inst_1 : Zero β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
refine :
  LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (support.{u_1, u_2} (M := β) (⇑(hf.approx n) : (a : α) → β) ∪
          support.{u_1, u_2} (M := β) (⇑(hg.approx n) : (a : α) → β)) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (support.{u_1, u_2} (M := β) (⇑((fun (n : ℕ) ↦ hf.approx n ⊓ hg.approx n) n) : (a : α) → β)) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
refine (measure_mono (support_inf _ _)).trans_lt ?_

Premises used: Function.support_inf, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst : TopologicalSpace β
inst_1 : Zero β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (support.{u_1, u_2} (M := β) (⇑(hf.approx n) : (a : α) → β) ∪
          support.{u_1, u_2} (M := β) (⇑(hg.approx n) : (a : α) → β)) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
measure_union_lt_top_iff.mpr ⟨hf.fin_support_approx n, hg.fin_support_approx n⟩

Premises used: Iff.mpr, MeasureTheory.measure_union_lt_top_iff, And.intro, MeasureTheory.FinStronglyMeasurable.fin_support_approx
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst : TopologicalSpace β
inst_1 : Zero β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (support.{u_1, u_2} (M := β) (⇑(hf.approx n) : (a : α) → β) ∪
          support.{u_1, u_2} (M := β) (⇑(hg.approx n) : (a : α) → β)) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
exact measure_union_lt_top_iff.mpr ⟨hf.fin_support_approx n, hg.fin_support_approx n⟩

Premises used: Iff.mpr, MeasureTheory.measure_union_lt_top_iff, And.intro, MeasureTheory.FinStronglyMeasurable.fin_support_approx
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
f : α → β
inst : TopologicalSpace β
inst_1 : T2Space β
inst_2 : Zero β
x : MeasurableSpace α
μ : Measure α
⊢ FinStronglyMeasurable f μ ↔
    StronglyMeasurable f ∧ ∃ (t : Set α), MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)

Tactic:
⟨fun hf => ⟨hf.stronglyMeasurable, hf.exists_set_sigmaFinite⟩, fun hf =>
    hf.1.finStronglyMeasurable_of_set_sigmaFinite hf.2.choose_spec.1 hf.2.choose_spec.2.1
      hf.2.choose_spec.2.2⟩

Premises used: Exists.choose_spec, MeasureTheory.FinStronglyMeasurable.exists_set_sigmaFinite, And.right, And.left, MeasureTheory.StronglyMeasurable.finStronglyMeasurable_of_set_sigmaFinite, And.intro, MeasureTheory.FinStronglyMeasurable.stronglyMeasurable, Iff.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
G : Type u_5
inst : SeminormedAddCommGroup G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : SecondCountableTopology G
f : α → G
_m0 : MeasurableSpace α
μ : Measure α
inst_4 : SigmaFinite μ
⊢ FinStronglyMeasurable f μ ↔ Measurable f

Tactic:
⟨fun h => h.measurable, fun h => (Measurable.stronglyMeasurable h).finStronglyMeasurable μ⟩

Premises used: MeasureTheory.StronglyMeasurable.finStronglyMeasurable, Measurable.stronglyMeasurable, MeasureTheory.FinStronglyMeasurable.measurable, Iff.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
G : Type u_5
inst : SeminormedAddCommGroup G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : SecondCountableTopology G
f : α → G
_m0 : MeasurableSpace α
μ : Measure α
inst_4 : SigmaFinite μ
hf : Measurable f
⊢ FinStronglyMeasurable f μ

Tactic:
(finStronglyMeasurable_iff_measurable μ).mpr hf

Premises used: Iff.mpr, MeasureTheory.finStronglyMeasurable_iff_measurable
-- 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)
⊢ 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 ι
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)
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 ι
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)
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 ι
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)
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 ι
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)
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 ι
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)
obtain :
  ∀ (t_sf : ℕ → ι →ₛ ι)
    (ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))),
    Measurable (uncurry u)
⊢ 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)
-- 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
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 ι
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
⊢ ∀ (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 ι
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
⊢ ∀ (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 ι
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
⊢ 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 ι
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)
⊢ Measurable (uncurry u)

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

Premises used: measurable_of_tendsto_metrizable
-- 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)
refine : ∀ (n : ℕ), Measurable (U n)
⊢ Measurable (uncurry u)

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

Premises used: measurable_of_tendsto_metrizable
-- 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 : ℕ
⊢ 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
-- 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 : ℕ
this :
  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)
rw : Measurable (β := β) fun (p : Prod.{u_5, u_7} α ↥(t_sf n).range) ↦ u (↑p.2 : ι) p.1
⊢ Measurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2

Tactic:
rw [this, @measurable_swap_iff α (↥(t_sf n).range) β m]

Premises used: measurable_swap_iff
-- 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 : ℕ
this :
  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)
⊢ Measurable (β := β) fun (p : Prod.{u_5, u_7} α ↥(t_sf n).range) ↦ u (↑p.2 : ι) p.1

Tactic:
measurable_from_prod_countable_left fun j => h j

Premises used: measurable_from_prod_countable_left, Subtype.val
-- 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 : ℕ
this :
  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)
⊢ Measurable (β := β) fun (p : Prod.{u_5, u_7} α ↥(t_sf n).range) ↦ u (↑p.2 : ι) p.1

Tactic:
exact measurable_from_prod_countable_left fun j => h 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 ι
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 : ℕ
⊢ Measurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2

Tactic:
have h_meas : Measurable fun p : (t_sf n).range × α => u (↑p.fst) p.snd := by
    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
    rw [this, @measurable_swap_iff α (↥(t_sf n).range) β m]
    exact measurable_from_prod_countable_left fun j => h j