awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst_1 : DecidablePred fun (x : Ω) ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), (↑i : WithTop ι) ≤ τ ω
hη : ∀ (ω : Ω), (↑i : WithTop ι) ≤ η ω
hs : MeasurableSet s
n : ι
this :
  {ω : Ω | s.piecewise (β := fun (i : Ω) ↦ WithTop ι) τ η ω ≤ (↑n : WithTop ι)} =
    s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}
rw : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | s.piecewise (β := fun (a : Ω) ↦ WithTop ι) τ η ω ≤ (↑n : WithTop ι)}

Tactic:
rw [this]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst_1 : DecidablePred fun (x : Ω) ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), (↑i : WithTop ι) ≤ τ ω
hη : ∀ (ω : Ω), (↑i : WithTop ι) ≤ η ω
hs : MeasurableSet s
n : ι
this :
  {ω : Ω | s.piecewise (β := fun (i : Ω) ↦ WithTop ι) τ η ω ≤ (↑n : WithTop ι)} =
    s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}
pos : ∀ (hin : i ≤ n), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)})
neg : ∀ (hin : ¬i ≤ n), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)})
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)})

Tactic:
by_cases hin : i ≤ n
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst_1 : DecidablePred fun (x : Ω) ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), (↑i : WithTop ι) ≤ τ ω
hη : ∀ (ω : Ω), (↑i : WithTop ι) ≤ η ω
hs : MeasurableSet s
n : ι
this :
  {ω : Ω | s.piecewise (β := fun (i : Ω) ↦ WithTop ι) τ η ω ≤ (↑n : WithTop ι)} =
    s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}
hin : i ≤ n
⊢ MeasurableSet s

Tactic:
have hs_n : MeasurableSet[𝒢 n] s := 𝒢.mono hin _ hs
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst_1 : DecidablePred fun (x : Ω) ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), (↑i : WithTop ι) ≤ τ ω
hη : ∀ (ω : Ω), (↑i : WithTop ι) ≤ η ω
hs : MeasurableSet s
n : ι
this :
  {ω : Ω | s.piecewise (β := fun (i : Ω) ↦ WithTop ι) τ η ω ≤ (↑n : WithTop ι)} =
    s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}
hin : i ≤ n
hs_n : MeasurableSet s
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)})

Tactic:
(hs_n.inter (hτ_st n)).union (hs_n.compl.inter (hη_st n))

Premises used: MeasurableSet.compl, MeasurableSet.union, MeasurableSet.inter
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst_1 : DecidablePred fun (x : Ω) ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), (↑i : WithTop ι) ≤ τ ω
hη : ∀ (ω : Ω), (↑i : WithTop ι) ≤ η ω
hs : MeasurableSet s
n : ι
this :
  {ω : Ω | s.piecewise (β := fun (i : Ω) ↦ WithTop ι) τ η ω ≤ (↑n : WithTop ι)} =
    s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}
hin : i ≤ n
hs_n : MeasurableSet s
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)})

Tactic:
exact (hs_n.inter (hτ_st n)).union (hs_n.compl.inter (hη_st n))

Premises used: MeasurableSet.compl, MeasurableSet.union, MeasurableSet.inter
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst_1 : DecidablePred fun (x : Ω) ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), (↑i : WithTop ι) ≤ τ ω
hη : ∀ (ω : Ω), (↑i : WithTop ι) ≤ η ω
hs : MeasurableSet s
n : ι
this :
  {ω : Ω | s.piecewise (β := fun (i : Ω) ↦ WithTop ι) τ η ω ≤ (↑n : WithTop ι)} =
    s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}
hin : ¬i ≤ n
⊢ ∀ (ω : Ω), ¬τ ω ≤ (↑n : WithTop ι)

Tactic:
have hτn : ∀ ω, ¬τ ω ≤ n := fun ω hτn => hin (mod_cast (hτ ω).trans hτn)
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst_1 : DecidablePred fun (x : Ω) ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), (↑i : WithTop ι) ≤ τ ω
hη : ∀ (ω : Ω), (↑i : WithTop ι) ≤ η ω
hs : MeasurableSet s
n : ι
this :
  {ω : Ω | s.piecewise (β := fun (i : Ω) ↦ WithTop ι) τ η ω ≤ (↑n : WithTop ι)} =
    s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}
