awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
j : WithTop ι
h : j ∈ Set.range τ
rw rw₁ rw₂ : MeasurableSet.{u_1} (α := Ω) (if j < (↑i : WithTop ι) then {ω : Ω | τ ω ≤ j} else ∅)
pos : ∀ (hji : j < (↑i : WithTop ι)), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ j}
neg neg₁ : ∀ (hji : ¬j < (↑i : WithTop ι)), MeasurableSet.{u_1} (α := Ω) ∅
⊢ MeasurableSet.{u_1} (α := Ω) (⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})

Tactic:
classical
  rw [Set.iUnion_eq_if]
  split_ifs with hji
  · lift j to ι using (ne_top_of_lt hji)
    exact f.mono (mod_cast hji.le) _ (hτ.measurableSet_le j)
  · exact @MeasurableSet.empty _ (f i)

Premises used: MeasurableSet.empty, Set.iUnion_eq_if
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
inst_1 : Countable ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}

Tactic:
hτ.measurableSet_eq_of_countable_range (Set.to_countable _) i

Premises used: MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range, Set.to_countable
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
h :
  ∀ (ω : Ω),
    Membership.mem (γ := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ω ↔
      Membership.mem (γ := Set Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ {ω : Ω | τ ω = (↑i : WithTop ι)}) ω
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ {ω : Ω | τ ω = (↑i : WithTop ι)})

Tactic:
ext1 ω
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ω ↔
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ {ω : Ω | τ ω = (↑i : WithTop ι)}) ω

Tactic:
simp [lt_iff_le_and_ne]

Premises used: lt_iff_le_and_ne
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ {ω : Ω | τ ω = (↑i : WithTop ι)})

Tactic:
have : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i} := by ext1 ω; simp [lt_iff_le_and_ne]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
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 : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
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).diff (hτ.measurableSet_eq_of_countable_range h_countable i)

Premises used: MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range, MeasurableSet.diff, MeasureTheory.IsStoppingTime.measurableSet_le
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
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).diff (hτ.measurableSet_eq_of_countable_range h_countable i)

Premises used: MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range, MeasurableSet.diff, MeasureTheory.IsStoppingTime.measurableSet_le
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
inst_1 : Countable ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}

Tactic:
hτ.measurableSet_lt_of_countable_range (Set.to_countable _) i

Premises used: MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable_range, Set.to_countable
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst : LinearOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
h :
  ∀ (ω : Ω),
    Membership.mem (γ := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω} ω ↔
      Membership.mem (γ := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}ᶜ ω
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω} {ω : Ω | τ ω < (↑i : WithTop ι)}ᶜ

Tactic:
ext1 ω
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst : LinearOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω} ω ↔
    Membership.mem (γ := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}ᶜ ω

Tactic:
simp only [Set.mem_setOf_eq, Set.mem_compl_iff, not_lt]

Premises used: Set.mem_setOf_eq, not_lt, Set.mem_compl_iff
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst : LinearOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω} {ω : Ω | τ ω < (↑i : WithTop ι)}ᶜ

Tactic:
have : {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ := by
    ext1 ω; simp only [Set.mem_setOf_eq, Set.mem_compl_iff, not_lt]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst : LinearOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω} {ω : Ω | τ ω < (↑i : WithTop ι)}ᶜ
rw : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}ᶜ
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω}

Tactic:
rw [this]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst : LinearOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω} {ω : Ω | τ ω < (↑i : WithTop ι)}ᶜ
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}ᶜ

Tactic:
(hτ.measurableSet_lt_of_countable_range h_countable i).compl

Premises used: MeasurableSet.compl, MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable_range
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst : LinearOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω} {ω : Ω | τ ω < (↑i : WithTop ι)}ᶜ
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}ᶜ

Tactic:
exact (hτ.measurableSet_lt_of_countable_range h_countable i).compl

Premises used: MeasurableSet.compl, MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable_range
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst : LinearOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
inst_1 : Countable ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω}

Tactic:
hτ.measurableSet_ge_of_countable_range (Set.to_countable _) i

