-- Mathlib/Probability/Process/Stopping.lean
theorem add_const_nat {f : Filtration ℕ m} {τ : Ω → ℕ} (hτ : IsStoppingTime f τ) {i : ℕ} :
    IsStoppingTime f fun ω => τ ω + i

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ : Ω → ℕ
hτ : IsStoppingTime f τ
i j : ℕ
hij : j < i
⊢ MeasurableSet {ω | τ ω + i = j}

Tactic:
convert @MeasurableSet.empty _ (f.1 j)

Result:
case h.e'_3
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ : Ω → ℕ
hτ : IsStoppingTime f τ
i j : ℕ
hij : j < i
⊢ {ω | τ ω + i = j} = ∅

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ : Ω → ℕ
hτ : IsStoppingTime f τ
i j : ℕ
hij : i ≤ j
⊢ MeasurableSet {ω | τ ω = j - i}

Tactic:
exact f.mono (j.sub_le i) _ (hτ.measurableSet_eq (j - i))

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ : Ω → ℕ
hτ : IsStoppingTime f τ
i j : ℕ
⊢ MeasurableSet {ω | τ ω + i = j}

Tactic:
by_cases hij : i ≤ j

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ : Ω → ℕ
hτ : IsStoppingTime f τ
i j : ℕ
hij : i ≤ j
⊢ MeasurableSet {ω | τ ω + i = j}

case neg
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ : Ω → ℕ
hτ : IsStoppingTime f τ
i j : ℕ
hij : ¬i ≤ j
⊢ MeasurableSet {ω | τ ω + i = j}

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ : Ω → ℕ
hτ : IsStoppingTime f τ
i : ℕ
⊢ IsStoppingTime f fun ω => τ ω + i

Tactic:
refine isStoppingTime_of_measurableSet_eq fun j => ?_

Result:
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ : Ω → ℕ
hτ : IsStoppingTime f τ
i j : ℕ
⊢ MeasurableSet {ω | τ ω + i = j}

Proof state:
case h.e'_3
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ : Ω → ℕ
hτ : IsStoppingTime f τ
i j : ℕ
hij : j < i
⊢ {ω | τ ω + i = j} = ∅

Tactic:
ext ω

Result:
case h.e'_3.h
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ : Ω → ℕ
hτ : IsStoppingTime f τ
i j : ℕ
hij : j < i
ω : Ω
⊢ ω ∈ {ω | τ ω + i = j} ↔ ω ∈ ∅

Proof state:
case h.e'_3.h
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ : Ω → ℕ
hτ : IsStoppingTime f τ
i j : ℕ
hij : j < i
ω : Ω
⊢ ¬τ ω + i = j

Tactic:
omega

Result:
no goals

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ : Ω → ℕ
hτ : IsStoppingTime f τ
i j : ℕ
hij : ¬i ≤ j
⊢ MeasurableSet {ω | τ ω + i = j}

Tactic:
rw [not_le] at hij

Result:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ : Ω → ℕ
hτ : IsStoppingTime f τ
i j : ℕ
hij : j < i
⊢ MeasurableSet {ω | τ ω + i = j}

Proof state:
case h.e'_3.h
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ : Ω → ℕ
hτ : IsStoppingTime f τ
i j : ℕ
hij : j < i
ω : Ω
⊢ ω ∈ {ω | τ ω + i = j} ↔ ω ∈ ∅

Tactic:
simp only [Set.mem_empty_iff_false, iff_false, Set.mem_setOf]

Result:
case h.e'_3.h
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ : Ω → ℕ
hτ : IsStoppingTime f τ
i j : ℕ
hij : j < i
ω : Ω
⊢ ¬τ ω + i = j

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ : Ω → ℕ
hτ : IsStoppingTime f τ
i j : ℕ
hij : i ≤ j
⊢ MeasurableSet {ω | τ ω + i = j}

Tactic:
simp_rw [eq_comm, ← Nat.sub_eq_iff_eq_add hij, eq_comm]

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
f : Filtration ℕ m
τ : Ω → ℕ
hτ : IsStoppingTime f τ
i j : ℕ
hij : i ≤ j
⊢ MeasurableSet {ω | τ ω = j - i}