awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
⊢ MeasurableSet
    (SProd.sprod (α := Set (↑(Set.singleton (n + 1)) : Type))
      {Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.singleton (n + 1)) (n + 1) ⋯} A)

Tactic:
MeasurableSet.prod (MeasurableSet.of_subtype_image trivial) (𝓕.mono hin _ hA)

Premises used: trivial, MeasurableSet.prod, MeasureTheory.Filtration.mono, MeasurableSet.of_subtype_image
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
⊢ MeasurableSet
    (SProd.sprod (α := Set (↑(Set.singleton (n + 1)) : Type))
      {Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.singleton (n + 1)) (n + 1) ⋯} A)

Tactic:
exact MeasurableSet.prod (MeasurableSet.of_subtype_image trivial) (𝓕.mono hin _ hA)
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
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) ⋯} A
⊢ (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

Tactic:
ext p
-- Module: Mathlib.Probability.Process.Predictable
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) × Ω
h : p.2 ∈ A → (i < (↑p.1 : ℕ) ↔ p.1 = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.singleton (n + 1)) (n + 1) ⋯)
⊢ 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

Tactic:
simp only [Set.mem_preimage, Set.mem_prod, Set.mem_Ioi, Set.mem_singleton_iff,
          and_congr_left_iff]

Premises used: Set.mem_Ioi, Set.mem_prod, Set.mem_singleton_iff, and_congr_left_iff, Set.mem_preimage
-- Module: Mathlib.Probability.Process.Predictable
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
h : i < n + 1 ↔ p.1 = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.singleton (n + 1)) (n + 1) ⋯
⊢ i < (↑p.1 : ℕ) ↔ p.1 = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.singleton (n + 1)) (n + 1) ⋯

Tactic:
rw [p.1.2]

Premises used: Prod.fst, Subtype.property
-- Module: Mathlib.Probability.Process.Predictable
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
h : i < n + 1
⊢ p.1 = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.singleton (n + 1)) (n + 1) ⋯

Tactic:
aesop
-- Module: Mathlib.Probability.Process.Predictable
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 < n + 1 ↔ p.1 = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.singleton (n + 1)) (n + 1) ⋯

Tactic:
exact ⟨fun _ ↦ by aesop, fun _ ↦ lt_add_one_iff.2 hin⟩
-- Module: Mathlib.Probability.Process.Predictable
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'

Tactic:
MeasurableSpace.generateFrom_le ?_

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.Probability.Process.Predictable
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)
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
⊢ 𝓕.predictable ≤ m'

Tactic:
refine MeasurableSpace.generateFrom_le ?_

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.Probability.Process.Predictable
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)
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet (SProd.sprod (α := Set ι) {⊥} A)

Tactic:
hm'bot A hA
-- Module: Mathlib.Probability.Process.Predictable
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)
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet (SProd.sprod (α := Set ι) {⊥} A)

Tactic:
exact hm'bot A hA
-- Module: Mathlib.Probability.Process.Predictable
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)
i : ι
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet (Set.Ioi i ×ˢ A)

Tactic:
hm' i A hA
-- Module: Mathlib.Probability.Process.Predictable
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)
i : ι
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet (Set.Ioi i ×ˢ A)

Tactic:
exact hm' i A hA
-- Module: Mathlib.Probability.Process.Predictable
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 : ι
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))
⊢ Measurable (β := ι × Ω) fun (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ ((↑x.1 : ι), x.2)

Tactic:
rw [measurable_iff_comap_le]

Premises used: measurable_iff_comap_le
-- Module: Mathlib.Probability.Process.Predictable
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))

Tactic:
MeasurableSpace.comap_le_iff_le_map.2 <|
    measurableSpace_le_predictable_of_measurableSet ?_ ?_

Premises used: Iff.mpr, MeasureTheory.measurableSpace_le_predictable_of_measurableSet, MeasurableSpace.comap_le_iff_le_map
-- Module: Mathlib.Probability.Process.Predictable
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)
refine_2 : ∀ (i_1 : ι) (A : Set Ω), MeasurableSet A → MeasurableSet (Set.Ioi i_1 ×ˢ 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))

Tactic:
refine MeasurableSpace.comap_le_iff_le_map.2 <|
    measurableSpace_le_predictable_of_measurableSet ?_ ?_

Premises used: Iff.mpr, MeasureTheory.measurableSpace_le_predictable_of_measurableSet, MeasurableSpace.comap_le_iff_le_map
-- Module: Mathlib.Probability.Process.Predictable
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
⊢ (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ ((↑p.1 : ι), p.2)) ⁻¹' SProd.sprod (α := Set ι) {⊥} A =
    SProd.sprod (α := Set (↑(Set.Iic i) : Type u_2)) {⊥} A

Tactic:
aesop
-- Module: Mathlib.Probability.Process.Predictable
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
refine_1 : MeasurableSet (SProd.sprod (α := Set (↑(Set.Iic i) : Type u_2)) {⊥} A)
⊢ MeasurableSet (SProd.sprod (α := Set ι) {⊥} A)

Tactic:
simp only [MeasurableSpace.map_def,
      (by aesop : (fun (p : Set.Iic i × Ω) ↦ ((p.1 : ι), p.2)) ⁻¹' ({⊥} ×ˢ A) = {⊥} ×ˢ A)]

Premises used: MeasurableSpace.map_def
-- Module: Mathlib.Probability.Process.Predictable
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 (↑(Set.Iic i) : Type u_2)) {⊥} A)

Tactic:
(measurableSet_singleton _).prod <| 𝓕.mono bot_le _ hA

Premises used: MeasurableSingletonClass.measurableSet_singleton, MeasurableSet.prod, MeasureTheory.Filtration.mono, bot_le
-- Module: Mathlib.Probability.Process.Predictable
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 (↑(Set.Iic i) : Type u_2)) {⊥} A)

