-- Mathlib/Probability/Process/Stopping.lean
theorem IsStoppingTime.piecewise_of_le (hτ_st : IsStoppingTime 𝒢 τ) (hη_st : IsStoppingTime 𝒢 η)
    (hτ : ∀ ω, i ≤ τ ω) (hη : ∀ ω, i ≤ η ω) (hs : MeasurableSet[𝒢 i] s) :
    IsStoppingTime 𝒢 (s.piecewise τ η)

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), i ≤ τ ω
hη : ∀ (ω : Ω), i ≤ η ω
hs : MeasurableSet s
⊢ IsStoppingTime 𝒢 (s.piecewise τ η)

Tactic:
intro n

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), i ≤ τ ω
hη : ∀ (ω : Ω), i ≤ η ω
hs : MeasurableSet s
n : ι
⊢ MeasurableSet {ω | s.piecewise τ η ω ≤ n}

Proof state:
case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), i ≤ τ ω
hη : ∀ (ω : Ω), i ≤ η ω
hs : MeasurableSet s
n : ι
this : {ω | s.piecewise τ η ω ≤ n} = s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n}
hin : ¬i ≤ n
hτn : ∀ (ω : Ω), ¬τ ω ≤ n
hηn : ∀ (ω : Ω), ¬η ω ≤ n
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n})

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

Result:
no goals

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), i ≤ τ ω
hη : ∀ (ω : Ω), i ≤ η ω
hs : MeasurableSet s
n : ι
ω : Ω
⊢ (if ω ∈ s then τ ω else η ω) ≤ n ↔ ω ∈ s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n}

Tactic:
by_cases hx : ω ∈ s <;> simp [hx]

Result:
no goals

Proof state:
case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), i ≤ τ ω
hη : ∀ (ω : Ω), i ≤ η ω
hs : MeasurableSet s
n : ι
this : {ω | s.piecewise τ η ω ≤ n} = s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n}
hin : i ≤ n
hs_n : MeasurableSet s
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n})

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

Result:
no goals

Proof state:
case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), i ≤ τ ω
hη : ∀ (ω : Ω), i ≤ η ω
hs : MeasurableSet s
n : ι
this : {ω | s.piecewise τ η ω ≤ n} = s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n}
hin : i ≤ n
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n})

Tactic:
have hs_n : MeasurableSet[𝒢 n] s := 𝒢.mono hin _ hs

Result:
case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), i ≤ τ ω
hη : ∀ (ω : Ω), i ≤ η ω
hs : MeasurableSet s
n : ι
this : {ω | s.piecewise τ η ω ≤ n} = s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n}
hin : i ≤ n
hs_n : MeasurableSet s
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n})

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), i ≤ τ ω
hη : ∀ (ω : Ω), i ≤ η ω
hs : MeasurableSet s
n : ι
⊢ {ω | s.piecewise τ η ω ≤ n} = s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n}

Tactic:
ext1 ω

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), i ≤ τ ω
hη : ∀ (ω : Ω), i ≤ η ω
hs : MeasurableSet s
n : ι
ω : Ω
⊢ ω ∈ {ω | s.piecewise τ η ω ≤ n} ↔ ω ∈ s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), i ≤ τ ω
hη : ∀ (ω : Ω), i ≤ η ω
hs : MeasurableSet s
n : ι
⊢ MeasurableSet {ω | s.piecewise τ η ω ≤ n}

Tactic:
have : {ω | s.piecewise τ η ω ≤ n} = s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n} := by
  ext1 ω
  simp only [Set.piecewise, Set.mem_inter_iff, Set.mem_setOf_eq, and_congr_right_iff]
  by_cases hx : ω ∈ s <;> simp [hx]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), i ≤ τ ω
hη : ∀ (ω : Ω), i ≤ η ω
hs : MeasurableSet s
n : ι
this : {ω | s.piecewise τ η ω ≤ n} = s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n}
⊢ MeasurableSet {ω | s.piecewise τ η ω ≤ n}

Proof state:
case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), i ≤ τ ω
hη : ∀ (ω : Ω), i ≤ η ω
hs : MeasurableSet s
n : ι
this : {ω | s.piecewise τ η ω ≤ n} = s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n}
hin : ¬i ≤ n
hτn : ∀ (ω : Ω), ¬τ ω ≤ n
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n})

Tactic:
have hηn : ∀ ω, ¬η ω ≤ n := fun ω hηn => hin ((hη ω).trans hηn)

Result:
case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), i ≤ τ ω
hη : ∀ (ω : Ω), i ≤ η ω
hs : MeasurableSet s
n : ι
this : {ω | s.piecewise τ η ω ≤ n} = s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n}
hin : ¬i ≤ n
hτn : ∀ (ω : Ω), ¬τ ω ≤ n
hηn : ∀ (ω : Ω), ¬η ω ≤ n
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n})

Proof state:
case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), i ≤ τ ω
hη : ∀ (ω : Ω), i ≤ η ω
hs : MeasurableSet s
n : ι
this : {ω | s.piecewise τ η ω ≤ n} = s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n}
hin : ¬i ≤ n
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n})

Tactic:
have hτn : ∀ ω, ¬τ ω ≤ n := fun ω hτn => hin ((hτ ω).trans hτn)

Result:
case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), i ≤ τ ω
hη : ∀ (ω : Ω), i ≤ η ω
hs : MeasurableSet s
n : ι
this : {ω | s.piecewise τ η ω ≤ n} = s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n}
hin : ¬i ≤ n
hτn : ∀ (ω : Ω), ¬τ ω ≤ n
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n})