awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
m_1 : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace (↑(memPartition t n) : Type u_1)
s : Set α
hs : s ∈ memPartition t n
suffices : MeasurableSet.{u_1} (α := α) {x : α | memPartitionSet t n x = s}
⊢ MeasurableSet (α := α)
    (Set.preimage (β := (↑(memPartition t n) : Type u_1))
      (fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ memPartition t n) (memPartitionSet t n a) ⋯)
      {Subtype.mk (p := fun (x : Set α) ↦ x ∈ memPartition t n) s hs})

Tactic:
suffices MeasurableSet[partitionFiltration ht n] {x | memPartitionSet t n x = s} by
    convert! this
    ext x
    simp
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
m_1 : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace (↑(memPartition t n) : Type u_1)
s : Set α
hs : s ∈ memPartition t n
simp_rw : MeasurableSet.{u_1} (α := α) {x : α | x ∈ s}
⊢ MeasurableSet.{u_1} (α := α) {x : α | memPartitionSet t n x = s}

Tactic:
simp_rw [memPartitionSet_eq_iff _ hs]

Premises used: memPartitionSet_eq_iff
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
m_1 : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace (↑(memPartition t n) : Type u_1)
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet.{u_1} (α := α) {x : α | x ∈ s}

Tactic:
measurableSet_partitionFiltration_of_mem _ _ hs

Premises used: ProbabilityTheory.measurableSet_partitionFiltration_of_mem
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
m_1 : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace (↑(memPartition t n) : Type u_1)
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet.{u_1} (α := α) {x : α | x ∈ s}

Tactic:
exact measurableSet_partitionFiltration_of_mem _ _ hs

Premises used: ProbabilityTheory.measurableSet_partitionFiltration_of_mem
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
⊢ Measurable (memPartitionSet t n)

Tactic:
measurable_subtype_coe.comp (measurable_memPartitionSet_subtype ht _ _)

Premises used: measurable_subtype_coe, Measurable.comp, ProbabilityTheory.measurable_memPartitionSet_subtype
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
⊢ Measurable (memPartitionSet t n)

Tactic:
(measurable_partitionFiltration_memPartitionSet ht n).mono ((partitionFiltration ht).le n) le_rfl

Premises used: le_rfl, MeasureTheory.Filtration.le, ProbabilityTheory.partitionFiltration, ProbabilityTheory.measurable_partitionFiltration_memPartitionSet, Measurable.mono
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
rw : ⨆ (i : ℕ), generateFrom (memPartition t i)
| generateFrom (Set.range t)

Tactic:
rw [← generateFrom_iUnion_memPartition t, ← iSup_generateFrom]

Premises used: MeasurableSpace.generateFrom_iUnion_memPartition, MeasurableSpace.iSup_generateFrom
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
conv_rhs :
  Eq.{u_1 + 1} (α := MeasurableSpace α) (⨆ (n : ℕ), (↑(partitionFiltration (t := t) ht) : ℕ → MeasurableSpace α) n)
    (⨆ (i : ℕ), generateFrom (memPartition t i))
⊢ ⨆ (n : ℕ), (↑(partitionFiltration (t := t) ht) : ℕ → MeasurableSpace α) n = generateFrom (Set.range t)

Tactic:
conv_rhs => rw [← generateFrom_iUnion_memPartition t, ← iSup_generateFrom]

Premises used: MeasurableSpace.generateFrom_iUnion_memPartition, MeasurableSpace.iSup_generateFrom
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ Eq.{u_1 + 1} (α := MeasurableSpace α) (⨆ (n : ℕ), (↑(partitionFiltration (t := t) ht) : ℕ → MeasurableSpace α) n)
    (⨆ (i : ℕ), generateFrom (memPartition t i))

Tactic:
rfl
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
ht_range rw : generateFrom (Set.range t) = m
rw₁ rw₂ : m = m
⊢ ⨆ (n : ℕ), (↑(partitionFiltration (t := t) ht) : ℕ → MeasurableSpace α) n = m

Tactic:
rw [iSup_partitionFiltration_eq_generateFrom_range ht, ht_range]

Premises used: ProbabilityTheory.iSup_partitionFiltration_eq_generateFrom_range
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
n : ℕ
s : Set α
hs : s ∈ countablePartition α n
⊢ MeasurableSet s