hin : ¬i ≤ n
hτn : ∀ (ω : Ω), ¬τ ω ≤ (↑n : WithTop ι)
⊢ ∀ (ω : Ω), ¬η ω ≤ (↑n : WithTop ι)

Tactic:
have hηn : ∀ ω, ¬η ω ≤ n := fun ω hηn => hin (mod_cast (hη ω).trans hηn)
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst_1 : DecidablePred fun (x : Ω) ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), (↑i : WithTop ι) ≤ τ ω
hη : ∀ (ω : Ω), (↑i : WithTop ι) ≤ η ω
hs : MeasurableSet s
n : ι
this :
  {ω : Ω | s.piecewise (β := fun (i : Ω) ↦ WithTop ι) τ η ω ≤ (↑n : WithTop ι)} =
    s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}
hin : ¬i ≤ n
hτn : ∀ (ω : Ω), ¬τ ω ≤ (↑n : WithTop ι)
hηn : ∀ (ω : Ω), ¬η ω ≤ (↑n : WithTop ι)
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)})

Tactic:
simp [hτn, hηn, @MeasurableSet.empty _ _]

Premises used: MeasurableSet.empty
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
𝒢 : Filtration ι m
i j : ι
s : Set Ω
inst_1 : DecidablePred fun (x : Ω) ↦ x ∈ s
hij : i ≤ j
hs : MeasurableSet s
⊢ IsStoppingTime 𝒢
    (s.piecewise (β := fun (a : Ω) ↦ WithTop ι) (fun (x : Ω) ↦ (↑i : WithTop ι)) fun (x : Ω) ↦ (↑j : WithTop ι))

Tactic:
(isStoppingTime_const 𝒢 i).piecewise_of_le (isStoppingTime_const 𝒢 j) (fun _ => le_rfl)
    (fun _ => mod_cast hij) hs

