awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 := β) (⇑((fun (n : ℕ) ↦ hf.approx n ⊔ hg.approx n) n) : (a : α) → β)) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
have 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∞)
Tactic: refine (measure_mono (support_sup _ _)).trans_lt ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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) μ
have 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∞)
Tactic: refine
    ⟨fun n => hf.approx n ⊓ hg.approx n, fun n => ?_, fun x =>
      (hf.tendsto_approx x).inf_nhds (hg.tendsto_approx x)⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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∞)
have 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∞)
Tactic: refine (measure_mono (support_inf _ _)).trans_lt ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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 : ℕ → ι →ₛ ι), ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
have h_str_meas : StronglyMeasurable.{u_7, u_7} (α := ι) id
Tactic: have h_str_meas : StronglyMeasurable (id : ι → ι) := stronglyMeasurable_id
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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))
have refine : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((h_str_meas.approx n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
Tactic: refine ⟨h_str_meas.approx, fun j x => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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)
⊢ Measurable (uncurry u)
have obtain : ∀ (t_sf : ℕ → ι →ₛ ι)
  (ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))),
  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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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)
have rw : ∀ (x : ι × α), Tendsto (fun (i : ℕ) ↦ U i x) atTop (𝓝 (u x.1 x.2))
Tactic: rw [tendsto_pi_nhds]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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
⊢ Measurable (uncurry u)
have h_tendsto : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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)
have refine : ∀ (n : ℕ), Measurable (U n)
Tactic: refine measurable_of_tendsto_metrizable (fun n => ?_) h_tendsto
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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
have 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)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2
have rw : Measurable (β := β) fun (p : Prod.{u_5, u_7} α ↥(t_sf n).range) ↦ u (↑p.2 : ι) p.1
Tactic: rw [this, @measurable_swap_iff α (↥(t_sf n).range) β m]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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 (U n)
have h_meas : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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
⊢ Measurable (U n)
have 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) sorry, 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 (U n)
have 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) sorry, p.2))
Tactic: simp_rw [U, this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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))
have refine : Measurable (β := ↥(t_sf n).range) fun (p : ι × α) ↦
  Subtype.mk (p := fun (x : ι) ↦ x ∈ (t_sf n).range) ((t_sf n : (a : ι) → ι) p.1) sorry
Tactic: refine h_meas.comp (Measurable.prodMk ?_ measurable_snd)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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)
⊢ StronglyMeasurable (uncurry u)
have this : let this := borel β;
BorelSpace β
Tactic: borelize β
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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 : ℕ → ι →ₛ ι), ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
have h_str_meas : StronglyMeasurable.{u_7, u_7} (α := ι) id
Tactic: have h_str_meas : StronglyMeasurable (id : ι → ι) := stronglyMeasurable_id
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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))
have refine : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((h_str_meas.approx n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))
Tactic: refine ⟨h_str_meas.approx, fun j x => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 (uncurry u)
have obtain : ∀ (t_sf : ℕ → ι →ₛ ι)
  (ht_sf : ∀ (j : ι) (x : α), Tendsto (fun (n : ℕ) ↦ u ((t_sf n : (a : ι) → ι) j) x) atTop (𝓝 (u j x))),
  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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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)
have rw : ∀ (x : ι × α), Tendsto (fun (i : ℕ) ↦ U i x) atTop (𝓝 (u x.1 x.2))
Tactic: rw [tendsto_pi_nhds]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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
⊢ StronglyMeasurable (uncurry u)
have h_tendsto : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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)
have refine : ∀ (n : ℕ), StronglyMeasurable (U n)
Tactic: refine stronglyMeasurable_of_tendsto _ (fun n => ?_) h_tendsto
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
have refine_1 : Measurable (β := β) fun (p : Prod.{u_7, u_5} (↥(t_sf n).range) α) ↦ u (↑p.1 : ι) p.2
Tactic: refine stronglyMeasurable_iff_measurable_separable.2 ⟨?_, ?_⟩