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 : ι
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 : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
h : (↑i : WithTop ι) < τ ω ∨ (↑i : WithTop ι) = τ ω ↔ τ ω = (↑i : WithTop ι) ∨ (↑i : WithTop ι) < τ ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω} ω ↔
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∪ {ω : Ω | (↑i : WithTop ι) < τ ω}) ω

Tactic:
simp only [le_iff_lt_or_eq, Set.mem_setOf_eq, Set.mem_union]

Premises used: Set.mem_union, Set.mem_setOf_eq, le_iff_lt_or_eq
-- 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 : ι
ω : Ω
⊢ (↑i : WithTop ι) < ⊤ ∨ (↑i : WithTop ι) = ⊤ ↔ ⊤ = (↑i : WithTop ι) ∨ (↑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 : ι
ω : Ω
a : ι
h : i < a ∨ i = a ↔ a = i ∨ i < a
⊢ (↑i : WithTop ι) < (↑a : WithTop ι) ∨ (↑i : WithTop ι) = (↑a : WithTop ι) ↔
    (↑a : WithTop ι) = (↑i : WithTop ι) ∨ (↑i : WithTop ι) < (↑a : 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 : ι
ω : Ω
a : ι
h : i < a ∨ a = i ↔ a = i ∨ i < a
h₁ h₂ : a = i ∨ i < a ↔ a = i ∨ i < a
⊢ i < a ∨ i = a ↔ a = i ∨ i < a

Tactic:
rw [@eq_comm _ i, or_comm]

Premises used: eq_comm, or_comm
-- 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 : ∀ (x : WithTop ι), (↑i : WithTop ι) < x ∨ (↑i : WithTop ι) = x ↔ x = (↑i : WithTop ι) ∨ (↑i : WithTop ι) < x
⊢ (↑i : WithTop ι) < τ ω ∨ (↑i : WithTop ι) = τ ω ↔ τ ω = (↑i : WithTop ι) ∨ (↑i : WithTop ι) < τ ω

Tactic:
cases τ ω with
    | top => simp
    | coe a =>
      norm_cast
      rw [@eq_comm _ i, or_comm]

Premises used: eq_comm, WithTop.top, or_comm, 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 : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω}
    ({ω : Ω | τ ω = (↑i : WithTop ι)} ∪ {ω : Ω | (↑i : WithTop ι) < τ ω})

Tactic:
have : {ω | i ≤ τ ω} = {ω | τ ω = i} ∪ {ω | i < τ ω} := by
    ext1 ω
    simp only [le_iff_lt_or_eq, Set.mem_setOf_eq, Set.mem_union]
    cases τ ω with
    | top => simp
    | coe a =>
      norm_cast
      rw [@eq_comm _ i, or_comm]
-- 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_eq' i).union (hτ.measurableSet_gt' i)

Premises used: MeasurableSet.union, MeasureTheory.IsStoppingTime.measurableSet_gt', MeasureTheory.IsStoppingTime.measurableSet_eq'
-- 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_eq' i).union (hτ.measurableSet_gt' i)

Premises used: MeasurableSet.union, MeasureTheory.IsStoppingTime.measurableSet_gt', MeasureTheory.IsStoppingTime.measurableSet_eq'
-- 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 :
  ∀ (ω : Ω),
    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 : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ω ↔
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ {ω : Ω | τ ω = (↑i : WithTop ι)}) ω

Tactic:
simp only [lt_iff_le_and_ne, Set.mem_setOf_eq, Set.mem_diff]

Premises used: lt_iff_le_and_ne, Set.mem_setOf_eq, Set.mem_diff
-- 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 : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ {ω : Ω | τ ω = (↑i : WithTop ι)})

Tactic:
have : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i} := by
    ext1 ω
    simp only [lt_iff_le_and_ne, Set.mem_setOf_eq, Set.mem_diff]
-- 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).diff (hτ.measurableSet_eq' i)

Premises used: MeasurableSet.diff, MeasureTheory.IsStoppingTime.measurableSet_le', MeasureTheory.IsStoppingTime.measurableSet_eq'
-- 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).diff (hτ.measurableSet_eq' i)

Premises used: MeasurableSet.diff, MeasureTheory.IsStoppingTime.measurableSet_le', MeasureTheory.IsStoppingTime.measurableSet_eq'
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
rw : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}

Tactic:
rw [← Set.univ_inter {ω | τ ω = i}, measurableSet_inter_eq_iff, Set.univ_inter]

Premises used: setOf, Set.univ_inter, WithTop.some, Eq, MeasureTheory.IsStoppingTime.measurableSet_inter_eq_iff
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}

Tactic:
hτ.measurableSet_eq_of_countable_range h_countable i

Premises used: MeasureTheory.IsStoppingTime.measurableSet_eq_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 τ
h_countable : (Set.range τ).Countable
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}

Tactic:
exact hτ.measurableSet_eq_of_countable_range h_countable i

Premises used: MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
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 : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
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 : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
h : (↑i : WithTop ι) < τ ω ∨ (↑i : WithTop ι) = τ ω ↔ τ ω = (↑i : WithTop ι) ∨ (↑i : WithTop ι) < τ ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω} ω ↔
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∪ {ω : Ω | (↑i : WithTop ι) < τ ω}) ω