Tactic:
measurableSet_generateFrom hs

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
n : ℕ
t : α
⊢ MeasurableSet (countablePartitionSet n t)

Tactic:
measurableSet_countableFiltration_of_mem n (countablePartitionSet_mem n t)

Premises used: MeasurableSpace.countablePartitionSet_mem, ProbabilityTheory.measurableSet_countableFiltration_of_mem
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
n : ℕ
m : MeasurableSpace (↑(countablePartition α n) : Type u_1)
⊢ Measurable (β := (↑(countablePartition α n) : Type u_1)) fun (a : α) ↦
    Subtype.mk (p := fun (x : Set α) ↦ x ∈ countablePartition α n) (countablePartitionSet n a) ⋯

Tactic:
measurable_memPartitionSet_subtype
    (measurableSet_enumerateCountable_countableGeneratingSet (α := α)) n m

Premises used: Set.Mem, MeasurableSpace.countablePartitionSet, MeasurableSpace.measurableSet_enumerateCountable_countableGeneratingSet, ProbabilityTheory.measurable_memPartitionSet_subtype, MeasurableSpace.countablePartition
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_2
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
n : ℕ
⊢ Measurable.{u_2, u_2} (α := α) (countablePartitionSet n)

Tactic:
measurable_subtype_coe.comp (measurable_countablePartitionSet_subtype _ _)

Premises used: measurable_subtype_coe, Measurable.comp, MeasurableSpace.countablePartitionSet, ProbabilityTheory.measurable_countablePartitionSet_subtype
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_2
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
n : ℕ
⊢ Measurable.{u_2, u_2} (α := α) (countablePartitionSet n)

Tactic:
(measurable_countableFiltration_countablePartitionSet α n).mono ((countableFiltration α).le n)
    le_rfl

Premises used: le_rfl, ProbabilityTheory.countableFiltration, MeasureTheory.Filtration.le, Measurable.mono, ProbabilityTheory.measurable_countableFiltration_countablePartitionSet
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_2
m : MeasurableSpace α
inst : CountablyGenerated α
rw : ⨆ (i : ℕ), generateFrom (countablePartition α i)
| m

Tactic:
rw [← generateFrom_iUnion_countablePartition α, ← iSup_generateFrom]

Premises used: MeasurableSpace.generateFrom_iUnion_countablePartition, MeasurableSpace.iSup_generateFrom
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_2
m : MeasurableSpace α
inst : CountablyGenerated α
conv_rhs :
  Eq.{u_2 + 1} (α := MeasurableSpace α) (⨆ (n : ℕ), (↑(countableFiltration α) : ℕ → MeasurableSpace α) n)
    (⨆ (i : ℕ), generateFrom (countablePartition α i))
⊢ ⨆ (n : ℕ), (↑(countableFiltration α) : ℕ → MeasurableSpace α) n = m

Tactic:
conv_rhs => rw [← generateFrom_iUnion_countablePartition α, ← iSup_generateFrom]

Premises used: MeasurableSpace.generateFrom_iUnion_countablePartition, MeasurableSpace.iSup_generateFrom
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_2
m : MeasurableSpace α
inst : CountablyGenerated α
⊢ Eq.{u_2 + 1} (α := MeasurableSpace α) (⨆ (n : ℕ), (↑(countableFiltration α) : ℕ → MeasurableSpace α) n)
    (⨆ (i : ℕ), generateFrom (countablePartition α i))

Tactic:
rfl
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : OrderBot ι
𝓕 : Filtration ι m
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet (SProd.sprod (α := Set ι) {⊥} s)

Tactic:
MeasurableSpace.measurableSet_generateFrom <| Or.inl ⟨s, hs, rfl⟩

Premises used: MeasurableSpace.measurableSet_generateFrom, And.intro, Exists.intro, Or.inl, rfl
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : OrderBot ι
𝓕 : Filtration ι m
i : ι
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet (Set.Ioi i ×ˢ s)

Tactic:
MeasurableSpace.measurableSet_generateFrom <| Or.inr ⟨i, s, hs, rfl⟩

Premises used: MeasurableSpace.measurableSet_generateFrom, And.intro, Exists.intro, Or.inr, rfl
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
inl : ∀ (hij : j ≤ i), MeasurableSet (Set.Ioc i j ×ˢ s)
inr : ∀ (hij : i ≤ j), MeasurableSet (Set.Ioc i j ×ˢ s)
⊢ MeasurableSet (Set.Ioc i j ×ˢ s)