Tactic:
exact (measurableSet_singleton _).prod <| 𝓕.mono bot_le _ hA

Premises used: MeasurableSingletonClass.measurableSet_singleton, MeasurableSet.prod, MeasureTheory.Filtration.mono, bot_le
-- Module: Mathlib.Probability.Process.Predictable
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 :
  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 (Set.Ioi j ×ˢ A)

Tactic:
simp only [MeasurableSpace.map_def]

Premises used: MeasurableSpace.map_def
-- Module: Mathlib.Probability.Process.Predictable
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)
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)
⊢ 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

Premises used: le_total
-- Module: Mathlib.Probability.Process.Predictable
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
⊢ (fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ ((↑p.1 : ι), p.2)) ⁻¹' Set.Ioi j ×ˢ A =
    SProd.sprod (α := Set { x : ι // x ∈ Set.Iic i }) (Subtype.val (p := fun (x : ι) ↦ x ∈ Set.Iic i) ⁻¹' Set.Ioc j i) A

Tactic:
grind
-- Module: Mathlib.Probability.Process.Predictable
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
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)
⊢ 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:
rw [(by grind : (fun (p : Set.Iic i × Ω) ↦ ((p.1 : ι), p.2)) ⁻¹' Set.Ioi j ×ˢ A
        = (Subtype.val ⁻¹' (Set.Ioc j i)) ×ˢ A)]
-- Module: Mathlib.Probability.Process.Predictable
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
    (SProd.sprod (α := Set { x : ι // x ∈ Set.Iic i }) (Subtype.val (p := fun (x : ι) ↦ x ∈ Set.Iic i) ⁻¹' Set.Ioc j i)
      A)

Tactic:
(measurable_subtype_coe measurableSet_Ioc).prod (𝓕.mono hji _ hA)

Premises used: measurable_subtype_coe, MeasurableSet.prod, MeasureTheory.Filtration.mono, measurableSet_Ioc
-- Module: Mathlib.Probability.Process.Predictable
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
    (SProd.sprod (α := Set { x : ι // x ∈ Set.Iic i }) (Subtype.val (p := fun (x : ι) ↦ x ∈ Set.Iic i) ⁻¹' Set.Ioc j i)
      A)

Tactic:
exact (measurable_subtype_coe measurableSet_Ioc).prod (𝓕.mono hji _ hA)

Premises used: measurable_subtype_coe, MeasurableSet.prod, MeasureTheory.Filtration.mono, measurableSet_Ioc
-- Module: Mathlib.Probability.Process.Predictable
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
hij : i ≤ j
⊢ Eq (α := Set (Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω))
    ((fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ ((↑p.1 : ι), p.2)) ⁻¹' Set.Ioi j ×ˢ A) ∅

Tactic:
grind
-- 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)
⊢ StronglyMeasurable (β := E) fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2

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

Premises used: MeasureTheory.SimpleFunc.mk, Exists.intro, MeasureTheory.StronglyMeasurable
-- 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)
refine_1 : ∀ (m_1 : ℕ) (x : E), MeasurableSet (X m_1 ⁻¹' {x})
refine_2 : ∀ (m : ℕ), (Set.range (X m)).Finite
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' := ⋯, 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))
⊢ StronglyMeasurable (β := E) fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2

Tactic:
refine ⟨fun m ↦ SimpleFunc.mk (X m) ?_ ?_, ?_⟩
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
ι : Type u_2
m_1 : 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_1
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 : ℕ) (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
    (StronglyMeasurable.approx h𝓕 m : (a : ι × Ω) → E) ((↑x.1 : ι), x.2)
m : ℕ
⊢ ∀ (x : E), MeasurableSet (X m ⁻¹' {x})

Tactic:
fun e ↦ measurable_inclusion_predictable <| (h𝓕.approx m).measurableSet_fiber e

Premises used: MeasureTheory.StronglyMeasurable.approx, Set.Mem, setOf, Set.preimage, Set.singleton, MeasureTheory.SimpleFunc.measurableSet_fiber, MeasureTheory.measurable_inclusion_predictable
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
ι : Type u_2
m_1 : 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_1
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 : ℕ) (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
    (StronglyMeasurable.approx h𝓕 m : (a : ι × Ω) → E) ((↑x.1 : ι), x.2)
m : ℕ
⊢ ∀ (x : E), MeasurableSet (X m ⁻¹' {x})

Tactic:
exact fun e ↦ measurable_inclusion_predictable <| (h𝓕.approx m).measurableSet_fiber e

Premises used: MeasureTheory.StronglyMeasurable.approx, MeasureTheory.SimpleFunc.measurableSet_fiber, MeasureTheory.measurable_inclusion_predictable
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
ι : Type u_2
m_1 : 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_1
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 : ℕ) (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
    (StronglyMeasurable.approx h𝓕 m : (a : ι × Ω) → E) ((↑x.1 : ι), x.2)
m : ℕ
⊢ Set.range (X m) ⊆ Set.range (ι := ι × Ω) (⇑(StronglyMeasurable.approx h𝓕 m) : (a : ι × Ω) → E)

Tactic:
grind
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
ι : Type u_2
m_1 : 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_1
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 : ℕ) (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦
    (StronglyMeasurable.approx h𝓕 m : (a : ι × Ω) → E) ((↑x.1 : ι), x.2)
m : ℕ
⊢ (Set.range (X m)).Finite

Tactic:
exact Set.Finite.subset (h𝓕.approx m).finite_range (by grind)

Premises used: MeasureTheory.StronglyMeasurable.approx, MeasureTheory.SimpleFunc.finite_range, Set.Finite.subset