-- Mathlib/Probability/Process/Stopping.lean
theorem IsStoppingTime.measurableSet_lt_of_isLUB (hτ : IsStoppingTime f τ) (i : ι)
    (h_lub : IsLUB (Set.Iio i) i) : MeasurableSet[f i] {ω | τ ω < i}

Proof state:
case h.refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : ∀ s ∈ 𝓝 i, ∃ a, ∀ b ≥ a, seq b ∈ s
h_bound : ∀ (j : ℕ), seq j < i
k : ι
hk_lt_i : k < i
h_nhds : Set.Ici k ∈ 𝓝 i
⊢ ∃ i, k ≤ seq i

Tactic:
obtain ⟨a, ha⟩ : ∃ a : ℕ, ∀ b : ℕ, b ≥ a → k ≤ seq b := h_tendsto (Set.Ici k) h_nhds

Result:
case h.refine_1.intro
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : ∀ s ∈ 𝓝 i, ∃ a, ∀ b ≥ a, seq b ∈ s
h_bound : ∀ (j : ℕ), seq j < i
k : ι
hk_lt_i : k < i
h_nhds : Set.Ici k ∈ 𝓝 i
a : ℕ
ha : ∀ b ≥ a, k ≤ seq b
⊢ ∃ i, k ≤ seq i

Proof state:
case neg.intro.intro.intro.intro
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
h_Ioi_eq_Union : Set.Iio i = ⋃ j, {k | k ≤ seq j}
h_lt_eq_preimage : {ω | τ ω < i} = τ ⁻¹' Set.Iio i
⊢ MeasurableSet {ω | τ ω < i}

Tactic:
rw [h_lt_eq_preimage, h_Ioi_eq_Union]

Result:
case neg.intro.intro.intro.intro
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
h_Ioi_eq_Union : Set.Iio i = ⋃ j, {k | k ≤ seq j}
h_lt_eq_preimage : {ω | τ ω < i} = τ ⁻¹' Set.Iio i
⊢ MeasurableSet (τ ⁻¹' ⋃ j, {k | k ≤ seq j})

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
this : {ω | τ ω < i} = ∅
⊢ MeasurableSet {ω | τ ω < i}

Tactic:
rw [this]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
this : {ω | τ ω < i} = ∅
⊢ MeasurableSet ∅

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
this : {ω | τ ω < i} = ∅
⊢ MeasurableSet ∅

Tactic:
exact @MeasurableSet.empty _ (f i)

Result:
no goals

Proof state:
case pos.h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
ω : Ω
⊢ ω ∈ {ω | τ ω < i} ↔ ω ∈ ∅

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

Result:
case pos.h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
ω : Ω
⊢ ¬τ ω < i