awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
inst_1 : LinearOrder ι
inst_2 : OrderBot ι
inst_3 : MeasurableSpace ι
inst_4 : TopologicalSpace ι
inst_5 : OpensMeasurableSpace ι
inst_6 : OrderClosedTopology ι
𝓕 : Filtration ι m
u : ι → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
i : ι
this_1 : MeasurableSpace (ι × Ω) := 𝓕.predictable
this : MeasurableSpace (Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) :=
  MeasurableSpace.prod (Subtype.instMeasurableSpace (p := fun (x : ι) ↦ x ∈ Set.Iic i)) ((↑𝓕 : ι → MeasurableSpace Ω) i)
X : (m : ℕ) → (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) → E :=
  fun (m_1 : ℕ) (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
    (StronglyMeasurable.approx h𝓕 m_1 : (a : ι × Ω) → E) ((↑x.1 : ι), x.2)
n : Prod.{u_2, u_1} { x : ι // x ∈ Set.Iic i } Ω
⊢ Tendsto.{0, u_3} (β := E)
    (fun (n_1 : ℕ) ↦
      ((fun (m_1 : ℕ) ↦
              ({ toFun := X m_1, measurableSet_fiber' := ⋯, finite_range' := ⋯ } :
                SimpleFunc (Prod.{u_2, u_1} { x : ι // x ∈ Set.Iic i } Ω) E))
            n_1 :
          (a : { x : ι // x ∈ Set.Iic i } × Ω) → E)
        n)
    atTop (𝓝 ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) n))

Tactic:
apply h𝓕.tendsto_approx

Premises used: MeasureTheory.StronglyMeasurable.tendsto_approx
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
inst_1 : LinearOrder ι
inst_2 : OrderBot ι
inst_3 : MeasurableSpace ι
inst_4 : TopologicalSpace ι
inst_5 : OpensMeasurableSpace ι
inst_6 : OrderClosedTopology ι
𝓕 : Filtration ι m
u : ι → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
i : ι
this_1 : MeasurableSpace (ι × Ω) := 𝓕.predictable
this : MeasurableSpace (Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) :=
  MeasurableSpace.prod (Subtype.instMeasurableSpace (p := fun (x : ι) ↦ x ∈ Set.Iic i)) ((↑𝓕 : ι → MeasurableSpace Ω) i)
X : (m : ℕ) → (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) → E :=
  fun (m_1 : ℕ) (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
    (StronglyMeasurable.approx h𝓕 m_1 : (a : ι × Ω) → E) ((↑x.1 : ι), x.2)
⊢ ∀ (x : Prod.{u_2, u_1} { x : ι // x ∈ Set.Iic i } Ω),
    Tendsto.{0, u_3} (β := E)
      (fun (n : ℕ) ↦
        ((fun (m_1 : ℕ) ↦
                ({ toFun := X m_1, measurableSet_fiber' := ⋯, finite_range' := ⋯ } :
                  SimpleFunc (Prod.{u_2, u_1} { x : ι // x ∈ Set.Iic i } Ω) E))
              n :
            (a : { x : ι // x ∈ Set.Iic i } × Ω) → E)
          x)
      atTop (𝓝 ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2) x))

Tactic:
exact fun n ↦ by apply h𝓕.tendsto_approx
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
inst_1 : LinearOrder ι
inst_2 : OrderBot ι
inst_3 : MeasurableSpace ι
inst_4 : TopologicalSpace ι
inst_5 : OpensMeasurableSpace ι
inst_6 : OrderClosedTopology ι
𝓕 : Filtration ι m
u : ι → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
⊢ StronglyAdapted (β := fun (i : ι) ↦ E) 𝓕 u

Tactic:
h𝓕.isStronglyProgressive.stronglyAdapted

Premises used: MeasureTheory.IsStronglyProgressive.stronglyAdapted, MeasureTheory.IsStronglyPredictable.isStronglyProgressive
-- Module: Mathlib.Probability.Process.Predictable
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)
⊢ StronglyMeasurable (u (n + 1))

Tactic:
⟨(fun m ↦ SimpleFunc.mk (X m) ?_ ?_), (fun ω ↦ h𝓕.tendsto_approx ⟨(n + 1), ω⟩)⟩

Premises used: MeasureTheory.SimpleFunc.mk, Prod.mk, HAdd.hAdd, MeasureTheory.StronglyMeasurable.tendsto_approx, Exists.intro, MeasureTheory.StronglyMeasurable, OfNat.ofNat
-- Module: Mathlib.Probability.Process.Predictable
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})
refine_2 : ∀ (m : ℕ), (Set.range (X m)).Finite
⊢ StronglyMeasurable (u (n + 1))

Tactic:
refine ⟨(fun m ↦ SimpleFunc.mk (X m) ?_ ?_), (fun ω ↦ h𝓕.tendsto_approx ⟨(n + 1), ω⟩)⟩
-- Module: Mathlib.Probability.Process.Predictable
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
⊢ X m ⁻¹' {s} =
    {ω : Ω |
      Membership.mem (γ := Set (ℕ × Ω))
        (Set.preimage (β := E) (⇑(StronglyMeasurable.approx h𝓕 m) : (a : ℕ × Ω) → E) {s}) (n + 1, ω)}

Tactic:
aesop
-- Module: Mathlib.Probability.Process.Predictable
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
refine_1 :
  MeasurableSet.{u_1} (α := Ω)
    {ω : Ω |
      Membership.mem (γ := Set (ℕ × Ω))
        (Set.preimage (β := E) (⇑(StronglyMeasurable.approx h𝓕 m) : (a : ℕ × Ω) → E) {s}) (n + 1, ω)}
⊢ MeasurableSet (X m ⁻¹' {s})

Tactic:
rw [(by aesop : X m ⁻¹' {s} = {ω | (n + 1, ω) ∈ h𝓕.approx m ⁻¹' {s}})]
-- Module: Mathlib.Probability.Process.Predictable
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
refine_1 :
  MeasurableSet.{u_1} (α := ℕ × Ω) (Set.preimage (β := E) (⇑(StronglyMeasurable.approx h𝓕 m) : (a : ℕ × Ω) → E) {s})
⊢ MeasurableSet.{u_1} (α := Ω)
    {ω : Ω |
      Membership.mem (γ := Set (ℕ × Ω))
        (Set.preimage (β := E) (⇑(StronglyMeasurable.approx h𝓕 m) : (a : ℕ × Ω) → E) {s}) (n + 1, ω)}

Tactic:
apply measurableSet_prodMk_add_one_of_predictable

Premises used: MeasureTheory.measurableSet_prodMk_add_one_of_predictable
-- Module: Mathlib.Probability.Process.Predictable
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} (α := ℕ × Ω) (Set.preimage (β := E) (⇑(StronglyMeasurable.approx h𝓕 m) : (a : ℕ × Ω) → E) {s})

Tactic:
apply (h𝓕.approx m).measurableSet_fiber

Premises used: MeasureTheory.StronglyMeasurable.approx, MeasureTheory.SimpleFunc.measurableSet_fiber
-- Module: Mathlib.Probability.Process.Predictable
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 : ℕ
refine_2 : Set.range (X m) ⊆ Set.range.{u_3, u_1 + 1} (ι := ℕ × Ω) (⇑(StronglyMeasurable.approx h𝓕 m) : (a : ℕ × Ω) → E)
⊢ (Set.range (X m)).Finite

Tactic:
apply (h𝓕.approx m).finite_range.subset

Premises used: MeasureTheory.StronglyMeasurable.approx, MeasureTheory.SimpleFunc.finite_range, Set.Finite.subset
-- Module: Mathlib.Probability.Process.Predictable
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 : ℕ
refine_2 :
  ∀ (y : Ω),
    Membership.mem (γ := Set E)
      (Set.range.{u_3, u_1 + 1} (ι := ℕ × Ω) (⇑(StronglyMeasurable.approx h𝓕 m) : (a : ℕ × Ω) → E)) (X m y)
⊢ Set.range (X m) ⊆ Set.range.{u_3, u_1 + 1} (ι := ℕ × Ω) (⇑(StronglyMeasurable.approx h𝓕 m) : (a : ℕ × Ω) → E)

Tactic:
rw [Set.range_subset_iff]

Premises used: Set.range_subset_iff
-- Module: Mathlib.Probability.Process.Predictable
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 : ℕ
⊢ ∀ (y : Ω),
    Membership.mem (γ := Set E)
      (Set.range.{u_3, u_1 + 1} (ι := ℕ × Ω) (⇑(StronglyMeasurable.approx h𝓕 m) : (a : ℕ × Ω) → E)) (X m y)

Tactic:
aesop
-- Module: Mathlib.Probability.Process.Predictable
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

Tactic:
⟨fun m ↦ SimpleFunc.mk (Y m) ?_ ?_, ?_⟩

Premises used: MeasureTheory.SimpleFunc.mk, Exists.intro, MeasureTheory.StronglyMeasurable, MeasureTheory.IsStronglyPredictable
-- Module: Mathlib.Probability.Process.Predictable
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
refine_3 :
  ∀ (x : ℕ × Ω),
    Tendsto
      (fun (n : ℕ) ↦
        ((fun (m_1 : ℕ) ↦
                ({ toFun := Y m_1, measurableSet_fiber' := ⋯, finite_range' := ⋯ } : SimpleFunc.{u_1, u_3} (ℕ × Ω) E))
              n :
            (a : ℕ × Ω) → E)
          x)
      atTop (𝓝 (Function.uncurry u x))
⊢ IsStronglyPredictable 𝓕 u

Tactic:
refine ⟨fun m ↦ SimpleFunc.mk (Y m) ?_ ?_, ?_⟩
-- Module: Mathlib.Probability.Process.Predictable
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
⊢ Y m ⁻¹' {s} = ⋃ (n : ℕ), SProd.sprod (α := Set ℕ) {n} (Function.curry (Y m) n ⁻¹' {s})

Tactic:
aesop
-- Module: Mathlib.Probability.Process.Predictable
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
refine_1 : MeasurableSet.{u_1} (α := ℕ × Ω) (⋃ (n : ℕ), SProd.sprod (α := Set ℕ) {n} (Function.curry (Y m) n ⁻¹' {s}))
⊢ MeasurableSet (Y m ⁻¹' {s})

Tactic:
rw [(by aesop : Y m ⁻¹' {s} = ⋃ n : ℕ, {n} ×ˢ ((Function.curry (Y m) n) ⁻¹' {s}))]
-- Module: Mathlib.Probability.Process.Predictable
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}))

Tactic:
MeasurableSet.iUnion <| fun n ↦ ?_

Premises used: MeasurableSet.iUnion
-- Module: Mathlib.Probability.Process.Predictable
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
refine_1 : ∀ (n : ℕ), MeasurableSet (SProd.sprod (α := Set ℕ) {n} (Function.curry (Y m) n ⁻¹' {s}))
⊢ MeasurableSet.{u_1} (α := ℕ × Ω) (⋃ (n : ℕ), SProd.sprod (α := Set ℕ) {n} (Function.curry (Y m) n ⁻¹' {s}))

Tactic:
refine MeasurableSet.iUnion <| fun n ↦ ?_

Premises used: MeasurableSet.iUnion
-- Module: Mathlib.Probability.Process.Predictable
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}))
refine_1₁ : ∀ (n : ℕ), MeasurableSet (SProd.sprod (α := Set ℕ) {n + 1} (Function.curry (Y m) (n + 1) ⁻¹' {s}))
⊢ MeasurableSet (SProd.sprod (α := Set ℕ) {n} (Function.curry (Y m) n ⁻¹' {s}))

Tactic:
rcases n with rfl | n

Premises used: rfl
-- Module: Mathlib.Probability.Process.Predictable
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
refine_1 : MeasurableSet (Function.curry (Y m) 0 ⁻¹' {s})
⊢ MeasurableSet (SProd.sprod (α := Set ℕ) {0} (Function.curry (Y m) 0 ⁻¹' {s}))

Tactic:
apply measurableSet_predictable_singleton_bot_prod

Premises used: MeasureTheory.measurableSet_predictable_singleton_bot_prod
-- Module: Mathlib.Probability.Process.Predictable
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_1 : 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
this : MeasurableSpace Ω := (↑𝓕 : ℕ → MeasurableSpace Ω) 0
⊢ MeasurableSet (Function.curry (Y m) 0 ⁻¹' {s})

Tactic:
(h₀.approx m).measurableSet_fiber s

Premises used: MeasureTheory.StronglyMeasurable.approx, MeasureTheory.SimpleFunc.measurableSet_fiber, ite
-- Module: Mathlib.Probability.Process.Predictable
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_1 : 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
this : MeasurableSpace Ω := (↑𝓕 : ℕ → MeasurableSpace Ω) 0
⊢ MeasurableSet (Function.curry (Y m) 0 ⁻¹' {s})

Tactic:
exact (h₀.approx m).measurableSet_fiber s

Premises used: MeasureTheory.StronglyMeasurable.approx, MeasureTheory.SimpleFunc.measurableSet_fiber
-- Module: Mathlib.Probability.Process.Predictable
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 (Function.curry (Y m) (n + 1) ⁻¹' {s})
⊢ MeasurableSet (SProd.sprod (α := Set ℕ) {n + 1} (Function.curry (Y m) (n + 1) ⁻¹' {s}))

Tactic:
apply measurableSet_predictable_singleton_prod

Premises used: MeasureTheory.measurableSet_predictable_singleton_prod
-- Module: Mathlib.Probability.Process.Predictable
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})
neg : ∀ (hmk : m < n + 1), MeasurableSet (Function.curry (Y m) (n + 1) ⁻¹' {s})
⊢ MeasurableSet (Function.curry (Y m) (n + 1) ⁻¹' {s})

Tactic:
by_cases! hmk : n + 1 ≤ m
-- Module: Mathlib.Probability.Process.Predictable
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
⊢ Function.curry (Y m) (n + 1) = Function.curry (X m) (n + 1)

Tactic:
aesop
-- Module: Mathlib.Probability.Process.Predictable
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
pos : MeasurableSet (Function.curry (X m) (n + 1) ⁻¹' {s})
⊢ MeasurableSet (Function.curry (Y m) (n + 1) ⁻¹' {s})

Tactic:
rw [(by aesop : Function.curry (Y m) (n + 1) = Function.curry (X m) (n + 1))]
-- Module: Mathlib.Probability.Process.Predictable
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_1 : 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
this : MeasurableSpace Ω := (↑𝓕 : ℕ → MeasurableSpace Ω) n
⊢ MeasurableSet (Function.curry (X m) (n + 1) ⁻¹' {s})

Tactic:
((h n).approx m).measurableSet_fiber s

Premises used: MeasureTheory.StronglyMeasurable.approx, MeasureTheory.SimpleFunc.measurableSet_fiber
-- Module: Mathlib.Probability.Process.Predictable
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_1 : 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
this : MeasurableSpace Ω := (↑𝓕 : ℕ → MeasurableSpace Ω) n
⊢ MeasurableSet (Function.curry (X m) (n + 1) ⁻¹' {s})

Tactic:
exact ((h n).approx m).measurableSet_fiber s

Premises used: MeasureTheory.StronglyMeasurable.approx, MeasureTheory.SimpleFunc.measurableSet_fiber
-- Module: Mathlib.Probability.Process.Predictable
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
⊢ Function.curry (Y m) (n + 1) = Function.curry (X m) 0

Tactic:
aesop