awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Predictable
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
β : Type u_4
inst : TopologicalSpace β
f : Filtration ℕ m
u : ℕ → Ω → β
hu : StronglyAdapted (β := fun (n : ℕ) ↦ β) f fun (n : ℕ) ↦ u (n + 1)
hu0 : StronglyMeasurable (u 0)
⊢ StronglyAdapted (β := fun (i : ℕ) ↦ β) f u

Tactic:
fun n =>
  match n with
  | 0 => hu0
  | n + 1 => (hu n).mono (f.mono n.le_succ)

Premises used: Nat.le_succ, _private.0.MeasureTheory.Predictable.stronglyAdapted.match_1, MeasureTheory.StronglyAdapted, MeasureTheory.StronglyMeasurable.mono, MeasureTheory.Filtration.mono, MeasureTheory.StronglyMeasurable
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
i j : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (fun (x : Ω) ↦ (↑i : WithTop ι)) ω ≤ (↑j : WithTop ι)}

Tactic:
simp only [MeasurableSet.const]

Premises used: MeasurableSet.const
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}

Tactic:
hτ i
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
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 : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
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 : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
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 : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
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 : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
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 : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
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 : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
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 : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : IsMin i
ω : Ω
pos : ∀ (hi_min : ∀ (b : ι), ¬b < i) (ω : Ω), ¬τ ω < (↑i : WithTop ι)
⊢ ¬τ ω < (↑i : WithTop ι)

Tactic:
rw [isMin_iff_forall_not_lt] at hi_min

Premises used: isMin_iff_forall_not_lt
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ∀ (b : ι), ¬b < i
ω : Ω
⊢ ¬⊤ < (↑i : WithTop ι)

Tactic:
simp
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ∀ (b : ι), ¬b < i
ω : Ω
t : ι
⊢ ¬(↑t : WithTop ι) < (↑i : WithTop ι)

Tactic:
mod_cast hi_min t

Premises used: congrArg, cast, WithTop.coe_lt_coe._simp_1, Eq.symm, Not
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ∀ (b : ι), ¬b < i
ω : Ω
t : ι
⊢ ¬(↑t : WithTop ι) < (↑i : WithTop ι)

Tactic:
exact mod_cast hi_min t
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ∀ (b : ι), ¬b < i
ω : Ω
pos : ∀ (x : WithTop ι), ¬x < (↑i : WithTop ι)
⊢ ¬τ ω < (↑i : WithTop ι)

Tactic:
cases τ ω with
    | top => simp
    | coe t => exact mod_cast hi_min t

Premises used: WithTop.top, WithTop.coe
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
h :
  ∀ (ω : Ω),
    Membership.mem (γ := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ω ↔ ω ∈ τ ⁻¹' Set.Iic (↑(Order.pred i) : WithTop ι)
⊢ {ω : Ω | τ ω < (↑i : WithTop ι)} = τ ⁻¹' Set.Iic (↑(Order.pred i) : WithTop ι)

Tactic:
ext ω
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
ω : Ω
⊢ ⊤ < (↑i : WithTop ι) ↔ ⊤ ≤ (↑(Order.pred i) : WithTop ι)

Tactic:
simp
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
ω : Ω
t : ι
h : t < i ↔ t ≤ Order.pred i
⊢ (↑t : WithTop ι) < (↑i : WithTop ι) ↔ (↑t : WithTop ι) ≤ (↑(Order.pred i) : WithTop ι)

Tactic:
simp only [coe_lt_coe, coe_le_coe]

Premises used: WithTop.coe_lt_coe, WithTop.coe_le_coe
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
ω : Ω
t : ι
h h₁ : t < i ↔ t < i
⊢ t < i ↔ t ≤ Order.pred i

Tactic:
rw [le_pred_iff_of_not_isMin hi_min]

Premises used: Order.le_pred_iff_of_not_isMin
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
ω : Ω
h : ∀ (x : WithTop ι), x < (↑i : WithTop ι) ↔ x ≤ (↑(Order.pred i) : WithTop ι)
⊢ τ ω < (↑i : WithTop ι) ↔ τ ω ≤ (↑(Order.pred i) : WithTop ι)

Tactic:
cases τ ω with
    | top => simp
    | coe t =>
      simp only [coe_lt_coe, coe_le_coe]
      rw [le_pred_iff_of_not_isMin hi_min]

Premises used: Order.le_pred_iff_of_not_isMin, WithTop.coe_lt_coe, WithTop.top, WithTop.coe_le_coe, WithTop.coe
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
⊢ {ω : Ω | τ ω < (↑i : WithTop ι)} = τ ⁻¹' Set.Iic (↑(Order.pred i) : WithTop ι)

Tactic:
have : {ω : Ω | τ ω < i} = τ ⁻¹' Set.Iic (pred i : ι) := by
    ext ω
    push _ ∈ _
    cases τ ω with
    | top => simp
    | coe t =>
      simp only [coe_lt_coe, coe_le_coe]
      rw [le_pred_iff_of_not_isMin hi_min]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
this : {ω : Ω | τ ω < (↑i : WithTop ι)} = τ ⁻¹' Set.Iic (↑(Order.pred i) : WithTop ι)
neg : MeasurableSet (τ ⁻¹' Set.Iic (↑(Order.pred 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 : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
this : {ω : Ω | τ ω < (↑i : WithTop ι)} = τ ⁻¹' Set.Iic (↑(Order.pred i) : WithTop ι)
⊢ MeasurableSet (τ ⁻¹' Set.Iic (↑(Order.pred i) : WithTop ι))

Tactic:
f.mono (pred_le i) _ (hτ.measurableSet_le <| pred i)

Premises used: MeasureTheory.IsStoppingTime.measurableSet_le, Order.pred_le, Order.pred, MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
this : {ω : Ω | τ ω < (↑i : WithTop ι)} = τ ⁻¹' Set.Iic (↑(Order.pred i) : WithTop ι)
⊢ MeasurableSet (τ ⁻¹' Set.Iic (↑(Order.pred i) : WithTop ι))

Tactic:
exact f.mono (pred_le i) _ (hτ.measurableSet_le <| pred i)

Premises used: MeasureTheory.IsStoppingTime.measurableSet_le, Order.pred_le, Order.pred, MeasureTheory.Filtration.mono
-- 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 :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} a ↔
      Membership.mem (γ := Set Ω)
        ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j}) a
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})