Tactic:
obtain hij | 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 ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
hij : j ≤ i
⊢ MeasurableSet (Set.Ioc i j ×ˢ s)

Tactic:
simp [hij]
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
hij : i ≤ j
⊢ (Set.Ioi i \ Set.Ioi j) ×ˢ s = Set.Ioi i ×ˢ (s \ s) ∪ (Set.Ioi i \ Set.Ioi j) ×ˢ s

Tactic:
simp
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
hij : i ≤ j
inr : MeasurableSet (Set.Ioi i ×ˢ s \ Set.Ioi j ×ˢ s)
⊢ MeasurableSet (Set.Ioc i j ×ˢ s)

Tactic:
rw [← Set.Ioi_diff_Ioi, (by simp : (Set.Ioi i \ Set.Ioi j) ×ˢ s
      = Set.Ioi i ×ˢ (s \ s) ∪ (Set.Ioi i \ Set.Ioi j) ×ˢ s), ← Set.prod_diff_prod]

Premises used: Set.prod_diff_prod, Set.Ioi_diff_Ioi
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
hij : i ≤ j
⊢ MeasurableSet (Set.Ioi i ×ˢ s \ Set.Ioi j ×ˢ s)

Tactic:
(measurableSet_predictable_Ioi_prod hs).diff
      (measurableSet_predictable_Ioi_prod <| 𝓕.mono hij _ hs)

Premises used: MeasurableSet.diff, MeasureTheory.measurableSet_predictable_Ioi_prod, MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
hij : i ≤ j
⊢ MeasurableSet (Set.Ioi i ×ˢ s \ Set.Ioi j ×ˢ s)

Tactic:
exact (measurableSet_predictable_Ioi_prod hs).diff
      (measurableSet_predictable_Ioi_prod <| 𝓕.mono hij _ hs)

Premises used: MeasurableSet.diff, MeasureTheory.measurableSet_predictable_Ioi_prod, MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
n : ℕ
s : Set Ω
hs : MeasurableSet s
rw : MeasurableSet (Set.Ioc n (n + 1) ×ˢ s)
rw₁ : {n + 1} = Set.Ioc n (n + 1)
⊢ MeasurableSet (SProd.sprod (α := Set ℕ) {n + 1} s)

Tactic:
rw [(_ : {n + 1} = Set.Ioc n (n + 1))]
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
n : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet (Set.Ioc n (n + 1) ×ˢ s)

Tactic:
measurableSet_predictable_Ioc_prod _ _ hs

Premises used: MeasureTheory.measurableSet_predictable_Ioc_prod
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
n : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet (Set.Ioc n (n + 1) ×ˢ s)

Tactic:
exact measurableSet_predictable_Ioc_prod _ _ hs

Premises used: MeasureTheory.measurableSet_predictable_Ioc_prod
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
n : ℕ
s : Set Ω
hs : MeasurableSet s
h : ∀ (m : ℕ), Membership.mem (γ := Set ℕ) {n + 1} m ↔ m ∈ Set.Ioc n (n + 1)
⊢ {n + 1} = Set.Ioc n (n + 1)

Tactic:
ext m
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
m_1 : MeasurableSpace Ω
𝓕 : Filtration ℕ m_1
n : ℕ
s : Set Ω
hs : MeasurableSet s
m : ℕ
⊢ m = n + 1 ↔ n < m ∧ m ≤ n + 1

Tactic:
lia
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
⊢ Eq (α := Set Ω) {ω : Ω | (n + 1, ω) ∈ s}
    (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)

Tactic:
aesop
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
rw :
  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)
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (n + 1, ω) ∈ 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))]
-- Module: Mathlib.Probability.Process.Predictable
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)

Tactic:
measurableSet_preimage (mβ := Subtype.instMeasurableSpace.prod (𝓕 n))
    measurable_prodMk_left <| measurableSet_preimage ?_ hs

Premises used: measurableSet_preimage, measurable_prodMk_left
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
refine : Measurable (β := ℕ × Ω) fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)
⊢ 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)

Tactic:
refine measurableSet_preimage (mβ := Subtype.instMeasurableSpace.prod (𝓕 n))
    measurable_prodMk_left <| measurableSet_preimage ?_ hs

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

