awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (n + 1, ω) ∈ s}
have rw : MeasurableSet (α := Ω)
  (Prod.mk (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.singleton (n + 1)) (n + 1) sorry) ⁻¹'
    (fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' s)
Tactic: rw [(by aesop : {ω | (n + 1, ω) ∈ s} = (Prod.mk (α := Set.singleton (n + 1)) (β := Ω)
      ⟨n + 1, rfl⟩) ⁻¹' ((fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' s))]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
⊢ MeasurableSet (α := Ω)
    (Prod.mk (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.singleton (n + 1)) (n + 1) ⋯) ⁻¹'
      (fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' s)
have refine : Measurable (β := ℕ × Ω) fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)
Tactic: refine measurableSet_preimage (mβ := Subtype.instMeasurableSpace.prod (𝓕 n))
    measurable_prodMk_left <| measurableSet_preimage ?_ hs
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
⊢ 𝓕.predictable ≤
    MeasurableSpace.map (fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2))
      (MeasurableSpace.prod (Subtype.instMeasurableSpace (p := fun (x : ℕ) ↦ x ∈ Set.singleton (n + 1)))
        ((↑𝓕 : ℕ → MeasurableSpace Ω) n))
have refine : ∀ (t : Set (ℕ × Ω)),
  Membership.mem (γ := Set (Set (ℕ × Ω)))
      ({s : Set (ℕ × Ω) | ∃ (A : Set Ω), MeasurableSet A ∧ s = SProd.sprod (α := Set ℕ) {⊥} A} ∪
        {s : Set (ℕ × Ω) | ∃ (i : ℕ) (A : Set Ω), MeasurableSet A ∧ s = Set.Ioi i ×ˢ A})
      t →
    MeasurableSet t
