awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
this :
  Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) + Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n)
⊢ stoppedProcess u τ n =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) +
      ∑ i ∈ Finset.range (n + 1), Set.indicator {a : Ω | τ a = (↑i : ℕ∞)} (u i)
have rw : Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) + ∑ i ∈ Finset.range n, Set.indicator {ω : Ω | τ ω = (↑i : ℕ∞)} (u i) =
  Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) +
    ∑ i ∈ Finset.range (n + 1), Set.indicator {a : Ω | τ a = (↑i : ℕ∞)} (u i)
Tactic: rw [stoppedProcess_eq, this, Finset.sum_range_succ_comm, ← add_assoc]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
this :
  Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) + Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n)
rw :
  Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) + ∑ i ∈ Finset.range n, Set.indicator {ω : Ω | τ ω = (↑i : ℕ∞)} (u i) =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) +
      ∑ i ∈ Finset.range (n + 1), Set.indicator {a : Ω | τ a = (↑i : ℕ∞)} (u i)
⊢ stoppedProcess u τ n =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) +
      ∑ i ∈ Finset.range (n + 1), Set.indicator {a : Ω | τ a = (↑i : ℕ∞)} (u i)
have rw₁ : Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) + Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n) +
    ∑ i ∈ Finset.range n, Set.indicator {ω : Ω | τ ω = (↑i : ℕ∞)} (u i) =
  Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) +
    ∑ i ∈ Finset.range (n + 1), Set.indicator {a : Ω | τ a = (↑i : ℕ∞)} (u i)
Tactic: rw [stoppedProcess_eq, this, Finset.sum_range_succ_comm, ← add_assoc]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
this :
  Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) + Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n)
rw :
  Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) + ∑ i ∈ Finset.range n, Set.indicator {ω : Ω | τ ω = (↑i : ℕ∞)} (u i) =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) +
      ∑ i ∈ Finset.range (n + 1), Set.indicator {a : Ω | τ a = (↑i : ℕ∞)} (u i)
rw₁ :
  Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) + Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n) +
      ∑ i ∈ Finset.range n, Set.indicator {ω : Ω | τ ω = (↑i : ℕ∞)} (u i) =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) +
      ∑ i ∈ Finset.range (n + 1), Set.indicator {a : Ω | τ a = (↑i : ℕ∞)} (u i)
⊢ stoppedProcess u τ n =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) +
      ∑ i ∈ Finset.range (n + 1), Set.indicator {a : Ω | τ a = (↑i : ℕ∞)} (u i)
have rw₂ : Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) + Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n) +
    ∑ i ∈ Finset.range n, Set.indicator {ω : Ω | τ ω = (↑i : ℕ∞)} (u i) =
  Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) +
    (Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n) +
      ∑ x ∈ Finset.range n, Set.indicator {a : Ω | τ a = (↑x : ℕ∞)} (u x))
Tactic: rw [stoppedProcess_eq, this, Finset.sum_range_succ_comm, ← add_assoc]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst : AddCommMonoid β
n : ℕ
this :
  Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) + Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n)
rw :
  Set.indicator {a : Ω | (↑n : ℕ∞) ≤ τ a} (u n) + ∑ i ∈ Finset.range n, Set.indicator {ω : Ω | τ ω = (↑i : ℕ∞)} (u i) =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) +
      ∑ i ∈ Finset.range (n + 1), Set.indicator {a : Ω | τ a = (↑i : ℕ∞)} (u i)
rw₁ :
  Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) + Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n) +
      ∑ i ∈ Finset.range n, Set.indicator {ω : Ω | τ ω = (↑i : ℕ∞)} (u i) =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) +
      ∑ i ∈ Finset.range (n + 1), Set.indicator {a : Ω | τ a = (↑i : ℕ∞)} (u i)
rw₂ :
  Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) + Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n) +
      ∑ i ∈ Finset.range n, Set.indicator {ω : Ω | τ ω = (↑i : ℕ∞)} (u i) =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) +
      (Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n) +
        ∑ x ∈ Finset.range n, Set.indicator {a : Ω | τ a = (↑x : ℕ∞)} (u x))
