awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
neg : MeasurableSet (Function.curry (X m) 0 ⁻¹' {s})
⊢ MeasurableSet (Function.curry (Y m) (n + 1) ⁻¹' {s})

Tactic:
rw [(by aesop : Function.curry (Y m) (n + 1) = Function.curry (X m) 0)]
-- 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
⊢ 0 ≤ n

Tactic:
simp
-- 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
neg : MeasurableSet (Function.curry (X m) 0 ⁻¹' {s})
⊢ MeasurableSet (Function.curry (X m) 0 ⁻¹' {s})

Tactic:
apply 𝓕.mono (i := 0) (by simp)

Premises used: MeasureTheory.Filtration.mono
-- 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 : m < n + 1
this : MeasurableSpace Ω := (↑𝓕 : ℕ → MeasurableSpace Ω) 0
⊢ MeasurableSet (Function.curry (X m) 0 ⁻¹' {s})

Tactic:
(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_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 : m < n + 1
this : MeasurableSpace Ω := (↑𝓕 : ℕ → MeasurableSpace Ω) 0
⊢ MeasurableSet (Function.curry (X 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 : ℕ
refine_2 : Set.Finite.{u_3} (α := E) (⋃ k ∈ Finset.range (m + 1), Set.range (Function.curry (X m) k))
refine_2₁ : Set.range (Y m) ⊆ ⋃ k ∈ Finset.range (m + 1), Set.range (Function.curry (X m) k)
⊢ (Set.range (Y m)).Finite

Tactic:
apply Set.Finite.subset (s := ⋃ k ∈ Finset.range (m + 1), Set.range (Function.curry (X m) k))

Premises used: 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₀ : 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 : ℕ
⊢ (↑(Finset.range (m + 1)) : Set ℕ).Finite

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 : ℕ
refine_2 : ∀ (n : ℕ) (hn : n ∈ (↑(Finset.range (m + 1)) : Set ℕ)), (Set.range (Function.curry (X m) n)).Finite
⊢ Set.Finite.{u_3} (α := E) (⋃ k ∈ Finset.range (m + 1), Set.range (Function.curry (X m) k))

Tactic:
refine Set.Finite.biUnion' (by aesop) (fun n hn ↦ ?_)

Premises used: Set.Finite.biUnion'
-- 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 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
refine_2₁ :
  ∀ (n : ℕ) (hn : n + 1 ∈ (↑(Finset.range (m + 1)) : Set ℕ)), (Set.range (Function.curry (X m) (n + 1))).Finite
⊢ (Set.range (Function.curry (X m) n)).Finite

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 : ℕ
hn : 0 ∈ (↑(Finset.range (m + 1)) : Set ℕ)
⊢ (Set.range (Function.curry (X m) 0)).Finite

Tactic:
@(h₀.approx m).finite_range

Premises used: MeasureTheory.StronglyMeasurable.approx, MeasureTheory.SimpleFunc.finite_range
-- 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 : ℕ
hn : 0 ∈ (↑(Finset.range (m + 1)) : Set ℕ)
⊢ (Set.range (Function.curry (X m) 0)).Finite

Tactic:
exact @(h₀.approx m).finite_range

Premises used: MeasureTheory.StronglyMeasurable.approx, MeasureTheory.SimpleFunc.finite_range
-- 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 n : ℕ
hn : n + 1 ∈ (↑(Finset.range (m + 1)) : Set ℕ)
⊢ (Set.range (Function.curry (X m) (n + 1))).Finite

Tactic:
@((h n).approx m).finite_range

Premises used: MeasureTheory.StronglyMeasurable.approx, MeasureTheory.SimpleFunc.finite_range
-- 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 n : ℕ
hn : n + 1 ∈ (↑(Finset.range (m + 1)) : Set ℕ)
⊢ (Set.range (Function.curry (X m) (n + 1))).Finite

Tactic:
exact @((h n).approx m).finite_range

Premises used: MeasureTheory.StronglyMeasurable.approx, MeasureTheory.SimpleFunc.finite_range
-- 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 : ℕ
e : E
he : e ∈ Set.range (Y m)
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
⊢ 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

Premises used: Set.mem_range, Iff.mp
-- 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 : ℕ
e : E
he : e ∈ Set.range (Y m)
n : ℕ
ω : Ω
hnω : Y m (n, ω) = e
refine_2 : ∃ (i : ℕ) (_ : i ∈ Finset.range (m + 1)) (y : Ω), Function.curry (X m) i y = e
⊢ Membership.mem (γ := Set E) (⋃ k ∈ Finset.range (m + 1), Set.range (Function.curry (X m) k)) e

Tactic:
simp_rw [Set.mem_iUnion, Set.mem_range]

Premises used: Set.mem_range, Set.mem_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 : ℕ
e : E
he : e ∈ Set.range (Y m)
n : ℕ
ω : Ω
hnω : Y m (n, ω) = e
⊢ (if n ≤ m then n else 0) ∈ Finset.range (m + 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 : ℕ
e : E
he : e ∈ Set.range (Y m)
n : ℕ
ω : Ω
hnω : Y m (n, ω) = e
⊢ Function.curry (X m) (if n ≤ m then n else 0) ω = e

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 : ℕ
e : E
he : e ∈ Set.range (Y m)
n : ℕ
ω : Ω
hnω : Y m (n, ω) = e
⊢ ∃ (i : ℕ) (_ : i ∈ Finset.range (m + 1)) (y : Ω), Function.curry (X m) i y = e

Tactic:
exact ⟨if n ≤ m then n else 0, by aesop, ω, by 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)
n : ℕ
ω : Ω
refine_3 : Tendsto (fun (m : ℕ) ↦ X m (n, ω)) atTop (𝓝 (Function.uncurry u (n, ω)))
refine_3₁ :
  EventuallyEq.{0, u_3} (β := E) atTop
    (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, ω))
    fun (m : ℕ) ↦ X m (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, ω)))

Tactic:
rw [tendsto_congr' (f₂ := fun m ↦ X m ⟨n, ω⟩)]

Premises used: Filter.tendsto_congr'
-- 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)
n : ℕ
ω : Ω
refine_3 : Tendsto (fun (m : ℕ) ↦ X m (0, ω)) atTop (𝓝 (Function.uncurry u (0, ω)))
refine_3₁ : ∀ (n : ℕ), Tendsto (fun (m : ℕ) ↦ X m (n + 1, ω)) atTop (𝓝 (Function.uncurry u (n + 1, ω)))
⊢ Tendsto (fun (m : ℕ) ↦ X m (n, ω)) atTop (𝓝 (Function.uncurry u (n, ω)))

Tactic:
rcases n with rfl | n

Premises used: rfl
-- 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)
ω : Ω
⊢ Tendsto (fun (m : ℕ) ↦ X m (0, ω)) atTop (𝓝 (Function.uncurry u (0, ω)))

Tactic:
h₀.tendsto_approx ω

Premises used: MeasureTheory.StronglyMeasurable.tendsto_approx
-- 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)
ω : Ω
⊢ Tendsto (fun (m : ℕ) ↦ X m (0, ω)) atTop (𝓝 (Function.uncurry u (0, ω)))

Tactic:
exact h₀.tendsto_approx ω

Premises used: MeasureTheory.StronglyMeasurable.tendsto_approx
-- 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)
ω : Ω
n : ℕ
⊢ Tendsto (fun (m : ℕ) ↦ X m (n + 1, ω)) atTop (𝓝 (Function.uncurry u (n + 1, ω)))

Tactic:
(h n).tendsto_approx ω

Premises used: MeasureTheory.StronglyMeasurable.tendsto_approx
-- 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)
ω : Ω
n : ℕ
⊢ Tendsto (fun (m : ℕ) ↦ X m (n + 1, ω)) atTop (𝓝 (Function.uncurry u (n + 1, ω)))

Tactic:
exact (h n).tendsto_approx ω

Premises used: MeasureTheory.StronglyMeasurable.tendsto_approx
-- 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)
n : ℕ
ω : Ω
m : ℕ
hm : n ≤ m
simp : Y m (n, ω) = X m (n, ω)
⊢ ({ toFun := Y m, measurableSet_fiber' := ⋯, finite_range' := ⋯ } : (a : ℕ × Ω) → E) (n, ω) = X m (n, ω)

