awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
n : ℕ
this_1 : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
this : MeasurableSpace Ω := (↑𝓕 : ℕ → MeasurableSpace Ω) n
X : (m : ℕ) → Ω → E := fun (m_1 : ℕ) ↦ Function.curry (⇑(StronglyMeasurable.approx h𝓕 m_1) : (a : ℕ × Ω) → E) (n + 1)
refine_1 : ∀ (m_1 : ℕ) (x : E), MeasurableSet (X m_1 ⁻¹' {x})
⊢ StronglyMeasurable (u (n + 1))
have refine_2 : ∀ (m : ℕ), (Set.range (X m)).Finite
Tactic: refine ⟨(fun m ↦ SimpleFunc.mk (X m) ?_ ?_), (fun ω ↦ h𝓕.tendsto_approx ⟨(n + 1), ω⟩)⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
n : ℕ
this_1 : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
this : MeasurableSpace Ω := (↑𝓕 : ℕ → MeasurableSpace Ω) n
X : (m : ℕ) → Ω → E := fun (m : ℕ) ↦ Function.curry (⇑(StronglyMeasurable.approx h𝓕 m) : (a : ℕ × Ω) → E) (n + 1)
m : ℕ
s : E
⊢ MeasurableSet (X m ⁻¹' {s})
have refine_1 : MeasurableSet.{u_1} (α := Ω)
  {ω : Ω |
    Membership.mem (γ := Set (ℕ × Ω)) (Set.preimage (β := E) (⇑(StronglyMeasurable.approx h𝓕 m) : (a : ℕ × Ω) → E) {s})
      (n + 1, ω)}
Tactic: rw [(by aesop : X m ⁻¹' {s} = {ω | (n + 1, ω) ∈ h𝓕.approx m ⁻¹' {s}})]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
n : ℕ
this_1 : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
this : MeasurableSpace Ω := (↑𝓕 : ℕ → MeasurableSpace Ω) n
X : (m : ℕ) → Ω → E := fun (m : ℕ) ↦ Function.curry (⇑(StronglyMeasurable.approx h𝓕 m) : (a : ℕ × Ω) → E) (n + 1)
m : ℕ
s : E
⊢ MeasurableSet.{u_1} (α := Ω)
    {ω : Ω |
      Membership.mem (γ := Set (ℕ × Ω))
        (Set.preimage (β := E) (⇑(StronglyMeasurable.approx h𝓕 m) : (a : ℕ × Ω) → E) {s}) (n + 1, ω)}
have refine_1 : MeasurableSet.{u_1} (α := ℕ × Ω) (Set.preimage (β := E) (⇑(StronglyMeasurable.approx h𝓕 m) : (a : ℕ × Ω) → E) {s})
Tactic: apply measurableSet_prodMk_add_one_of_predictable
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
n : ℕ
this_1 : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
this : MeasurableSpace Ω := (↑𝓕 : ℕ → MeasurableSpace Ω) n
X : (m : ℕ) → Ω → E := fun (m : ℕ) ↦ Function.curry (⇑(StronglyMeasurable.approx h𝓕 m) : (a : ℕ × Ω) → E) (n + 1)
m : ℕ
⊢ (Set.range (X m)).Finite
have refine_2 : Set.range (X m) ⊆ Set.range.{u_3, u_1 + 1} (ι := ℕ × Ω) (⇑(StronglyMeasurable.approx h𝓕 m) : (a : ℕ × Ω) → E)
Tactic: apply (h𝓕.approx m).finite_range.subset
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
n : ℕ
this_1 : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
this : MeasurableSpace Ω := (↑𝓕 : ℕ → MeasurableSpace Ω) n
X : (m : ℕ) → Ω → E := fun (m : ℕ) ↦ Function.curry (⇑(StronglyMeasurable.approx h𝓕 m) : (a : ℕ × Ω) → E) (n + 1)
m : ℕ
⊢ Set.range (X m) ⊆ Set.range.{u_3, u_1 + 1} (ι := ℕ × Ω) (⇑(StronglyMeasurable.approx h𝓕 m) : (a : ℕ × Ω) → E)
have refine_2 : ∀ (y : Ω),
  Membership.mem (γ := Set E)
    (Set.range.{u_3, u_1 + 1} (ι := ℕ × Ω) (⇑(StronglyMeasurable.approx h𝓕 m) : (a : ℕ × Ω) → E)) (X m y)
Tactic: rw [Set.range_subset_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m_1 : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m_1 : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m_1 : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
⊢ IsStronglyPredictable 𝓕 u
have refine_1 : ∀ (m_1 : ℕ) (x : E), MeasurableSet (Y m_1 ⁻¹' {x})
Tactic: refine ⟨fun m ↦ SimpleFunc.mk (Y m) ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m_1 : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m_1 : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m_1 : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
refine_1 : ∀ (m_1 : ℕ) (x : E), MeasurableSet (Y m_1 ⁻¹' {x})
⊢ IsStronglyPredictable 𝓕 u
have refine_2 : ∀ (m : ℕ), (Set.range (Y m)).Finite
Tactic: refine ⟨fun m ↦ SimpleFunc.mk (Y m) ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m_1 : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m_1 : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m_1 : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
refine_1 : ∀ (m_1 : ℕ) (x : E), MeasurableSet (Y m_1 ⁻¹' {x})
refine_2 : ∀ (m : ℕ), (Set.range (Y m)).Finite
⊢ IsStronglyPredictable 𝓕 u
have refine_3 : ∀ (x : ℕ × Ω),
  Tendsto
    (fun (n : ℕ) ↦
      ((fun (m_1 : ℕ) ↦
              ({ toFun := Y m_1, measurableSet_fiber' := sorry, finite_range' := sorry } : SimpleFunc.{u_1, u_3} (ℕ × Ω) E))
            n :
          (a : ℕ × Ω) → E)
        x)
    atTop (𝓝 (Function.uncurry u x))
Tactic: refine ⟨fun m ↦ SimpleFunc.mk (Y m) ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
s : E
⊢ MeasurableSet (Y m ⁻¹' {s})
have refine_1 : MeasurableSet.{u_1} (α := ℕ × Ω) (⋃ (n : ℕ), SProd.sprod (α := Set ℕ) {n} (Function.curry (Y m) n ⁻¹' {s}))
Tactic: rw [(by aesop : Y m ⁻¹' {s} = ⋃ n : ℕ, {n} ×ˢ ((Function.curry (Y m) n) ⁻¹' {s}))]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
s : E
⊢ MeasurableSet.{u_1} (α := ℕ × Ω) (⋃ (n : ℕ), SProd.sprod (α := Set ℕ) {n} (Function.curry (Y m) n ⁻¹' {s}))
have refine_1 : ∀ (n : ℕ), MeasurableSet (SProd.sprod (α := Set ℕ) {n} (Function.curry (Y m) n ⁻¹' {s}))
Tactic: refine MeasurableSet.iUnion <| fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
s : E
n : ℕ
⊢ MeasurableSet (SProd.sprod (α := Set ℕ) {n} (Function.curry (Y m) n ⁻¹' {s}))
have refine_1 : MeasurableSet (SProd.sprod (α := Set ℕ) {0} (Function.curry (Y m) 0 ⁻¹' {s}))
Tactic: rcases n with rfl | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
s : E
n : ℕ
refine_1 : MeasurableSet (SProd.sprod (α := Set ℕ) {0} (Function.curry (Y m) 0 ⁻¹' {s}))
⊢ MeasurableSet (SProd.sprod (α := Set ℕ) {n} (Function.curry (Y m) n ⁻¹' {s}))
have refine_1₁ : ∀ (n : ℕ), MeasurableSet (SProd.sprod (α := Set ℕ) {n + 1} (Function.curry (Y m) (n + 1) ⁻¹' {s}))
Tactic: rcases n with rfl | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
s : E
⊢ MeasurableSet (SProd.sprod (α := Set ℕ) {0} (Function.curry (Y m) 0 ⁻¹' {s}))
have refine_1 : MeasurableSet (Function.curry (Y m) 0 ⁻¹' {s})
Tactic: apply measurableSet_predictable_singleton_bot_prod
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
s : E
n : ℕ
⊢ MeasurableSet (SProd.sprod (α := Set ℕ) {n + 1} (Function.curry (Y m) (n + 1) ⁻¹' {s}))
have refine_1 : MeasurableSet (Function.curry (Y m) (n + 1) ⁻¹' {s})
Tactic: apply measurableSet_predictable_singleton_prod
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
s : E
n : ℕ
⊢ MeasurableSet (Function.curry (Y m) (n + 1) ⁻¹' {s})
have pos : ∀ (hmk : n + 1 ≤ m), MeasurableSet (Function.curry (Y m) (n + 1) ⁻¹' {s})
Tactic: by_cases! hmk : n + 1 ≤ m
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
s : E
n : ℕ
pos : ∀ (hmk : n + 1 ≤ m), MeasurableSet (Function.curry (Y m) (n + 1) ⁻¹' {s})
⊢ MeasurableSet (Function.curry (Y m) (n + 1) ⁻¹' {s})
have neg : ∀ (hmk : m < n + 1), MeasurableSet (Function.curry (Y m) (n + 1) ⁻¹' {s})
Tactic: by_cases! hmk : n + 1 ≤ m
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
s : E
n : ℕ
hmk : n + 1 ≤ m
⊢ MeasurableSet (Function.curry (Y m) (n + 1) ⁻¹' {s})
have pos : MeasurableSet (Function.curry (X m) (n + 1) ⁻¹' {s})
Tactic: rw [(by aesop : Function.curry (Y m) (n + 1) = Function.curry (X m) (n + 1))]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
s : E
n : ℕ
hmk : m < n + 1
⊢ MeasurableSet (Function.curry (Y m) (n + 1) ⁻¹' {s})
have neg : MeasurableSet (Function.curry (X m) 0 ⁻¹' {s})
Tactic: rw [(by aesop : Function.curry (Y m) (n + 1) = Function.curry (X m) 0)]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
s : E
n : ℕ
hmk : m < n + 1
⊢ MeasurableSet (Function.curry (X m) 0 ⁻¹' {s})
have neg : MeasurableSet (Function.curry (X m) 0 ⁻¹' {s})
Tactic: apply 𝓕.mono (i := 0) (by simp)
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
⊢ (Set.range (Y m)).Finite
have refine_2 : Set.Finite.{u_3} (α := E) (⋃ k ∈ Finset.range (m + 1), Set.range (Function.curry (X m) k))
Tactic: apply Set.Finite.subset (s := ⋃ k ∈ Finset.range (m + 1), Set.range (Function.curry (X m) k))
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
refine_2 : Set.Finite.{u_3} (α := E) (⋃ k ∈ Finset.range (m + 1), Set.range (Function.curry (X m) k))
⊢ (Set.range (Y m)).Finite
have refine_2₁ : Set.range (Y m) ⊆ ⋃ k ∈ Finset.range (m + 1), Set.range (Function.curry (X m) k)
Tactic: apply Set.Finite.subset (s := ⋃ k ∈ Finset.range (m + 1), Set.range (Function.curry (X m) k))
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
⊢ Set.Finite.{u_3} (α := E) (⋃ k ∈ Finset.range (m + 1), Set.range (Function.curry (X m) k))
have refine_2 : ∀ (n : ℕ) (hn : n ∈ (↑(Finset.range (m + 1)) : Set ℕ)), (Set.range (Function.curry (X m) n)).Finite
Tactic: refine Set.Finite.biUnion' (by aesop) (fun n hn ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m n : ℕ
hn : n ∈ (↑(Finset.range (m + 1)) : Set ℕ)
⊢ (Set.range (Function.curry (X m) n)).Finite
have refine_2 : ∀ (hn : 0 ∈ (↑(Finset.range (m + 1)) : Set ℕ)), (Set.range (Function.curry (X m) 0)).Finite
Tactic: rcases n with rfl | n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m n : ℕ
hn : n ∈ (↑(Finset.range (m + 1)) : Set ℕ)
refine_2 : ∀ (hn : 0 ∈ (↑(Finset.range (m + 1)) : Set ℕ)), (Set.range (Function.curry (X m) 0)).Finite
⊢ (Set.range (Function.curry (X m) n)).Finite
have refine_2₁ : ∀ (n : ℕ) (hn : n + 1 ∈ (↑(Finset.range (m + 1)) : Set ℕ)), (Set.range (Function.curry (X m) (n + 1))).Finite
Tactic: rcases n with rfl | n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
e : E
he : e ∈ Set.range (Y m)
⊢ Membership.mem (γ := Set E) (⋃ k ∈ Finset.range (m + 1), Set.range (Function.curry (X m) k)) e
have refine_2 : ∀ (n : ℕ) (ω : Ω) (hnω : Y m (n, ω) = e),
  Membership.mem (γ := Set E) (⋃ k ∈ Finset.range (m + 1), Set.range (Function.curry (X m) k)) e
Tactic: obtain ⟨⟨n, ω⟩, hnω⟩ := Set.mem_range.mp he
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m_1
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
e : E
he : e ∈ Set.range (Y m)
n : ℕ
ω : Ω
hnω : Y m (n, ω) = e
⊢ Membership.mem (γ := Set E) (⋃ k ∈ Finset.range (m + 1), Set.range (Function.curry (X m) k)) e
have refine_2 : ∃ (i : ℕ) (_ : i ∈ Finset.range (m + 1)) (y : Ω), Function.curry (X m) i y = e
Tactic: simp_rw [Set.mem_iUnion, Set.mem_range]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m_1 : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m_1 : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m_1 : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
n : ℕ
ω : Ω
⊢ Tendsto
    (fun (n_1 : ℕ) ↦
      ((fun (m_1 : ℕ) ↦
              ({ toFun := Y m_1, measurableSet_fiber' := ⋯, finite_range' := ⋯ } : SimpleFunc.{u_1, u_3} (ℕ × Ω) E))
            n_1 :
          (a : ℕ × Ω) → E)
        (n, ω))
    atTop (𝓝 (Function.uncurry u (n, ω)))
have refine_3 : Tendsto (fun (m : ℕ) ↦ X m (n, ω)) atTop (𝓝 (Function.uncurry u (n, ω)))
Tactic: rw [tendsto_congr' (f₂ := fun m ↦ X m ⟨n, ω⟩)]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : (m : ℕ) → (x : ℕ × Ω) → E :=
  fun (m_1 : ℕ) (x : ℕ × Ω) ↦
    match (motive := ℕ → E) x.1 with
    | 0 => (h₀.approx m_1 : (a : Ω) → E) x.2
    | n.succ => (⋯.approx m_1 : (a : Ω) → E) x.2
Y : (m : ℕ) → (x : ℕ × Ω) → E := fun (m : ℕ) (x : ℕ × Ω) ↦ if x.1 ≤ m then X m x else X m (0, x.2)
n : ℕ
ω : Ω
refine_3 : Tendsto (fun (m : ℕ) ↦ X m (n, ω)) atTop (𝓝 (Function.uncurry u (n, ω)))
⊢ Tendsto
    (fun (n_1 : ℕ) ↦
      ((fun (m_1 : ℕ) ↦
              ({ toFun := Y m_1, measurableSet_fiber' := ⋯, finite_range' := ⋯ } : SimpleFunc.{u_1, u_3} (ℕ × Ω) E))
            n_1 :
          (a : ℕ × Ω) → E)
        (n, ω))
    atTop (𝓝 (Function.uncurry u (n, ω)))
have refine_3₁ : EventuallyEq.{0, u_3} (β := E) atTop
  (fun (n_1 : ℕ) ↦
    ((fun (m_1 : ℕ) ↦
            ({ toFun := Y m_1, measurableSet_fiber' := sorry, finite_range' := sorry } : SimpleFunc.{u_1, u_3} (ℕ × Ω) E))
          n_1 :
        (a : ℕ × Ω) → E)
      (n, ω))
  fun (m : ℕ) ↦ X m (n, ω)
Tactic: rw [tendsto_congr' (f₂ := fun m ↦ X m ⟨n, ω⟩)]