Premises used: Set.to_countable, MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable_range
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
h :
  ∀ (ω : Ω),
    Membership.mem (γ := Set Ω) {ω : Ω | (↑i : WithTop ι) < τ ω} ω ↔
      Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ ω
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) < τ ω} {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ

Tactic:
ext1 ω
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | (↑i : WithTop ι) < τ ω} ω ↔
    Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ ω

Tactic:
simp only [Set.mem_setOf_eq, Set.mem_compl_iff, not_le]

Premises used: not_le, Set.mem_setOf_eq, Set.mem_compl_iff
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) < τ ω} {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ

Tactic:
have : {ω | i < τ ω} = {ω | τ ω ≤ i}ᶜ := by
    ext1 ω; simp only [Set.mem_setOf_eq, Set.mem_compl_iff, not_le]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) < τ ω} {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ
rw : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑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 ι
hτ : IsStoppingTime f τ
i : ι
this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) < τ ω} {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ

Tactic:
(hτ.measurableSet_le i).compl

Premises used: MeasureTheory.IsStoppingTime.measurableSet_le, MeasurableSet.compl
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) < τ ω} {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ

Tactic:
exact (hτ.measurableSet_le i).compl

Premises used: MeasureTheory.IsStoppingTime.measurableSet_le, MeasurableSet.compl
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
pos : ∀ (hi_min : IsMin i), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
neg : ∀ (hi_min : ¬IsMin i), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}

Tactic:
by_cases hi_min : IsMin i

Premises used: IsMin
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ∅
rw : MeasurableSet.{u_1} (α := Ω) ∅
⊢ 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ∅
⊢ MeasurableSet.{u_1} (α := Ω) ∅

Tactic:
@MeasurableSet.empty _ (f i)

Premises used: MeasurableSet.empty
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ∅
⊢ MeasurableSet.{u_1} (α := Ω) ∅

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

Premises used: MeasurableSet.empty
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
pos : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ∅
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}

