awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≥ (↑i : WithTop ι)})
rw : MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≥ (↑i : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}

Tactic:
rw [this]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≥ (↑i : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≥ (↑i : WithTop ι)})

Tactic:
(hτ.measurableSet_le i).inter (hτ.measurableSet_ge i)

Premises used: MeasureTheory.IsStoppingTime.measurableSet_le, MeasureTheory.IsStoppingTime.measurableSet_ge, MeasurableSet.inter
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≥ (↑i : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≥ (↑i : WithTop ι)})

Tactic:
exact (hτ.measurableSet_le i).inter (hτ.measurableSet_ge i)

Premises used: MeasureTheory.IsStoppingTime.measurableSet_le, MeasureTheory.IsStoppingTime.measurableSet_ge, MeasurableSet.inter
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i j : ι
hle : i ≤ j
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}

Tactic:
f.mono hle _ <| hτ.measurableSet_eq i

Premises used: MeasureTheory.IsStoppingTime.measurableSet_eq, MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i j : ι
hle : i ≤ j
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}

Tactic:
f.mono hle _ <| hτ.measurableSet_lt i

Premises used: MeasureTheory.IsStoppingTime.measurableSet_lt, MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
inst_1 : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
i : ι
h :
  ∀ (ω : Ω),
    Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ω ↔
      Membership.mem (γ := Set Ω) (⋃ (k : ι), ⋃ (_ : k ≤ i), {ω : Ω | τ ω = (↑k : WithTop ι)}) ω
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
    (⋃ (k : ι), ⋃ (_ : k ≤ i), {ω : Ω | τ ω = (↑k : WithTop ι)})

Tactic:
ext ω
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
inst_1 : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
i : ι
ω : Ω
h : τ ω ≤ (↑i : WithTop ι) ↔ ∃ i_1 ≤ i, τ ω = (↑i_1 : WithTop ι)
⊢ Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ω ↔
    Membership.mem (γ := Set Ω) (⋃ (k : ι), ⋃ (_ : k ≤ i), {ω : Ω | τ ω = (↑k : WithTop ι)}) ω

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

Premises used: Set.mem_iUnion, Set.mem_setOf_eq, exists_prop
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
inst_1 : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
i : ι
ω : Ω
⊢ ⊤ ≤ (↑i : WithTop ι) ↔ ∃ i_1 ≤ i, ⊤ = (↑i_1 : WithTop ι)

Tactic:
simp
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
inst_1 : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
i : ι
ω : Ω
a : ι
h : a ≤ i ↔ ∃ i_1 ≤ i, a = i_1
⊢ (↑a : WithTop ι) ≤ (↑i : WithTop ι) ↔ ∃ i_1 ≤ i, (↑a : WithTop ι) = (↑i_1 : WithTop ι)

Tactic:
norm_cast
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
inst_1 : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
i : ι
ω : Ω
a : ι
⊢ a ≤ i ↔ ∃ i_1 ≤ i, a = i_1

Tactic:
simp
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
inst_1 : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
i : ι
ω : Ω
h : ∀ (x : WithTop ι), x ≤ (↑i : WithTop ι) ↔ ∃ i_1 ≤ i, x = (↑i_1 : WithTop ι)
⊢ τ ω ≤ (↑i : WithTop ι) ↔ ∃ i_1 ≤ i, τ ω = (↑i_1 : WithTop ι)

Tactic:
cases τ ω with
    | top => simp
    | coe a => norm_cast; simp

Premises used: WithTop.top, WithTop.coe
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
inst_1 : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
i : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
    (⋃ (k : ι), ⋃ (_ : k ≤ i), {ω : Ω | τ ω = (↑k : WithTop ι)})

Tactic:
have h_eq_iUnion : {ω | τ ω ≤ i} = ⋃ k ≤ i, {ω | τ ω = k} := by
    ext ω
    simp only [Set.mem_setOf_eq, Set.mem_iUnion, exists_prop]
    cases τ ω with
    | top => simp
    | coe a => norm_cast; simp
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
inst_1 : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
i : ι
h_eq_iUnion :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
    (⋃ (k : ι), ⋃ (_ : k ≤ i), {ω : Ω | τ ω = (↑k : WithTop ι)})
