-- 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:
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}

Tactic:
simp only [Set.piecewise, Set.mem_inter_iff, Set.mem_setOf_eq, and_congr_right_iff]

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 : ι
ω : Ω
⊢ (if ω ∈ s then τ ω else η ω) ≤ 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 : ι
this : {ω | s.piecewise τ η ω ≤ n} = s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n}
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n})

Tactic:
by_cases hin : i ≤ n

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
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n})

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})

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 : ι
this : {ω | s.piecewise τ η ω ≤ n} = s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n}
⊢ MeasurableSet {ω | s.piecewise τ η ω ≤ n}

Tactic:
rw [this]

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 ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n})