-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSpace_le [IsCountablyGenerated (atTop : Filter ι)] [IsDirected ι (· ≤ ·)]
    (hτ : IsStoppingTime f τ) : hτ.measurableSpace ≤ m

Proof state:
case inr.intro
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
τ : Ω → ι
inst✝¹ : atTop.IsCountablyGenerated
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
hτ : IsStoppingTime f τ
s : Set Ω
h✝ : Nonempty ι
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
⊢ MeasurableSet (⋃ n, s ∩ {ω | τ ω ≤ seq n})

Tactic:
exact MeasurableSet.iUnion fun i => f.le (seq i) _ (hs (seq i))

Result:
no goals

Proof state:
case inl
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
τ : Ω → ι
inst✝¹ : atTop.IsCountablyGenerated
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s
h✝ : IsEmpty ι
this : IsEmpty Ω
⊢ MeasurableSet s

Tactic:
apply Subsingleton.measurableSet

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
τ : Ω → ι
inst✝¹ : atTop.IsCountablyGenerated
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
hτ : IsStoppingTime f τ
s : Set Ω
h✝ : Nonempty ι
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
⊢ s = ⋃ n, s ∩ {ω | τ ω ≤ seq n}

Tactic:
ext ω

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
τ : Ω → ι
inst✝¹ : atTop.IsCountablyGenerated
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
hτ : IsStoppingTime f τ
s : Set Ω
h✝ : Nonempty ι
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
⊢ ω ∈ s ↔ ω ∈ ⋃ n, s ∩ {ω | τ ω ≤ seq n}

Proof state:
case h.mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
τ : Ω → ι
inst✝¹ : atTop.IsCountablyGenerated
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
hτ : IsStoppingTime f τ
s : Set Ω
h✝ : Nonempty ι
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
hx : ω ∈ s
⊢ ∃ i, ω ∈ s ∩ {ω | τ ω ≤ seq i}

Tactic:
suffices ∃ i, τ ω ≤ seq i from ⟨this.choose, hx, this.choose_spec⟩

Result:
case h.mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
τ : Ω → ι
inst✝¹ : atTop.IsCountablyGenerated
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
hτ : IsStoppingTime f τ
s : Set Ω
h✝ : Nonempty ι
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
hx : ω ∈ s
⊢ ∃ i, τ ω ≤ seq i

Proof state:
case h.mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
τ : Ω → ι
inst✝¹ : atTop.IsCountablyGenerated
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
hτ : IsStoppingTime f τ
s : Set Ω
h✝ : Nonempty ι
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
hx : ω ∈ s
⊢ ∃ i, τ ω ≤ seq i

Tactic:
rw [tendsto_atTop] at h_seq_tendsto

Result:
case h.mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
τ : Ω → ι
inst✝¹ : atTop.IsCountablyGenerated
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
hτ : IsStoppingTime f τ
s : Set Ω
h✝ : Nonempty ι
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
seq : ℕ → ι
h_seq_tendsto : ∀ (b : ι), ∀ᶠ (a : ℕ) in atTop, b ≤ seq a
ω : Ω
hx : ω ∈ s
⊢ ∃ i, τ ω ≤ seq i

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
τ : Ω → ι
inst✝¹ : atTop.IsCountablyGenerated
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
τ : Ω → ι
inst✝¹ : atTop.IsCountablyGenerated
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s
h✝ : IsEmpty ι
⊢ MeasurableSet s

case inr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
τ : Ω → ι
inst✝¹ : atTop.IsCountablyGenerated
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s
h✝ : Nonempty ι
⊢ MeasurableSet s

Proof state:
case inr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
τ : Ω → ι
inst✝¹ : atTop.IsCountablyGenerated
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s
h✝ : Nonempty ι
⊢ MeasurableSet s

Tactic:
change ∀ i, MeasurableSet[f i] (s ∩ {ω | τ ω ≤ i}) at hs

Result:
case inr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
τ : Ω → ι
inst✝¹ : atTop.IsCountablyGenerated
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
hτ : IsStoppingTime f τ
s : Set Ω
h✝ : Nonempty ι
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
⊢ MeasurableSet s

Proof state:
case h.mpr.intro.intro
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
τ : Ω → ι
inst✝¹ : atTop.IsCountablyGenerated
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
hτ : IsStoppingTime f τ
s : Set Ω
h✝ : Nonempty ι
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
w✝ : ℕ
hx : ω ∈ s
right✝ : ω ∈ {ω | τ ω ≤ seq w✝}
⊢ ω ∈ s

Tactic:
exact hx

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
τ : Ω → ι
inst✝¹ : atTop.IsCountablyGenerated
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
hτ : IsStoppingTime f τ
⊢ hτ.measurableSpace ≤ m

Tactic:
intro s hs

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
τ : Ω → ι
inst✝¹ : atTop.IsCountablyGenerated
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet s

Proof state:
case h.mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
τ : Ω → ι
inst✝¹ : atTop.IsCountablyGenerated
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
hτ : IsStoppingTime f τ
s : Set Ω
h✝ : Nonempty ι
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
⊢ ω ∈ s → ∃ i, ω ∈ s ∩ {ω | τ ω ≤ seq i}

Tactic:
intro hx

Result:
case h.mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
τ : Ω → ι
inst✝¹ : atTop.IsCountablyGenerated
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
hτ : IsStoppingTime f τ
s : Set Ω
h✝ : Nonempty ι
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
hx : ω ∈ s
⊢ ∃ i, ω ∈ s ∩ {ω | τ ω ≤ seq i}

Proof state:
case h.mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
τ : Ω → ι
inst✝¹ : atTop.IsCountablyGenerated
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
hτ : IsStoppingTime f τ
s : Set Ω
h✝ : Nonempty ι
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
⊢ (∃ i, ω ∈ s ∩ {ω | τ ω ≤ seq i}) → ω ∈ s

Tactic:
rintro ⟨_, hx, _⟩

Result:
case h.mpr.intro.intro
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
τ : Ω → ι
inst✝¹ : atTop.IsCountablyGenerated
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
hτ : IsStoppingTime f τ
s : Set Ω
h✝ : Nonempty ι
hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
ω : Ω
w✝ : ℕ
hx : ω ∈ s
right✝ : ω ∈ {ω | τ ω ≤ seq w✝}
⊢ ω ∈ s