rw : MeasurableSet.{u_1} (α := Ω) (⋃ (k : ι), ⋃ (_ : k ≤ i), {ω : Ω | τ ω = (↑k : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}

Tactic:
rw [h_eq_iUnion]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
inst_1 : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
i : ι
h_eq_iUnion :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
    (⋃ (k : ι), ⋃ (_ : k ≤ i), {ω : Ω | τ ω = (↑k : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) (⋃ (k : ι), ⋃ (_ : k ≤ i), {ω : Ω | τ ω = (↑k : WithTop ι)})

Tactic:
MeasurableSet.biUnion (Set.to_countable _) fun k hk => ?_

Premises used: Set.Mem, Set.to_countable, MeasurableSet.biUnion
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
inst_1 : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
i : ι
h_eq_iUnion :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
    (⋃ (k : ι), ⋃ (_ : k ≤ i), {ω : Ω | τ ω = (↑k : WithTop ι)})
refine :
  ∀ (k : ι) (hk : Membership.mem (γ := Set ι) (fun (k : ι) ↦ (Preorder.toLE : LE ι).1 k i) k),
    MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑k : WithTop ι)}
⊢ MeasurableSet.{u_1} (α := Ω) (⋃ (k : ι), ⋃ (_ : k ≤ i), {ω : Ω | τ ω = (↑k : WithTop ι)})

Tactic:
refine MeasurableSet.biUnion (Set.to_countable _) fun k hk => ?_

Premises used: Set.to_countable, MeasurableSet.biUnion
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
inst_1 : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
i : ι
h_eq_iUnion :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
    (⋃ (k : ι), ⋃ (_ : k ≤ i), {ω : Ω | τ ω = (↑k : WithTop ι)})
k : ι
hk : Membership.mem (γ := Set ι) (fun (k : ι) ↦ (Preorder.toLE : LE ι).1 k i) k
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑k : WithTop ι)}

Tactic:
f.mono hk _ (hτ k)

Premises used: MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
inst_1 : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
i : ι
h_eq_iUnion :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
    (⋃ (k : ι), ⋃ (_ : k ≤ i), {ω : Ω | τ ω = (↑k : WithTop ι)})
k : ι
hk : Membership.mem (γ := Set ι) (fun (k : ι) ↦ (Preorder.toLE : LE ι).1 k i) k
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑k : WithTop ι)}

Tactic:
exact f.mono hk _ (hτ k)

Premises used: MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
pos : ∀ (ht : 𝓝[>] t = ⊥), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
neg : ∀ (ht : ¬𝓝[>] t = ⊥), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}

Tactic:
by_cases ht : 𝓝[>] t = ⊥
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : 𝓝[>] t = ⊥
h :
  ∀ (x : Ω),
    Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)} x ↔
      Membership.mem (γ := Set Ω) ({ω : Ω | τ ω < (↑t : WithTop ι)} ∪ {ω : Ω | τ ω = (↑t : WithTop ι)}) x
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
    ({ω : Ω | τ ω < (↑t : WithTop ι)} ∪ {ω : Ω | τ ω = (↑t : WithTop ι)})

Tactic:
ext
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : 𝓝[>] t = ⊥
x : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)} x ↔
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω < (↑t : WithTop ι)} ∪ {ω : Ω | τ ω = (↑t : WithTop ι)}) x

Tactic:
grind
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : 𝓝[>] t = ⊥
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
    ({ω : Ω | τ ω < (↑t : WithTop ι)} ∪ {ω : Ω | τ ω = (↑t : WithTop ι)})

Tactic:
have h_eq : {ω | τ ω ≤ t} = {ω | τ ω < t} ∪ {ω | τ ω = t} := by ext; grind
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : 𝓝[>] t = ⊥
h_eq :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
    ({ω : Ω | τ ω < (↑t : WithTop ι)} ∪ {ω : Ω | τ ω = (↑t : WithTop ι)})