Tactic: refine MeasurableSpace.generateFrom_le ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet (SProd.sprod (α := Set ℕ) {⊥} A)
have inl : MeasurableSet.{u_1} (α := { x : ℕ // x ∈ Set.singleton (n + 1) } × Ω) ∅
Tactic: rw [MeasurableSpace.map_def,
      (_ : (fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' ({⊥} ×ˢ A) = ∅)]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
inl : MeasurableSet.{u_1} (α := { x : ℕ // x ∈ Set.singleton (n + 1) } × Ω) ∅
⊢ MeasurableSet (SProd.sprod (α := Set ℕ) {⊥} A)
have rw : Eq (α := Set ((↑(Set.singleton (n + 1)) : Type) × Ω))
  ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' SProd.sprod (α := Set ℕ) {⊥} A) ∅
Tactic: rw [MeasurableSpace.map_def,
      (_ : (fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' ({⊥} ×ˢ A) = ∅)]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ Eq (α := Set ((↑(Set.singleton (n + 1)) : Type) × Ω))
    ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' SProd.sprod (α := Set ℕ) {⊥} A) ∅
have h : ∀ (p : (↑(Set.singleton (n + 1)) : Type) × Ω),
  Membership.mem (γ := Set ((↑(Set.singleton (n + 1)) : Type) × Ω))
      ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' SProd.sprod (α := Set ℕ) {⊥} A) p ↔
    Membership.mem (γ := Set ((↑(Set.singleton (n + 1)) : Type) × Ω)) ∅ p
Tactic: ext p
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
p : (↑(Set.singleton (n + 1)) : Type) × Ω
⊢ Membership.mem (γ := Set ((↑(Set.singleton (n + 1)) : Type) × Ω))
      ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' SProd.sprod (α := Set ℕ) {⊥} A) p ↔
    Membership.mem (γ := Set ((↑(Set.singleton (n + 1)) : Type) × Ω)) ∅ p
have h : (↑p.1 : ℕ) = 0 → p.2 ∉ A
Tactic: simp only [Nat.bot_eq_zero, Set.mem_preimage, Set.mem_prod, Set.mem_singleton_iff,
        Set.mem_empty_iff_false, iff_false, not_and]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet (α := { x : ℕ // x ∈ Set.singleton (n + 1) } × Ω)
    ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' Set.Ioi i ×ˢ A)
have inr : ∀ (hni : n < i),
  MeasurableSet (α := { x : ℕ // x ∈ Set.singleton (n + 1) } × Ω)
    ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' Set.Ioi i ×ˢ A)
Tactic: obtain hni | hin := lt_or_ge n i
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
inr :
  ∀ (hni : n < i),
    MeasurableSet (α := { x : ℕ // x ∈ Set.singleton (n + 1) } × Ω)
      ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' Set.Ioi i ×ˢ A)
⊢ MeasurableSet (α := { x : ℕ // x ∈ Set.singleton (n + 1) } × Ω)
    ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' Set.Ioi i ×ˢ A)
have inr₁ : ∀ (hin : i ≤ n),
  MeasurableSet (α := { x : ℕ // x ∈ Set.singleton (n + 1) } × Ω)
    ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' Set.Ioi i ×ˢ A)
Tactic: obtain hni | hin := lt_or_ge n i
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
⊢ MeasurableSet (α := { x : ℕ // x ∈ Set.singleton (n + 1) } × Ω)
    ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' Set.Ioi i ×ˢ A)
have inr : MeasurableSet.{u_1} (α := { x : ℕ // x ∈ Set.singleton (n + 1) } × Ω) ∅
Tactic: rw [(_ : (fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' (Set.Ioi i ×ˢ A) = ∅)]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
inr : MeasurableSet.{u_1} (α := { x : ℕ // x ∈ Set.singleton (n + 1) } × Ω) ∅
⊢ MeasurableSet (α := { x : ℕ // x ∈ Set.singleton (n + 1) } × Ω)
    ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' Set.Ioi i ×ˢ A)
have rw : Eq (α := Set ((↑(Set.singleton (n + 1)) : Type) × Ω))
  ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' Set.Ioi i ×ˢ A) ∅
Tactic: rw [(_ : (fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' (Set.Ioi i ×ˢ A) = ∅)]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
⊢ Eq (α := Set ((↑(Set.singleton (n + 1)) : Type) × Ω))
    ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' Set.Ioi i ×ˢ A) ∅
have h : ∀ (p : (↑(Set.singleton (n + 1)) : Type) × Ω),
  Membership.mem (γ := Set ((↑(Set.singleton (n + 1)) : Type) × Ω))
      ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' Set.Ioi i ×ˢ A) p ↔
    Membership.mem (γ := Set ((↑(Set.singleton (n + 1)) : Type) × Ω)) ∅ p
Tactic: ext p
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
p : (↑(Set.singleton (n + 1)) : Type) × Ω
⊢ Membership.mem (γ := Set ((↑(Set.singleton (n + 1)) : Type) × Ω))
      ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' Set.Ioi i ×ˢ A) p ↔
    Membership.mem (γ := Set ((↑(Set.singleton (n + 1)) : Type) × Ω)) ∅ p
have h : i < (↑p.1 : ℕ) → p.2 ∉ A
Tactic: simp only [Set.mem_preimage, Set.mem_prod, Set.mem_Ioi, Set.mem_empty_iff_false,
          iff_false, not_and]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
p : (↑(Set.singleton (n + 1)) : Type) × Ω
⊢ i < (↑p.1 : ℕ) → p.2 ∉ A
have h : i < n + 1 → p.2 ∉ A
Tactic: rw [p.1.2]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
⊢ MeasurableSet (α := { x : ℕ // x ∈ Set.singleton (n + 1) } × Ω)
    ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' Set.Ioi i ×ˢ A)
have inr : MeasurableSet
  (SProd.sprod (α := Set (↑(Set.singleton (n + 1)) : Type))
    {Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.singleton (n + 1)) (n + 1) sorry} A)
Tactic: rw [(_ : (fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' (Set.Ioi i ×ˢ A)
          = {⟨n + 1, rfl⟩} ×ˢ A)]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
inr :
  MeasurableSet
    (SProd.sprod (α := Set (↑(Set.singleton (n + 1)) : Type))
      {Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.singleton (n + 1)) (n + 1) ⋯} A)
⊢ MeasurableSet (α := { x : ℕ // x ∈ Set.singleton (n + 1) } × Ω)
    ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' Set.Ioi i ×ˢ A)
have rw : (fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' Set.Ioi i ×ˢ A =
  SProd.sprod (α := Set (↑(Set.singleton (n + 1)) : Type))
    {Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.singleton (n + 1)) (n + 1) sorry} A
Tactic: rw [(_ : (fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' (Set.Ioi i ×ˢ A)
          = {⟨n + 1, rfl⟩} ×ˢ A)]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
⊢ (fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' Set.Ioi i ×ˢ A =
    SProd.sprod (α := Set (↑(Set.singleton (n + 1)) : Type))
      {Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.singleton (n + 1)) (n + 1) ⋯} A
have h : ∀ (p : (↑(Set.singleton (n + 1)) : Type) × Ω),
  Membership.mem (γ := Set ((↑(Set.singleton (n + 1)) : Type) × Ω))
      ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' Set.Ioi i ×ˢ A) p ↔
    p ∈
      SProd.sprod (α := Set (↑(Set.singleton (n + 1)) : Type))
        {Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.singleton (n + 1)) (n + 1) sorry} A
Tactic: ext p
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
p : (↑(Set.singleton (n + 1)) : Type) × Ω
⊢ Membership.mem (γ := Set ((↑(Set.singleton (n + 1)) : Type) × Ω))
      ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' Set.Ioi i ×ˢ A) p ↔
    p ∈
      SProd.sprod (α := Set (↑(Set.singleton (n + 1)) : Type))
        {Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.singleton (n + 1)) (n + 1) ⋯} A
have h : p.2 ∈ A → (i < (↑p.1 : ℕ) ↔ p.1 = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.singleton (n + 1)) (n + 1) sorry)
Tactic: simp only [Set.mem_preimage, Set.mem_prod, Set.mem_Ioi, Set.mem_singleton_iff,
          and_congr_left_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
p : (↑(Set.singleton (n + 1)) : Type) × Ω
hp2 : p.2 ∈ A
⊢ i < (↑p.1 : ℕ) ↔ p.1 = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.singleton (n + 1)) (n + 1) ⋯
have h : i < n + 1 ↔ p.1 = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.singleton (n + 1)) (n + 1) sorry
Tactic: rw [p.1.2]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
inst_1 : OrderBot ι
𝓕 : Filtration ι m
m' : MeasurableSpace (ι × Ω)
hm'bot : ∀ (A : Set Ω), MeasurableSet A → MeasurableSet (SProd.sprod (α := Set ι) {⊥} A)
hm' : ∀ (i : ι) (A : Set Ω), MeasurableSet A → MeasurableSet (Set.Ioi i ×ˢ A)
⊢ 𝓕.predictable ≤ m'
have refine : ∀ (t : Set (ι × Ω)),
  Membership.mem (γ := Set (Set (ι × Ω)))
      ({s : Set (ι × Ω) | ∃ (A : Set Ω), MeasurableSet A ∧ s = SProd.sprod (α := Set ι) {⊥} A} ∪
        {s : Set (ι × Ω) | ∃ (i : ι) (A : Set Ω), MeasurableSet A ∧ s = Set.Ioi i ×ˢ A})
      t →
    MeasurableSet t
Tactic: refine MeasurableSpace.generateFrom_le ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : OrderBot ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OpensMeasurableSpace ι
inst_5 : OrderClosedTopology ι
𝓕 : Filtration ι m
i : ι
⊢ Measurable (β := ι × Ω) fun (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ ((↑x.1 : ι), x.2)
have rw : LE.le (α := MeasurableSpace (Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω))
  (MeasurableSpace.comap (fun (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ ((↑x.1 : ι), x.2)) 𝓕.predictable)
  (MeasurableSpace.prod (Subtype.instMeasurableSpace (p := fun (x : ι) ↦ x ∈ Set.Iic i))
    ((↑𝓕 : ι → MeasurableSpace Ω) i))
Tactic: rw [measurable_iff_comap_le]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : OrderBot ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OpensMeasurableSpace ι
inst_5 : OrderClosedTopology ι
𝓕 : Filtration ι m
i : ι
⊢ LE.le (α := MeasurableSpace (Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω))
    (MeasurableSpace.comap (fun (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ ((↑x.1 : ι), x.2)) 𝓕.predictable)
    (MeasurableSpace.prod (Subtype.instMeasurableSpace (p := fun (x : ι) ↦ x ∈ Set.Iic i))
      ((↑𝓕 : ι → MeasurableSpace Ω) i))
have refine_1 : ∀ (A : Set Ω), MeasurableSet A → MeasurableSet (SProd.sprod (α := Set ι) {⊥} A)
Tactic: refine MeasurableSpace.comap_le_iff_le_map.2 <|
    measurableSpace_le_predictable_of_measurableSet ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : OrderBot ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OpensMeasurableSpace ι
inst_5 : OrderClosedTopology ι
𝓕 : Filtration ι m
i : ι
refine_1 : ∀ (A : Set Ω), MeasurableSet A → MeasurableSet (SProd.sprod (α := Set ι) {⊥} A)
⊢ LE.le (α := MeasurableSpace (Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω))
    (MeasurableSpace.comap (fun (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ ((↑x.1 : ι), x.2)) 𝓕.predictable)
    (MeasurableSpace.prod (Subtype.instMeasurableSpace (p := fun (x : ι) ↦ x ∈ Set.Iic i))
      ((↑𝓕 : ι → MeasurableSpace Ω) i))
have refine_2 : ∀ (i_1 : ι) (A : Set Ω), MeasurableSet A → MeasurableSet (Set.Ioi i_1 ×ˢ A)
Tactic: refine MeasurableSpace.comap_le_iff_le_map.2 <|
    measurableSpace_le_predictable_of_measurableSet ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : OrderBot ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OpensMeasurableSpace ι
inst_5 : OrderClosedTopology ι
𝓕 : Filtration ι m
i : ι
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet (SProd.sprod (α := Set ι) {⊥} A)
have refine_1 : MeasurableSet (SProd.sprod (α := Set (↑(Set.Iic i) : Type u_2)) {⊥} A)
Tactic: simp only [MeasurableSpace.map_def,
      (by aesop : (fun (p : Set.Iic i × Ω) ↦ ((p.1 : ι), p.2)) ⁻¹' ({⊥} ×ˢ A) = {⊥} ×ˢ A)]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : OrderBot ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OpensMeasurableSpace ι
inst_5 : OrderClosedTopology ι
𝓕 : Filtration ι m
i j : ι
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet (Set.Ioi j ×ˢ A)
have refine_2 : MeasurableSet (α := Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω)
  ((fun (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ ((↑x.1 : ι), x.2)) ⁻¹' Set.Ioi j ×ˢ A)
Tactic: simp only [MeasurableSpace.map_def]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : OrderBot ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OpensMeasurableSpace ι
inst_5 : OrderClosedTopology ι
𝓕 : Filtration ι m
i j : ι
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet (α := Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω)
    ((fun (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ ((↑x.1 : ι), x.2)) ⁻¹' Set.Ioi j ×ˢ A)
have refine_2 : ∀ (hji : j ≤ i),
  MeasurableSet (α := Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω)
    ((fun (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ ((↑x.1 : ι), x.2)) ⁻¹' Set.Ioi j ×ˢ A)
Tactic: obtain hji | hij := le_total j i
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : OrderBot ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OpensMeasurableSpace ι
inst_5 : OrderClosedTopology ι
𝓕 : Filtration ι m
i j : ι
A : Set Ω
hA : MeasurableSet A
refine_2 :
  ∀ (hji : j ≤ i),
    MeasurableSet (α := Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω)
      ((fun (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ ((↑x.1 : ι), x.2)) ⁻¹' Set.Ioi j ×ˢ A)
⊢ MeasurableSet (α := Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω)
    ((fun (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ ((↑x.1 : ι), x.2)) ⁻¹' Set.Ioi j ×ˢ A)
have refine_2₁ : ∀ (hij : i ≤ j),
  MeasurableSet (α := Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω)
    ((fun (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ ((↑x.1 : ι), x.2)) ⁻¹' Set.Ioi j ×ˢ A)
Tactic: obtain hji | hij := le_total j i
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : OrderBot ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OpensMeasurableSpace ι
inst_5 : OrderClosedTopology ι
𝓕 : Filtration ι m
i j : ι
A : Set Ω
hA : MeasurableSet A
hji : j ≤ i
⊢ MeasurableSet (α := Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω)
    ((fun (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ ((↑x.1 : ι), x.2)) ⁻¹' Set.Ioi j ×ˢ A)
have refine_2 : MeasurableSet
  (SProd.sprod (α := Set { x : ι // x ∈ Set.Iic i }) (Subtype.val (p := fun (x : ι) ↦ x ∈ Set.Iic i) ⁻¹' Set.Ioc j i) A)
Tactic: rw [(by grind : (fun (p : Set.Iic i × Ω) ↦ ((p.1 : ι), p.2)) ⁻¹' Set.Ioi j ×ˢ A
        = (Subtype.val ⁻¹' (Set.Ioc j i)) ×ˢ A)]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
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)
⊢ StronglyMeasurable (β := E) fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2
have refine_1 : ∀ (m_1 : ℕ) (x : E), MeasurableSet (X m_1 ⁻¹' {x})
Tactic: refine ⟨fun m ↦ SimpleFunc.mk (X m) ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
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)
refine_1 : ∀ (m_1 : ℕ) (x : E), MeasurableSet (X m_1 ⁻¹' {x})
⊢ StronglyMeasurable (β := E) fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2
have refine_2 : ∀ (m : ℕ), (Set.range (X m)).Finite
Tactic: refine ⟨fun m ↦ SimpleFunc.mk (X m) ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
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)
refine_1 : ∀ (m_1 : ℕ) (x : E), MeasurableSet (X m_1 ⁻¹' {x})
refine_2 : ∀ (m : ℕ), (Set.range (X m)).Finite
⊢ StronglyMeasurable (β := E) fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2
have refine_3 : ∀ (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' := sorry, finite_range' := sorry } :
                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: refine ⟨fun m ↦ SimpleFunc.mk (X 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𝓕 : 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))
have refine_1 : ∀ (m_1 : ℕ) (x : E), MeasurableSet (X m_1 ⁻¹' {x})
Tactic: refine ⟨(fun m ↦ SimpleFunc.mk (X m) ?_ ?_), (fun ω ↦ h𝓕.tendsto_approx ⟨(n + 1), ω⟩)⟩