Tactic:
simp
-- 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)
n : ℕ
ω : Ω
m : ℕ
hm : n ≤ m
⊢ Y m (n, ω) = X m (n, ω)

Tactic:
grind
-- 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)
n : ℕ
ω : Ω
h₁ :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ n ≤ x) x} x →
          Membership.mem (γ := Set ℕ)
            {x : ℕ |
              (fun (x : ℕ) ↦
                  Eq.{u_3 + 1} (α := E)
                    ((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, ω) :
                          E))
                      x)
                    ((fun (m : ℕ) ↦ X m (n, ω)) x))
                x}
            x}
      a
h₂ h₃ :
  ∀ (m_1 : ℕ) (hm : n ≤ m_1),
    ({ toFun := Y m_1, measurableSet_fiber' := ⋯, finite_range' := ⋯ } : (a : ℕ × Ω) → E) (n, ω) = X m_1 (n, ω)
⊢ EventuallyEq.{0, u_3} (β := E) atTop
    (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, ω))
    fun (m : ℕ) ↦ X m (n, ω)

Tactic:
filter_upwards [eventually_ge_atTop n] with m hm using by simp; grind

Premises used: Filter.eventually_ge_atTop
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
⊢ IsStronglyPredictable 𝓕 u ↔ StronglyMeasurable (u 0) ∧ ∀ (n : ℕ), StronglyMeasurable (u (n + 1))

Tactic:
⟨fun h𝓕 ↦ ⟨h𝓕.isStronglyProgressive.stronglyAdapted 0, h𝓕.measurable_add_one⟩,
    fun h ↦ .of_measurable_add_one h.1 h.2⟩

Premises used: And.right, And.left, And.intro, MeasureTheory.IsStronglyProgressive.stronglyAdapted, Iff.intro, MeasureTheory.IsStronglyPredictable.of_measurable_add_one, MeasureTheory.IsStronglyPredictable.measurable_add_one, OfNat.ofNat, MeasureTheory.IsStronglyPredictable.isStronglyProgressive