pos : MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω < (↑t : WithTop ι)} ∪ {ω : Ω | τ ω = (↑t : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}

Tactic:
rw [h_eq]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : 𝓝[>] t = ⊥
h_eq :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
    ({ω : Ω | τ ω < (↑t : WithTop ι)} ∪ {ω : Ω | τ ω = (↑t : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω < (↑t : WithTop ι)} ∪ {ω : Ω | τ ω = (↑t : WithTop ι)})

Tactic:
(hτ1 t).union (hτ2 t ht)

Premises used: MeasurableSet.union
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : 𝓝[>] t = ⊥
h_eq :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
    ({ω : Ω | τ ω < (↑t : WithTop ι)} ∪ {ω : Ω | τ ω = (↑t : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω < (↑t : WithTop ι)} ∪ {ω : Ω | τ ω = (↑t : WithTop ι)})

Tactic:
exact (hτ1 t).union (hτ2 t ht)

Premises used: MeasurableSet.union
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
⊢ (𝓝[>] t).NeBot

Tactic:
have : (𝓝[>] t).NeBot := ⟨ht⟩
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
⊢ ∃ᶠ (x : ι) in 𝓝[>] t, t < x

Tactic:
have h_freq : ∃ᶠ x in 𝓝[>] t, t < x :=
      Eventually.frequently <| eventually_nhdsWithin_of_forall fun _ hx ↦ hx
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
h_freq : ∃ᶠ (x : ι) in 𝓝[>] t, t < x
⊢ ∃ (ns : ℕ → ι), Tendsto ns atTop (𝓝[>] t) ∧ ∀ (n : ℕ), t < ns n

Tactic:
have := exists_seq_forall_of_frequently h_freq
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this_1 : (𝓝[>] t).NeBot
h_freq : ∃ᶠ (x : ι) in 𝓝[>] t, t < x
this : ∃ (ns : ℕ → ι), Tendsto ns atTop (𝓝[>] t) ∧ ∀ (n : ℕ), t < ns n
⊢ ∃ (ns : ℕ → ι), (Tendsto ns atTop (𝓝 t) ∧ ∀ᶠ (n : ℕ) in atTop, ns n ∈ Set.Ioi t) ∧ ∀ (n : ℕ), t < ns n

Tactic:
simp_rw [tendsto_nhdsWithin_iff] at this

Premises used: tendsto_nhdsWithin_iff
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this_1 : (𝓝[>] t).NeBot
h_freq : ∃ᶠ (x : ι) in 𝓝[>] t, t < x
this : ∃ (ns : ℕ → ι), (Tendsto ns atTop (𝓝 t) ∧ ∀ᶠ (n : ℕ) in atTop, ns n ∈ Set.Ioi t) ∧ ∀ (n : ℕ), t < ns n
obtain :
  ∀ (s : ℕ → ι) (hs_gt : ∀ (n : ℕ), t < s n) (hs_tendsto : Tendsto s atTop (𝓝 t)),
    (∀ᶠ (n : ℕ) in atTop, s n ∈ Set.Ioi t) → ∃ (s : ℕ → ι), (∀ (n : ℕ), t < s n) ∧ Tendsto s atTop (𝓝 t)
⊢ ∃ (s : ℕ → ι), (∀ (n : ℕ), t < s n) ∧ Tendsto s atTop (𝓝 t)

Tactic:
obtain ⟨s, ⟨hs_tendsto, _⟩, hs_gt⟩ := this
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
h_freq : ∃ᶠ (x : ι) in 𝓝[>] t, t < x
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
right : ∀ᶠ (n : ℕ) in atTop, s n ∈ Set.Ioi t
⊢ ∃ (s : ℕ → ι), (∀ (n : ℕ), t < s n) ∧ Tendsto s atTop (𝓝 t)

Tactic:
⟨s, hs_gt, hs_tendsto⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
h_freq : ∃ᶠ (x : ι) in 𝓝[>] t, t < x
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
right : ∀ᶠ (n : ℕ) in atTop, s n ∈ Set.Ioi t
⊢ ∃ (s : ℕ → ι), (∀ (n : ℕ), t < s n) ∧ Tendsto s atTop (𝓝 t)

Tactic:
exact ⟨s, hs_gt, hs_tendsto⟩
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
neg :
  ∀ (s : ℕ → ι) (hs_gt : ∀ (n : ℕ), t < s n) (hs_tendsto : Tendsto s atTop (𝓝 t)),
    MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}

Tactic:
obtain ⟨s, hs_gt, hs_tendsto⟩ : ∃ s : ℕ → ι, (∀ n, t < s n) ∧ Tendsto s atTop (𝓝 t) := by
    have h_freq : ∃ᶠ x in 𝓝[>] t, t < x :=
      Eventually.frequently <| eventually_nhdsWithin_of_forall fun _ hx ↦ hx
    have := exists_seq_forall_of_frequently h_freq
    simp_rw [tendsto_nhdsWithin_iff] at this
    obtain ⟨s, ⟨hs_tendsto, _⟩, hs_gt⟩ := this
    exact ⟨s, hs_gt, hs_tendsto⟩
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
⊢ ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u

Tactic:
have h_exists_lt (u : ι) (hu : t < u) : ∃ i, s i < u :=
    Eventually.exists (f := atTop) (hs_tendsto.eventually_lt_const hu)
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
u : WithTop ι
hu : (↑t : WithTop ι) < u
⊢ ∃ (i : ℕ), (↑(s i) : WithTop ι) < u

Tactic:
Eventually.exists (f := atTop) ?_

Premises used: Filter.Eventually.exists
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
u : WithTop ι
hu : (↑t : WithTop ι) < u
refine : ∀ᶠ (x : ℕ) in atTop, (↑(s x) : WithTop ι) < u
⊢ ∃ (i : ℕ), (↑(s i) : WithTop ι) < u

Tactic:
refine Eventually.exists (f := atTop) ?_

Premises used: Filter.Eventually.exists