Tactic:
MeasurableSpace.generateFrom_le ?_

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
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 ≤
    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))

Tactic:
refine MeasurableSpace.generateFrom_le ?_

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.Probability.Process.Predictable
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) } × Ω) ∅
rw :
  Eq (α := Set ((↑(Set.singleton (n + 1)) : Type) × Ω))
    ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' SProd.sprod (α := Set ℕ) {⊥} A) ∅
⊢ MeasurableSet (SProd.sprod (α := Set ℕ) {⊥} A)

Tactic:
rw [MeasurableSpace.map_def,
      (_ : (fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' ({⊥} ×ˢ A) = ∅)]

Premises used: MeasurableSpace.map_def
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet.{u_1} (α := { x : ℕ // x ∈ Set.singleton (n + 1) } × Ω) ∅

Tactic:
simp
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
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
⊢ Eq (α := Set ((↑(Set.singleton (n + 1)) : Type) × Ω))
    ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' SProd.sprod (α := Set ℕ) {⊥} A) ∅

Tactic:
ext p
-- Module: Mathlib.Probability.Process.Predictable
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) × Ω
h : (↑p.1 : ℕ) = 0 → p.2 ∉ A
⊢ 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:
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]

Premises used: iff_false, Set.mem_prod, Set.mem_singleton_iff, Set.mem_empty_iff_false, not_and, Nat.bot_eq_zero, Set.mem_preimage
-- Module: Mathlib.Probability.Process.Predictable
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) × Ω
⊢ (↑p.1 : ℕ) = 0 → p.2 ∉ A

Tactic:
fun hp1 ↦ False.elim <| Nat.succ_ne_zero n (hp1 ▸ p.1.2.symm)

Premises used: False.elim, Eq.rec, Prod.fst, Nat.succ_ne_zero, Eq.symm, Subtype.property
-- Module: Mathlib.Probability.Process.Predictable
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) × Ω
⊢ (↑p.1 : ℕ) = 0 → p.2 ∉ A

Tactic:
exact fun hp1 ↦ False.elim <| Nat.succ_ne_zero n (hp1 ▸ p.1.2.symm)
-- 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
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)
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)
⊢ 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

Premises used: lt_or_ge
-- 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
hni : n < i
inr : MeasurableSet.{u_1} (α := { x : ℕ // x ∈ Set.singleton (n + 1) } × Ω) ∅
rw :
  Eq (α := Set ((↑(Set.singleton (n + 1)) : Type) × Ω))
    ((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)

Tactic:
rw [(_ : (fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' (Set.Ioi i ×ˢ A) = ∅)]
-- 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
hni : n < i
⊢ MeasurableSet.{u_1} (α := { x : ℕ // x ∈ Set.singleton (n + 1) } × Ω) ∅

Tactic:
simp
-- 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
hni : n < i
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
⊢ Eq (α := Set ((↑(Set.singleton (n + 1)) : Type) × Ω))
    ((fun (p : (↑(Set.singleton (n + 1)) : Type) × Ω) ↦ ((↑p.1 : ℕ), p.2)) ⁻¹' Set.Ioi i ×ˢ 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
hni : n < i
p : (↑(Set.singleton (n + 1)) : Type) × Ω
h : i < (↑p.1 : ℕ) → p.2 ∉ A
⊢ 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:
simp only [Set.mem_preimage, Set.mem_prod, Set.mem_Ioi, Set.mem_empty_iff_false,
          iff_false, not_and]

Premises used: iff_false, Set.mem_Ioi, Set.mem_prod, Set.mem_empty_iff_false, not_and, 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
hni : n < i
p : (↑(Set.singleton (n + 1)) : Type) × Ω
h : i < n + 1 → p.2 ∉ A
⊢ i < (↑p.1 : ℕ) → p.2 ∉ A

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
hni : n < i
p : (↑(Set.singleton (n + 1)) : Type) × Ω
⊢ i < n + 1 → p.2 ∉ A

Tactic:
grind
-- 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
inr :
  MeasurableSet
    (SProd.sprod (α := Set (↑(Set.singleton (n + 1)) : Type))
      {Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.singleton (n + 1)) (n + 1) ⋯} A)
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) ⋯} A
⊢ MeasurableSet (α := { x : ℕ // x ∈ Set.singleton (n + 1) } × Ω)
    ((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)
          = {⟨n + 1, rfl⟩} ×ˢ A)]