Premises used: le_rfl, WithTop.coe_le_coe._simp_1, cast, MeasureTheory.isStoppingTime_const, Eq.symm, MeasureTheory.IsStoppingTime.piecewise_of_le
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
s : Set Ω
inst : DecidablePred fun (x : Ω) ↦ x ∈ s
ι' : Type u_4
α : Type u_5
inst_1 : Nonempty ι'
i j : ι'
f : ι' → Ω → α
h :
  ∀ (ω : Ω),
    stoppedValue f
        (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) fun (x : Ω) ↦ (↑j : WithTop ι'))
        ω =
      s.piecewise (β := fun (i : Ω) ↦ α) (f i) (f j) ω
⊢ stoppedValue f
      (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) fun (x : Ω) ↦ (↑j : WithTop ι')) =
    s.piecewise (β := fun (i : Ω) ↦ α) (f i) (f j)

Tactic:
ext ω
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
s : Set Ω
inst : DecidablePred fun (x : Ω) ↦ x ∈ s
ι' : Type u_4
α : Type u_5
inst_1 : Nonempty ι'
i j : ι'
f : ι' → Ω → α
ω : Ω
h :
  f
      (untopA
        (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) (fun (x : Ω) ↦ (↑j : WithTop ι'))
          ω))
      ω =
    s.piecewise (β := fun (i : Ω) ↦ α) (f i) (f j) ω
⊢ stoppedValue f
      (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) fun (x : Ω) ↦ (↑j : WithTop ι'))
      ω =
    s.piecewise (β := fun (i : Ω) ↦ α) (f i) (f j) ω

Tactic:
rw [stoppedValue]

Premises used: MeasureTheory.stoppedValue
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
s : Set Ω
inst : DecidablePred fun (x : Ω) ↦ x ∈ s
ι' : Type u_4
α : Type u_5
inst_1 : Nonempty ι'
i j : ι'
f : ι' → Ω → α
ω : Ω
pos :
  ∀ (hx : ω ∈ s),
    f
        (untopA
          (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι'))
            (fun (x : Ω) ↦ (↑j : WithTop ι')) ω))
        ω =
      s.piecewise (β := fun (i : Ω) ↦ α) (f i) (f j) ω
neg :
  ∀ (hx : ω ∉ s),
    f
        (untopA
          (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι'))
            (fun (x : Ω) ↦ (↑j : WithTop ι')) ω))
        ω =
      s.piecewise (β := fun (i : Ω) ↦ α) (f i) (f j) ω
⊢ f
      (untopA
        (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) (fun (x : Ω) ↦ (↑j : WithTop ι'))
          ω))
      ω =
    s.piecewise (β := fun (i : Ω) ↦ α) (f i) (f j) ω

Tactic:
by_cases hx : ω ∈ s
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
s : Set Ω
inst : DecidablePred fun (x : Ω) ↦ x ∈ s
ι' : Type u_4
α : Type u_5
inst_1 : Nonempty ι'
i j : ι'
f : ι' → Ω → α
ω : Ω
hx : ω ∈ s
⊢ f
      (untopA
        (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) (fun (x : Ω) ↦ (↑j : WithTop ι'))
          ω))
      ω =
    s.piecewise (β := fun (i : Ω) ↦ α) (f i) (f j) ω

Tactic:
simp [hx]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
s : Set Ω
inst : DecidablePred fun (x : Ω) ↦ x ∈ s
ι' : Type u_4
α : Type u_5
inst_1 : Nonempty ι'
i j : ι'
f : ι' → Ω → α
ω : Ω
hx : ω ∉ s
⊢ f
      (untopA
        (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) (fun (x : Ω) ↦ (↑j : WithTop ι'))
          ω))
      ω =
    s.piecewise (β := fun (i : Ω) ↦ α) (f i) (f j) ω

Tactic:
simp [hx]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
s : Set Ω
inst : DecidablePred fun (x : Ω) ↦ x ∈ s
ι' : Type u_4
α : Type u_5
inst_1 : AddCommGroup α
inst_2 : Nonempty ι'
i j : ι'
f : ι' → Ω → α
h :
  ∀ (ω : Ω),
    stoppedValue f
        (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) fun (x : Ω) ↦ (↑j : WithTop ι'))
        ω =
      (s.indicator (f i) + sᶜ.indicator (f j)) ω
⊢ stoppedValue f
      (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) fun (x : Ω) ↦ (↑j : WithTop ι')) =
    s.indicator (f i) + sᶜ.indicator (f j)

Tactic:
ext ω
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
s : Set Ω
inst : DecidablePred fun (x : Ω) ↦ x ∈ s
ι' : Type u_4
α : Type u_5
inst_1 : AddCommGroup α
inst_2 : Nonempty ι'
i j : ι'
f : ι' → Ω → α
ω : Ω
h :
  f
      (untopA
        (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) (fun (x : Ω) ↦ (↑j : WithTop ι'))
          ω))
      ω =
    (s.indicator (f i) + sᶜ.indicator (f j)) ω
⊢ stoppedValue f
      (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) fun (x : Ω) ↦ (↑j : WithTop ι'))
      ω =
    (s.indicator (f i) + sᶜ.indicator (f j)) ω

Tactic:
rw [stoppedValue]

Premises used: MeasureTheory.stoppedValue
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
s : Set Ω
inst : DecidablePred fun (x : Ω) ↦ x ∈ s
ι' : Type u_4
α : Type u_5
inst_1 : AddCommGroup α
inst_2 : Nonempty ι'
i j : ι'
f : ι' → Ω → α
ω : Ω
pos :
  ∀ (hx : ω ∈ s),
    f
        (untopA
          (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι'))
            (fun (x : Ω) ↦ (↑j : WithTop ι')) ω))
        ω =
      (s.indicator (f i) + sᶜ.indicator (f j)) ω
neg :
  ∀ (hx : ω ∉ s),
    f
        (untopA
          (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι'))
            (fun (x : Ω) ↦ (↑j : WithTop ι')) ω))
        ω =
      (s.indicator (f i) + sᶜ.indicator (f j)) ω
⊢ f
      (untopA
        (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) (fun (x : Ω) ↦ (↑j : WithTop ι'))
          ω))
      ω =
    (s.indicator (f i) + sᶜ.indicator (f j)) ω

Tactic:
by_cases hx : ω ∈ s
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
s : Set Ω
inst : DecidablePred fun (x : Ω) ↦ x ∈ s
ι' : Type u_4
α : Type u_5
inst_1 : AddCommGroup α
inst_2 : Nonempty ι'
i j : ι'
f : ι' → Ω → α
ω : Ω
hx : ω ∈ s
⊢ f
      (untopA
        (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) (fun (x : Ω) ↦ (↑j : WithTop ι'))
          ω))
      ω =
    (s.indicator (f i) + sᶜ.indicator (f j)) ω

Tactic:
simp [hx]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
s : Set Ω
inst : DecidablePred fun (x : Ω) ↦ x ∈ s
ι' : Type u_4
α : Type u_5
inst_1 : AddCommGroup α
inst_2 : Nonempty ι'
i j : ι'
f : ι' → Ω → α
ω : Ω
hx : ω ∉ s
⊢ f
      (untopA
        (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) (fun (x : Ω) ↦ (↑j : WithTop ι'))
          ω))
      ω =
    (s.indicator (f i) + sᶜ.indicator (f j)) ω

Tactic:
simp [hx]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
inst_4 : SigmaFiniteFiltration μ ℱ
hτ : IsStoppingTime ℱ τ
h_countable : (Set.range τ).Countable
inst_5 : SigmaFinite (μ.trim ⋯)
i : ι
⊢ μ[f | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] μ[f | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
condExp_ae_eq_restrict_of_measurableSpace_eq_on
    (hτ.measurableSpace_le) (ℱ.le i)
    (hτ.measurableSet_eq_of_countable_range' h_countable i) fun t => ?_

Premises used: MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range', MeasureTheory.IsStoppingTime.measurableSpace_le, MeasureTheory.Filtration.le, MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
inst_4 : SigmaFiniteFiltration μ ℱ
hτ : IsStoppingTime ℱ τ
h_countable : (Set.range τ).Countable
inst_5 : SigmaFinite (μ.trim ⋯)
i : ι
refine :
  ∀ (t : Set Ω),
    MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t)
⊢ μ[f | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] μ[f | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
refine condExp_ae_eq_restrict_of_measurableSpace_eq_on
    (hτ.measurableSpace_le) (ℱ.le i)
    (hτ.measurableSet_eq_of_countable_range' h_countable i) fun t => ?_

Premises used: MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range', MeasureTheory.IsStoppingTime.measurableSpace_le, MeasureTheory.Filtration.le, MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
inst_4 : SigmaFiniteFiltration μ ℱ
hτ : IsStoppingTime ℱ τ
h_countable : (Set.range τ).Countable
inst_5 : SigmaFinite (μ.trim ⋯)
i : ι
t : Set Ω
rw : MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)})
rw₁ rw₂ : MeasurableSet (t ∩ {ω : Ω | τ ω = (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)})
⊢ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t)

Tactic:
rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]

Premises used: Set.inter_comm, MeasureTheory.IsStoppingTime.measurableSet_inter_eq_iff
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
inst_4 : Countable ι
inst_5 : SigmaFiniteFiltration μ ℱ
hτ : IsStoppingTime ℱ τ
inst_6 : SigmaFinite (μ.trim ⋯)
i : ι
⊢ μ[f | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] μ[f | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
condExp_stopping_time_ae_eq_restrict_eq_of_countable_range hτ (Set.to_countable _) i

Premises used: MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq_of_countable_range, Set.to_countable
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
hτ : IsStoppingTime ℱ τ
i : ι
inst_4 : SigmaFinite (μ.trim ⋯)
rw : hτ.measurableSpace ⊓ (↑ℱ : ι → MeasurableSpace Ω) i ≤ hτ.measurableSpace
hτ₁ : IsStoppingTime ℱ τ
⊢ ⋯.measurableSpace ≤ hτ.measurableSpace

Tactic:
rw [IsStoppingTime.measurableSpace_min_const]

Premises used: MeasureTheory.IsStoppingTime.measurableSpace_min_const
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
hτ : IsStoppingTime ℱ τ
i : ι
inst_4 : SigmaFinite (μ.trim ⋯)
⊢ hτ.measurableSpace ⊓ (↑ℱ : ι → MeasurableSpace Ω) i ≤ hτ.measurableSpace

Tactic:
inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
hτ : IsStoppingTime ℱ τ
i : ι
inst_4 : SigmaFinite (μ.trim ⋯)
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
have : SigmaFinite (μ.trim hτ.measurableSpace_le) :=
    haveI h_le : (hτ.min_const i).measurableSpace ≤ hτ.measurableSpace := by
      rw [IsStoppingTime.measurableSpace_min_const]
      exact inf_le_left
    sigmaFiniteTrim_mono _ h_le
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
hτ : IsStoppingTime ℱ τ
i : ι
inst_4 : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
⊢ μ[f | ⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ (↑i : WithTop ι)})] μ[f | hτ.measurableSpace]

Tactic:
(condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le
    (hτ.min_const i).measurableSpace_le (hτ.measurableSet_le' i) fun t => ?_).symm

Premises used: MeasureTheory.IsStoppingTime.measurableSpace_le, MeasureTheory.IsStoppingTime.measurableSet_le', MeasureTheory.IsStoppingTime.min_const, Filter.EventuallyEq.symm, MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
hτ : IsStoppingTime ℱ τ
i : ι
inst_4 : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
refine :
  ∀ (t : Set Ω),
    MeasurableSet ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ t)
⊢ μ[f | ⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ (↑i : WithTop ι)})] μ[f | hτ.measurableSpace]

Tactic:
refine (condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le
    (hτ.min_const i).measurableSpace_le (hτ.measurableSet_le' i) fun t => ?_).symm

Premises used: MeasureTheory.IsStoppingTime.measurableSpace_le, MeasureTheory.IsStoppingTime.measurableSet_le', MeasureTheory.IsStoppingTime.min_const, Filter.EventuallyEq.symm, MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
hτ : IsStoppingTime ℱ τ
i : ι
inst_4 : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
t : Set Ω
rw : MeasurableSet (t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
rw₁ rw₂ : MeasurableSet (t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
⊢ MeasurableSet ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ t)

Tactic:
rw [Set.inter_comm _ t, hτ.measurableSet_inter_le_const_iff]

Premises used: MeasureTheory.IsStoppingTime.measurableSet_inter_le_const_iff, Set.inter_comm
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
inst_7 : SigmaFiniteFiltration μ ℱ
hτ : IsStoppingTime ℱ τ
inst_8 : SigmaFinite (μ.trim ⋯)
i : ι
⊢ μ[f | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] μ[f | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le (ℱ.le i)
    (hτ.measurableSet_eq' i) fun t => ?_

Premises used: MeasureTheory.IsStoppingTime.measurableSpace_le, MeasureTheory.Filtration.le, MeasureTheory.IsStoppingTime.measurableSet_eq', MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
inst_7 : SigmaFiniteFiltration μ ℱ
hτ : IsStoppingTime ℱ τ
inst_8 : SigmaFinite (μ.trim ⋯)
i : ι
refine :
  ∀ (t : Set Ω),
    MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t)
⊢ μ[f | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] μ[f | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
refine condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le (ℱ.le i)
    (hτ.measurableSet_eq' i) fun t => ?_

Premises used: MeasureTheory.IsStoppingTime.measurableSpace_le, MeasureTheory.Filtration.le, MeasureTheory.IsStoppingTime.measurableSet_eq', MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : Ω → E
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
inst_7 : SigmaFiniteFiltration μ ℱ
hτ : IsStoppingTime ℱ τ
inst_8 : SigmaFinite (μ.trim ⋯)
i : ι
t : Set Ω
rw : MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)})
rw₁ rw₂ : MeasurableSet (t ∩ {ω : Ω | τ ω = (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)})
⊢ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t)

Tactic:
rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]

Premises used: Set.inter_comm, MeasureTheory.IsStoppingTime.measurableSet_inter_eq_iff