Tactic:
suffices {ω | τ ω < i} = ∅ by rw [this]; exact @MeasurableSet.empty _ (f i)
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
pos : ∀ (ω : Ω), Membership.mem (γ := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ω ↔ Membership.mem (γ := Set Ω) ∅ ω
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ∅

Tactic:
ext1 ω
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
ω : Ω
pos : ¬τ ω < (↑i : WithTop ι)
⊢ Membership.mem (γ := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ω ↔ Membership.mem (γ := Set Ω) ∅ ω

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

Premises used: iff_false, Set.mem_setOf_eq, Set.mem_empty_iff_false
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
ω : Ω
⊢ ¬⊤ < (↑i : WithTop ι)

Tactic:
simp
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
ω : Ω
t : ι
pos : ¬t < i
⊢ ¬(↑t : WithTop ι) < (↑i : WithTop ι)

Tactic:
norm_cast
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
ω : Ω
t : ι
⊢ ¬t < i

Tactic:
isMin_iff_forall_not_lt.mp hi_min t

Premises used: isMin_iff_forall_not_lt, Iff.mp
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
ω : Ω
t : ι
⊢ ¬t < i

Tactic:
exact isMin_iff_forall_not_lt.mp hi_min t

Premises used: isMin_iff_forall_not_lt, Iff.mp
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
ω : Ω
pos : ∀ (x : WithTop ι), ¬x < (↑i : WithTop ι)
⊢ ¬τ ω < (↑i : WithTop ι)

Tactic:
cases τ ω with
    | top => simp
    | coe t => norm_cast; exact isMin_iff_forall_not_lt.mp hi_min t

Premises used: WithTop.top, WithTop.coe
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
⊢ ∃ (seq : ℕ → ι), Monotone seq ∧ (∀ (j : ℕ), seq j ≤ i) ∧ Tendsto seq atTop (𝓝 i) ∧ ∀ (j : ℕ), seq j < i

Tactic:
h_lub.exists_seq_monotone_tendsto (not_isMin_iff.mp hi_min)

Premises used: not_isMin_iff, Set.Mem, setOf, Iff.mp, IsLUB.exists_seq_monotone_tendsto, Set.Iio
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
neg :
  ∀ (seq : ℕ → ι) (h_tendsto : Tendsto seq atTop (𝓝 i)) (h_bound : ∀ (j : ℕ), seq j < i),
    MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}

Tactic:
obtain ⟨seq, -, -, h_tendsto, h_bound⟩ :
      ∃ seq : ℕ → ι, Monotone seq ∧ (∀ j, seq j ≤ i) ∧ Tendsto seq atTop (𝓝 i) ∧ ∀ j, seq j < i :=
    h_lub.exists_seq_monotone_tendsto (not_isMin_iff.mp hi_min)

Premises used: not_isMin_iff, Monotone, Filter.seq, nhds, Filter.atTop, Filter.Tendsto, Iff.mp, IsLUB.exists_seq_monotone_tendsto
-- 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 : ι
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 :
  ∀ (k : WithTop ι),
    k ∈ Set.Iio (↑i : WithTop ι) ↔
      Membership.mem (γ := Set (WithTop ι)) (⋃ (j : ℕ), {k : WithTop ι | k ≤ (↑(seq j) : WithTop ι)}) k
⊢ Set.Iio (↑i : WithTop ι) = ⋃ (j : ℕ), {k : WithTop ι | k ≤ (↑(seq j) : WithTop ι)}

Tactic:
ext1 k
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
k : WithTop ι
h : k < (↑i : WithTop ι) ↔ ∃ (i : ℕ), k ≤ (↑(seq i) : WithTop ι)
⊢ k ∈ Set.Iio (↑i : WithTop ι) ↔
    Membership.mem (γ := Set (WithTop ι)) (⋃ (j : ℕ), {k : WithTop ι | k ≤ (↑(seq j) : WithTop ι)}) k

Tactic:
push _ ∈ _
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
k : WithTop ι
⊢ k < (↑i : WithTop ι) ↔ ∃ (i : ℕ), k ≤ (↑(seq i) : WithTop ι)

Tactic:
⟨fun hk_lt_i => ?_, fun h_exists_k_le_seq => ?_⟩

Premises used: Iff.intro
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
k : WithTop ι
h : ∀ (hk_lt_i : k < (↑i : WithTop ι)), ∃ (i : ℕ), k ≤ (↑(seq i) : WithTop ι)
h₁ : ∀ (h_exists_k_le_seq : ∃ (i : ℕ), k ≤ (↑(seq i) : WithTop ι)), k < (↑i : WithTop ι)
⊢ k < (↑i : WithTop ι) ↔ ∃ (i : ℕ), k ≤ (↑(seq i) : WithTop ι)

Tactic:
refine ⟨fun hk_lt_i => ?_, fun h_exists_k_le_seq => ?_⟩
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
k : WithTop ι
hk_lt_i : k < (↑i : WithTop ι)
h :
  ∀ (h_tendsto : ∀ s ∈ 𝓝 i, ∃ (a : ℕ), ∀ b ≥ a, seq b ∈ s) (h_bound : ∀ (j : ℕ), seq j < i) (k : WithTop ι)
    (hk_lt_i : k < (↑i : WithTop ι)), ∃ (i : ℕ), k ≤ (↑(seq i) : WithTop ι)
⊢ ∃ (i : ℕ), k ≤ (↑(seq i) : WithTop ι)

Tactic:
rw [tendsto_atTop'] at h_tendsto

Premises used: Filter.tendsto_atTop'
-- 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 : ι
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
hk_lt_i : ⊤ < (↑i : WithTop ι)
⊢ ∃ (i : ℕ), ⊤ ≤ (↑(seq i) : WithTop ι)

Tactic:
simp at hk_lt_i
-- 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 : ι
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 : WithTop ι) < (↑i : WithTop ι)
h : ∀ (hk_lt_i : k < i), ∃ (i : ℕ), k ≤ seq i
⊢ ∃ (i : ℕ), (↑k : WithTop ι) ≤ (↑(seq i) : WithTop ι)

Tactic:
norm_cast at hk_lt_i ⊢
-- 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 : ι
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
⊢ Set.Ici k ∈ 𝓝 i

Tactic:
have h_nhds : Set.Ici k ∈ 𝓝 i :=
          mem_nhds_iff.mpr ⟨Set.Ioi k, Set.Ioi_subset_Ici le_rfl, isOpen_Ioi, hk_lt_i⟩