-- Mathlib/Probability/Process/Stopping.lean
theorem add {f : Filtration ℕ m} {τ π : Ω → ℕ} (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) :
    IsStoppingTime f (τ + π)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ π : Ω → ℕ
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ℕ
⊢ MeasurableSet {ω | (τ + π) ω ≤ i}

Tactic:
rw [(_ : {ω | (τ + π) ω ≤ i} = ⋃ k ≤ i, {ω | π ω = k} ∩ {ω | τ ω + k ≤ i})]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ π : Ω → ℕ
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ℕ
⊢ MeasurableSet (⋃ k, ⋃ (_ : k ≤ i), {ω | π ω = k} ∩ {ω | τ ω + k ≤ i})

Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ π : Ω → ℕ
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ℕ
⊢ {ω | (τ + π) ω ≤ i} = ⋃ k, ⋃ (_ : k ≤ i), {ω | π ω = k} ∩ {ω | τ ω + k ≤ i}

Proof state:
case h
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ π : Ω → ℕ
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ℕ
ω : Ω
⊢ ω ∈ {ω | (τ + π) ω ≤ i} ↔ ω ∈ ⋃ k, ⋃ (_ : k ≤ i), {ω | π ω = k} ∩ {ω | τ ω + k ≤ i}

Tactic:
simp only [Pi.add_apply, Set.mem_setOf_eq, Set.mem_iUnion, Set.mem_inter_iff, exists_prop]

Result:
case h
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ π : Ω → ℕ
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ℕ
ω : Ω
⊢ τ ω + π ω ≤ i ↔ ∃ i_1 ≤ i, π ω = i_1 ∧ τ ω + i_1 ≤ i

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ π : Ω → ℕ
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ℕ
⊢ MeasurableSet (⋃ k, ⋃ (_ : k ≤ i), {ω | π ω = k} ∩ {ω | τ ω + k ≤ i})

Tactic:
exact MeasurableSet.iUnion fun k =>
  MeasurableSet.iUnion fun hk => (hπ.measurableSet_eq_le hk).inter (hτ.add_const_nat i)

Result:
no goals

Proof state:
case h
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ π : Ω → ℕ
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ℕ
ω : Ω
⊢ τ ω + π ω ≤ i ↔ ∃ i_1 ≤ i, π ω = i_1 ∧ τ ω + i_1 ≤ i

Tactic:
refine ⟨fun h => ⟨π ω, by omega, rfl, h⟩, ?_⟩

Result:
case h
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ π : Ω → ℕ
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ℕ
ω : Ω
⊢ (∃ i_1 ≤ i, π ω = i_1 ∧ τ ω + i_1 ≤ i) → τ ω + π ω ≤ i

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ π : Ω → ℕ
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ℕ
ω : Ω
h : τ ω + π ω ≤ i
⊢ π ω ≤ i

Tactic:
omega

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ π : Ω → ℕ
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ IsStoppingTime f (τ + π)

Tactic:
intro i

Result:
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ π : Ω → ℕ
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ℕ
⊢ MeasurableSet {ω | (τ + π) ω ≤ i}

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ π : Ω → ℕ
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ℕ
⊢ {ω | (τ + π) ω ≤ i} = ⋃ k, ⋃ (_ : k ≤ i), {ω | π ω = k} ∩ {ω | τ ω + k ≤ i}

Tactic:
ext ω

Result:
case h
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ π : Ω → ℕ
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ℕ
ω : Ω
⊢ ω ∈ {ω | (τ + π) ω ≤ i} ↔ ω ∈ ⋃ k, ⋃ (_ : k ≤ i), {ω | π ω = k} ∩ {ω | τ ω + k ≤ i}

Proof state:
case h
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ π : Ω → ℕ
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ℕ
ω : Ω
⊢ (∃ i_1 ≤ i, π ω = i_1 ∧ τ ω + i_1 ≤ i) → τ ω + π ω ≤ i

Tactic:
rintro ⟨j, hj, rfl, h⟩

Result:
case h.intro.intro.intro
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ π : Ω → ℕ
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ℕ
ω : Ω
hj : π ω ≤ i
h : τ ω + π ω ≤ i
⊢ τ ω + π ω ≤ i

Proof state:
case h.intro.intro.intro
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ π : Ω → ℕ
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ℕ
ω : Ω
hj : π ω ≤ i
h : τ ω + π ω ≤ i
⊢ τ ω + π ω ≤ i

Tactic:
assumption

Result:
no goals