⊢ stoppedProcess u τ n =
    Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) +
      ∑ i ∈ Finset.range (n + 1), Set.indicator {a : Ω | τ a = (↑i : ℕ∞)} (u i)
have rw₃ : Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) + Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n) +
    ∑ i ∈ Finset.range n, Set.indicator {ω : Ω | τ ω = (↑i : ℕ∞)} (u i) =
  Set.indicator {a : Ω | HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ τ a} (u n) + Set.indicator {a : Ω | τ a = (↑n : ℕ∞)} (u n) +
    ∑ x ∈ Finset.range n, Set.indicator {a : Ω | τ a = (↑x : ℕ∞)} (u x)
Tactic: rw [stoppedProcess_eq, this, Finset.sum_range_succ_comm, ← add_assoc]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 : ι
⊢ {ω : Ω | s.piecewise (β := fun (i : Ω) ↦ WithTop ι) τ η ω ≤ (↑n : WithTop ι)} =
    s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}
have h : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | s.piecewise (β := fun (i : Ω) ↦ WithTop ι) τ η ω ≤ (↑n : WithTop ι)} ω ↔
    ω ∈ s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}
Tactic: ext1 ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 : ι
ω : Ω
⊢ (if ω ∈ s then τ ω else η ω) ≤ (↑n : WithTop ι) ↔
    ω ∈ s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}
have pos : ∀ (hx : ω ∈ s),
  (if ω ∈ s then τ ω else η ω) ≤ (↑n : WithTop ι) ↔
    ω ∈ s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}
Tactic: by_cases hx : ω ∈ s
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 : ι
ω : Ω
pos :
  ∀ (hx : ω ∈ s),
    (if ω ∈ s then τ ω else η ω) ≤ (↑n : WithTop ι) ↔
      ω ∈ s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}
⊢ (if ω ∈ s then τ ω else η ω) ≤ (↑n : WithTop ι) ↔
    ω ∈ s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}
have neg : ∀ (hx : ω ∉ s),
  (if ω ∈ s then τ ω else η ω) ≤ (↑n : WithTop ι) ↔
    ω ∈ s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}
Tactic: by_cases hx : ω ∈ s
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
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 : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | s.piecewise (β := fun (a : Ω) ↦ WithTop ι) τ η ω ≤ (↑n : WithTop ι)}
have this : {ω : Ω | s.piecewise (β := fun (i : Ω) ↦ WithTop ι) τ η ω ≤ (↑n : WithTop ι)} =
  s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)}
Tactic: have : {ω | s.piecewise τ η ω ≤ n} = s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n} := by
    ext1 ω
    simp only [Set.piecewise, Set.mem_setOf_eq]
    by_cases hx : ω ∈ s <;> simp [hx]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | s.piecewise (β := fun (a : Ω) ↦ WithTop ι) τ η ω ≤ (↑n : WithTop ι)}