Tactic:
ext1 a
-- 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 : ι
a : Ω
h : τ a = (↑i : WithTop ι) ↔ τ a ≤ (↑i : WithTop ι) ∧ ∀ (x : Ω), τ x < (↑i : WithTop ι) → ¬τ a ≤ τ x
⊢ Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} a ↔
    Membership.mem (γ := Set Ω)
      ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j}) a

Tactic:
simp only [Set.mem_setOf_eq, Set.mem_range, Set.iUnion_exists, Set.iUnion_iUnion_eq',
      Set.mem_diff, Set.mem_iUnion, exists_prop, not_exists, not_and]

Premises used: Set.mem_range, Set.mem_iUnion, not_exists, Set.mem_setOf_eq, exists_prop, Set.mem_diff, Set.iUnion_exists, not_and, Set.iUnion_iUnion_eq'
-- 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 : ι
a : Ω
h : τ a = (↑i : WithTop ι) → τ a ≤ (↑i : WithTop ι) ∧ ∀ (x : Ω), τ x < (↑i : WithTop ι) → ¬τ a ≤ τ x
h₁ : (τ a ≤ (↑i : WithTop ι) ∧ ∀ (x : Ω), τ x < (↑i : WithTop ι) → ¬τ a ≤ τ x) → τ a = (↑i : WithTop ι)
⊢ τ a = (↑i : WithTop ι) ↔ τ a ≤ (↑i : WithTop ι) ∧ ∀ (x : Ω), τ x < (↑i : WithTop ι) → ¬τ a ≤ τ x

Tactic:
constructor
-- 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 : ι
a : Ω
h : τ a = (↑i : WithTop ι)
⊢ τ a ≤ (↑i : WithTop ι) ∧ ∀ (x : Ω), τ x < (↑i : WithTop ι) → ¬τ a ≤ τ x

Tactic:
simp only [h, lt_iff_le_not_ge, le_refl, and_imp, imp_self, imp_true_iff, and_self_iff]

Premises used: le_refl, lt_iff_le_not_ge, and_imp, imp_true_iff, imp_self, and_self_iff
-- 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 : ι
a : Ω
h : τ a ≤ (↑i : WithTop ι) ∧ ∀ (x : Ω), τ x < (↑i : WithTop ι) → ¬τ a ≤ τ x
⊢ τ a = (↑i : WithTop ι)

Tactic:
h.1.eq_or_lt.resolve_right fun h_lt => h.2 a h_lt le_rfl

Premises used: LE.le.eq_or_lt, le_rfl, And.right, And.left, Or.resolve_right
-- 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 : ι
a : Ω
h : τ a ≤ (↑i : WithTop ι) ∧ ∀ (x : Ω), τ x < (↑i : WithTop ι) → ¬τ a ≤ τ x
⊢ τ a = (↑i : WithTop ι)