Tactic:
simp only [le_iff_lt_or_eq, Set.mem_setOf_eq, Set.mem_union]

Premises used: Set.mem_union, Set.mem_setOf_eq, le_iff_lt_or_eq
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ (↑i : WithTop ι) < ⊤ ∨ (↑i : WithTop ι) = ⊤ ↔ ⊤ = (↑i : WithTop ι) ∨ (↑i : WithTop ι) < ⊤

Tactic:
simp
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
a : ι
h : i < a ∨ i = a ↔ a = i ∨ i < a
⊢ (↑i : WithTop ι) < (↑a : WithTop ι) ∨ (↑i : WithTop ι) = (↑a : WithTop ι) ↔
    (↑a : WithTop ι) = (↑i : WithTop ι) ∨ (↑i : WithTop ι) < (↑a : WithTop ι)

Tactic:
norm_cast
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
a : ι
h : i < a ∨ a = i ↔ a = i ∨ i < a
h₁ h₂ : a = i ∨ i < a ↔ a = i ∨ i < a
⊢ i < a ∨ i = a ↔ a = i ∨ i < a

Tactic:
rw [@eq_comm _ i, or_comm]

Premises used: eq_comm, or_comm
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
h : ∀ (x : WithTop ι), (↑i : WithTop ι) < x ∨ (↑i : WithTop ι) = x ↔ x = (↑i : WithTop ι) ∨ (↑i : WithTop ι) < x
⊢ (↑i : WithTop ι) < τ ω ∨ (↑i : WithTop ι) = τ ω ↔ τ ω = (↑i : WithTop ι) ∨ (↑i : WithTop ι) < τ ω

Tactic:
cases τ ω with
    | top => simp
    | coe a =>
      norm_cast
      rw [@eq_comm _ i, or_comm]

Premises used: eq_comm, WithTop.top, or_comm, WithTop.coe
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
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 only [le_iff_lt_or_eq, Set.mem_setOf_eq, Set.mem_union]
    cases τ ω with
    | top => simp
    | coe a =>
      norm_cast
      rw [@eq_comm _ i, or_comm]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
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 : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
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_eq_of_countable_range' h_countable i).union (hτ.measurableSet_gt' i)

Premises used: MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range', MeasurableSet.union, MeasureTheory.IsStoppingTime.measurableSet_gt'
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
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_eq_of_countable_range' h_countable i).union (hτ.measurableSet_gt' i)

Premises used: MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range', MeasurableSet.union, MeasureTheory.IsStoppingTime.measurableSet_gt'
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
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 τ
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 : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ω ↔
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ {ω : Ω | τ ω = (↑i : WithTop ι)}) ω

Tactic:
simp only [lt_iff_le_and_ne, Set.mem_setOf_eq, Set.mem_diff]

Premises used: lt_iff_le_and_ne, Set.mem_setOf_eq, Set.mem_diff
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
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 only [lt_iff_le_and_ne, Set.mem_setOf_eq, Set.mem_diff]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
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 : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
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: MeasurableSet.diff, MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range', MeasureTheory.IsStoppingTime.measurableSet_le'
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
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: MeasurableSet.diff, MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range', MeasureTheory.IsStoppingTime.measurableSet_le'
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
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
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : SecondCountableTopology ι
hτ : IsStoppingTime f τ
⊢ Measurable τ

Tactic:
measurable_of_Iic fun i ↦ ?_

Premises used: measurable_of_Iic
-- 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 : SecondCountableTopology ι
hτ : IsStoppingTime f τ
refine : ∀ (i : WithTop ι), MeasurableSet (τ ⁻¹' Set.Iic i)
⊢ Measurable τ

Tactic:
refine measurable_of_Iic fun i ↦ ?_

Premises used: measurable_of_Iic
-- 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 : SecondCountableTopology ι
hτ : IsStoppingTime f τ
⊢ MeasurableSet (τ ⁻¹' Set.Iic ⊤)

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 : SecondCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet (τ ⁻¹' Set.Iic (↑i : WithTop ι))

Tactic:
hτ.measurableSet_le' i

Premises used: Set.Mem, setOf, MeasureTheory.IsStoppingTime.measurableSet_le', Set.preimage, Set.Iic
-- 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 : SecondCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet (τ ⁻¹' Set.Iic (↑i : WithTop ι))

Tactic:
exact hτ.measurableSet_le' i

Premises used: MeasureTheory.IsStoppingTime.measurableSet_le'
-- 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 : SecondCountableTopology ι
hτ : IsStoppingTime f τ
i : WithTop ι
top : MeasurableSet (τ ⁻¹' Set.Iic ⊤)
coe : ∀ (i : ι), MeasurableSet (τ ⁻¹' Set.Iic (↑i : WithTop ι))
⊢ MeasurableSet (τ ⁻¹' Set.Iic i)

Tactic:
cases i with
  | top => simp
  | coe i => exact hτ.measurableSet_le' i

Premises used: WithTop.top, WithTop.coe