have rw : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)}
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)})
have pos : ∀ (hin : i ≤ n), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)})
Tactic: by_cases hin : i ≤ n
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)})
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)})
have neg : ∀ (hin : ¬i ≤ n), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)})
Tactic: by_cases hin : i ≤ n
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
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 ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)})
have hs_n : MeasurableSet s
Tactic: have hs_n : MeasurableSet[𝒢 n] s := 𝒢.mono hin _ hs
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
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 ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)})
have hτn : ∀ (ω : Ω), ¬τ ω ≤ (↑n : WithTop ι)
Tactic: have hτn : ∀ ω, ¬τ ω ≤ n := fun ω hτn => hin (mod_cast (hτ ω).trans hτn)
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
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 ι)
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑n : WithTop ι)} ∪ sᶜ ∩ {ω : Ω | η ω ≤ (↑n : WithTop ι)})
have hηn : ∀ (ω : Ω), ¬η ω ≤ (↑n : WithTop ι)
Tactic: have hηn : ∀ ω, ¬η ω ≤ n := fun ω hηn => hin (mod_cast (hη ω).trans hηn)
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
s : Set Ω
inst : DecidablePred fun (x : Ω) ↦ x ∈ s
ι' : Type u_4
α : Type u_5
inst_1 : Nonempty ι'
i j : ι'
f : ι' → Ω → α
⊢ stoppedValue f
      (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) fun (x : Ω) ↦ (↑j : WithTop ι')) =
    s.piecewise (β := fun (i : Ω) ↦ α) (f i) (f j)
have h : ∀ (ω : Ω),
  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 ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
s : Set Ω
inst : DecidablePred fun (x : Ω) ↦ x ∈ s
ι' : Type u_4
α : Type u_5
inst_1 : Nonempty ι'
i j : ι'
f : ι' → Ω → α
ω : Ω
⊢ stoppedValue f
      (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) fun (x : Ω) ↦ (↑j : WithTop ι'))
      ω =
    s.piecewise (β := fun (i : Ω) ↦ α) (f i) (f j) ω
have h : f
    (untopA
      (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) (fun (x : Ω) ↦ (↑j : WithTop ι'))
        ω))
    ω =
  s.piecewise (β := fun (i : Ω) ↦ α) (f i) (f j) ω
Tactic: rw [stoppedValue]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
s : Set Ω
inst : DecidablePred fun (x : Ω) ↦ x ∈ s
ι' : Type u_4
α : Type u_5
inst_1 : Nonempty ι'
i j : ι'
f : ι' → Ω → α
ω : Ω
⊢ f
      (untopA
        (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) (fun (x : Ω) ↦ (↑j : WithTop ι'))
          ω))
      ω =
    s.piecewise (β := fun (i : Ω) ↦ α) (f i) (f j) ω
have 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) ω
Tactic: by_cases hx : ω ∈ s
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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) ω
⊢ f
      (untopA
        (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) (fun (x : Ω) ↦ (↑j : WithTop ι'))
          ω))
      ω =
    s.piecewise (β := fun (i : Ω) ↦ α) (f i) (f j) ω
have 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) ω
Tactic: by_cases hx : ω ∈ s
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 : ι' → Ω → α
⊢ stoppedValue f
      (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) fun (x : Ω) ↦ (↑j : WithTop ι')) =
    s.indicator (f i) + sᶜ.indicator (f j)
have h : ∀ (ω : Ω),
  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 ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 : ι' → Ω → α
ω : Ω
⊢ stoppedValue f
      (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) fun (x : Ω) ↦ (↑j : WithTop ι'))
      ω =
    (s.indicator (f i) + sᶜ.indicator (f j)) ω
have h : f
    (untopA
      (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) (fun (x : Ω) ↦ (↑j : WithTop ι'))
        ω))
    ω =
  (s.indicator (f i) + sᶜ.indicator (f j)) ω
Tactic: rw [stoppedValue]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 : ι' → Ω → α
ω : Ω
⊢ f
      (untopA
        (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) (fun (x : Ω) ↦ (↑j : WithTop ι'))
          ω))
      ω =
    (s.indicator (f i) + sᶜ.indicator (f j)) ω
have 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)) ω
Tactic: by_cases hx : ω ∈ s
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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)) ω
⊢ f
      (untopA
        (s.piecewise (β := fun (a : Ω) ↦ WithTop ι') (fun (x : Ω) ↦ (↑i : WithTop ι')) (fun (x : Ω) ↦ (↑j : WithTop ι'))
          ω))
      ω =
    (s.indicator (f i) + sᶜ.indicator (f j)) ω
have 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)) ω
Tactic: by_cases hx : ω ∈ s
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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]
have refine : ∀ (t : Set Ω),
  MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t)
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 => ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 Ω
⊢ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t)
have rw : MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)})
Tactic: rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)})
⊢ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t)
have rw₁ : MeasurableSet (t ∩ {ω : Ω | τ ω = (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)})
Tactic: rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ⋯)
⊢ ⋯.measurableSpace ≤ hτ.measurableSpace
have rw : hτ.measurableSpace ⊓ (↑ℱ : ι → MeasurableSpace Ω) i ≤ hτ.measurableSpace
Tactic: rw [IsStoppingTime.measurableSpace_min_const]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
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 ⋯)
⊢ μ[f | ⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ (↑i : WithTop ι)})] μ[f | hτ.measurableSpace]
have this : SigmaFinite (μ.trim sorry)
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