Tactic:
exact h.1.eq_or_lt.resolve_right fun h_lt => h.2 a h_lt le_rfl

Premises used: LE.le.eq_or_lt, le_rfl, And.right, And.left, Or.resolve_right
-- 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 ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})

Tactic:
have : {ω | τ ω = i} = {ω | τ ω ≤ i} \ ⋃ (j ∈ Set.range τ) (_ : j < i), {ω | τ ω ≤ j} := by
    ext1 a
    simp only [Set.mem_setOf_eq, Set.mem_range, Set.iUnion_exists, Set.iUnion_iUnion_eq',
      Set.mem_diff, Set.mem_iUnion, exists_prop, not_exists, not_and]
    constructor <;> intro h
    · simp only [h, lt_iff_le_not_ge, le_refl, and_imp, imp_self, imp_true_iff, and_self_iff]
    · exact h.1.eq_or_lt.resolve_right fun h_lt => h.2 a h_lt le_rfl
-- 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})
rw :
  MeasurableSet.{u_1} (α := Ω)
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
⊢ 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 ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
⊢ MeasurableSet.{u_1} (α := Ω)
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})

Tactic:
(hτ.measurableSet_le i).diff ?_

Premises used: 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 ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
refine : MeasurableSet.{u_1} (α := Ω) (⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
⊢ MeasurableSet.{u_1} (α := Ω)
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})

Tactic:
refine (hτ.measurableSet_le i).diff ?_

Premises used: 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 ι)} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
⊢ MeasurableSet.{u_1} (α := Ω) (⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})

Tactic:
MeasurableSet.biUnion h_countable fun j _ => ?_

Premises used: MeasurableSet.biUnion
-- 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})
refine : ∀ j ∈ Set.range τ, MeasurableSet.{u_1} (α := Ω) (⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})
⊢ MeasurableSet.{u_1} (α := Ω) (⋃ j ∈ Set.range τ, ⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})

Tactic:
refine MeasurableSet.biUnion h_countable fun j _ => ?_

Premises used: MeasurableSet.biUnion
-- 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 : MeasurableSet.{u_1} (α := Ω) (if j < (↑i : WithTop ι) then {ω : Ω | τ ω ≤ j} else ∅)
⊢ MeasurableSet.{u_1} (α := Ω) (⋃ (_ : j < (↑i : WithTop ι)), {ω : Ω | τ ω ≤ j})

Tactic:
rw [Set.iUnion_eq_if]

Premises used: Set.iUnion_eq_if
-- 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 τ
pos : ∀ (hji : j < (↑i : WithTop ι)), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ j}
neg : ∀ (hji : ¬j < (↑i : WithTop ι)), MeasurableSet.{u_1} (α := Ω) ∅
⊢ MeasurableSet.{u_1} (α := Ω) (if j < (↑i : WithTop ι) then {ω : Ω | τ ω ≤ j} else ∅)

Tactic:
split_ifs with hji
-- 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 τ
hji : j < (↑i : WithTop ι)
⊢ j ≠ ⊤

Tactic:
(ne_top_of_lt hji)

Premises used: ne_top_of_lt
-- 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 τ
hji : j < (↑i : WithTop ι)
pos :
  ∀ (j : ι),
    (↑j : WithTop ι) ∈ Set.range τ →
      ∀ (hji : (↑j : WithTop ι) < (↑i : WithTop ι)), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑j : WithTop ι)}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ j}

Tactic:
lift j to ι using (ne_top_of_lt hji)

Premises used: ne_top_of_lt
-- 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 : ι
h : (↑j : WithTop ι) ∈ Set.range τ
hji : (↑j : WithTop ι) < (↑i : WithTop ι)
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑j : WithTop ι)}

Tactic:
f.mono (mod_cast hji.le) _ (hτ.measurableSet_le j)

Premises used: MeasureTheory.IsStoppingTime.measurableSet_le, MeasureTheory.Filtration.mono
-- 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 : ι
h : (↑j : WithTop ι) ∈ Set.range τ
hji : (↑j : WithTop ι) < (↑i : WithTop ι)
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑j : WithTop ι)}

Tactic:
exact f.mono (mod_cast hji.le) _ (hτ.measurableSet_le j)

Premises used: MeasureTheory.IsStoppingTime.measurableSet_le, MeasureTheory.Filtration.mono
-- 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 τ
hji : ¬j < (↑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 : 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 τ
hji : ¬j < (↑i : WithTop ι)
⊢ MeasurableSet.{u_1} (α := Ω) ∅

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

Premises used: MeasurableSet.empty