awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet s
j : ι
hij : ¬i ≤ j
⊢ MeasurableSet (s ∩ {ω : Ω | i ≤ j})

Tactic:
simp only [hij, Set.setOf_false, Set.inter_empty, @MeasurableSet.empty _ (f.1 j)]

Premises used: MeasurableSet.empty, Set.setOf_false, Set.inter_empty
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
j : WithTop ι
h :
  ∀ (ω : Ω),
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j}) ω ↔
      Membership.mem (γ := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j}) ω
⊢ Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
    ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})

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

Tactic:
simp only [Set.mem_inter_iff, Set.mem_setOf_eq, and_congr_right_iff]

Premises used: Set.mem_inter_iff, Set.mem_setOf_eq, and_congr_right_iff
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
j : WithTop ι
ω : Ω
hxi : τ ω = (↑i : WithTop ι)
h h₁ : (↑i : WithTop ι) ≤ j ↔ (↑i : WithTop ι) ≤ j
⊢ τ ω ≤ j ↔ (↑i : WithTop ι) ≤ j

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

Tactic:
have : ∀ j, {ω : Ω | τ ω = i} ∩ {ω : Ω | τ ω ≤ j} = {ω : Ω | τ ω = i} ∩ {_ω | i ≤ j} := by
    intro j
    ext1 ω
    simp only [Set.mem_inter_iff, Set.mem_setOf_eq, and_congr_right_iff]
    intro hxi
    rw [hxi]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this :
  ∀ (j : WithTop ι),
    Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
      ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})
mp : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)}) → MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
mpr : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)}) → MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)}) ↔ MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})

Tactic:
constructor
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this :
  ∀ (j : WithTop ι),
    Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
      ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})
h : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})

Tactic:
simpa [Set.inter_assoc, this] using h.2 i

Premises used: And.right, Set.inter_assoc
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this :
  ∀ (j : WithTop ι),
    Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
      ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})
h : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})

Tactic:
⟨f.le i _ h, fun j ↦ ?_⟩

Premises used: MeasurableSet, And.intro, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this :
  ∀ (j : WithTop ι),
    Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
      ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})
h : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
mpr : ∀ (j : ι), MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})

Tactic:
refine ⟨f.le i _ h, fun j ↦ ?_⟩
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this :
  ∀ (j : WithTop ι),
    Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
      ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})
h : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
j : ι
mpr : MeasurableSet (s ∩ ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)}))
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})

Tactic:
rw [Set.inter_assoc, this]

Premises used: Set.inter_assoc
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this :
  ∀ (j : WithTop ι),
    Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
      ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})
h : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
j : ι
pos :
  ∀ (hij : i ≤ j),
    MeasurableSet (s ∩ ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)}))
neg :
  ∀ (hij : ¬i ≤ j),
    MeasurableSet (s ∩ ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)}))
⊢ MeasurableSet (s ∩ ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)}))

Tactic:
by_cases hij : i ≤ j
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this :
  ∀ (j : WithTop ι),
    Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
      ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})
h : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
j : ι
hij : i ≤ j
pos : MeasurableSet (s ∩ ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | i ≤ j}))
⊢ MeasurableSet (s ∩ ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)}))

Tactic:
norm_cast
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this :
  ∀ (j : WithTop ι),
    Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
      ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})
h : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
j : ι
hij : i ≤ j
pos : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
⊢ MeasurableSet (s ∩ ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | i ≤ j}))

Tactic:
simp only [hij, Set.setOf_true, Set.inter_univ]

Premises used: Set.inter_univ, Set.setOf_true
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this :
  ∀ (j : WithTop ι),
    Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
      ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})
h : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
j : ι
hij : i ≤ j
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})

Tactic:
f.mono hij _ h

Premises used: MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this :
  ∀ (j : WithTop ι),
    Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
      ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})
h : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
j : ι
hij : i ≤ j
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})

Tactic:
exact f.mono hij _ h

Premises used: MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this :
  ∀ (j : WithTop ι),
    Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
      ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})
h : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
j : ι
hij : ¬i ≤ j
⊢ MeasurableSet (s ∩ ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)}))

Tactic:
simp [hij]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑i : WithTop ι)
⊢ hτ.measurableSpace ≤ (↑f : ι → MeasurableSpace Ω) i

Tactic:
(measurableSpace_mono hτ _ hτ_le).trans (measurableSpace_const _ _).le

Premises used: MeasureTheory.IsStoppingTime.measurableSpace_mono, Eq.le, LE.le.trans, MeasureTheory.IsStoppingTime.measurableSpace_const
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
⊢ hτ.measurableSpace ≤ m

Tactic:
(hτ.measurableSpace_le_of_le_const hτ_le).trans (f.le n)

Premises used: MeasureTheory.IsStoppingTime.measurableSpace_le_of_le_const, MeasureTheory.Filtration.le, LE.le.trans
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hτ_le : ∀ (ω : Ω), (↑i : WithTop ι) ≤ τ ω
⊢ (↑f : ι → MeasurableSpace Ω) i ≤ hτ.measurableSpace

Tactic:
(measurableSpace_const _ _).symm.le.trans (measurableSpace_mono _ hτ hτ_le)

Premises used: MeasureTheory.IsStoppingTime.measurableSpace_mono, Eq.le, LE.le.trans, Eq.symm, MeasureTheory.IsStoppingTime.measurableSpace_const
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι_1 : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst : SemilatticeSup ι
inst_1 : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst_2 : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
@sigmaFiniteTrim_mono _ _ ?_ _ _ _ ?_ ?_

Premises used: MeasureTheory.sigmaFiniteTrim_mono
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι_1 : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst : SemilatticeSup ι
inst_1 : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst_2 : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
refine_1 : MeasurableSpace Ω
refine_2 : (↑f : ι → MeasurableSpace Ω) ⊥ ≤ hτ.measurableSpace
refine_3 : SigmaFinite (m0 := (↑f : ι → MeasurableSpace Ω) ⊥) (μ.trim ⋯)
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
refine @sigmaFiniteTrim_mono _ _ ?_ _ _ _ ?_ ?_

Premises used: MeasureTheory.sigmaFiniteTrim_mono
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι_1 : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst : SemilatticeSup ι
inst_1 : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst_2 : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
⊢ MeasurableSpace Ω

Tactic:
exact f ⊥

Premises used: MeasureTheory.Filtration.seq, Bot.bot
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι_1 : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst : SemilatticeSup ι
inst_1 : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst_2 : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
⊢ (↑f : ι → MeasurableSpace Ω) ⊥ ≤ hτ.measurableSpace

Tactic:
hτ.le_measurableSpace_of_const_le fun _ => bot_le

Premises used: bot_le, MeasureTheory.IsStoppingTime.le_measurableSpace_of_const_le
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι_1 : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst : SemilatticeSup ι
inst_1 : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst_2 : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
⊢ (↑f : ι → MeasurableSpace Ω) ⊥ ≤ hτ.measurableSpace

Tactic:
exact hτ.le_measurableSpace_of_const_le fun _ => bot_le

Premises used: bot_le, MeasureTheory.IsStoppingTime.le_measurableSpace_of_const_le
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι_1 : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst : SemilatticeSup ι
inst_1 : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst_2 : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
⊢ SigmaFinite (m0 := (↑f : ι → MeasurableSpace Ω) ⊥) (μ.trim ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι_1 : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst : SemilatticeSup ι
inst_1 : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst_2 : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
@sigmaFiniteTrim_mono _ _ ?_ _ _ _ ?_ ?_

Premises used: MeasureTheory.sigmaFiniteTrim_mono
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι_1 : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst : SemilatticeSup ι
inst_1 : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst_2 : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
refine_1 : MeasurableSpace Ω
refine_2 : (↑f : ι → MeasurableSpace Ω) ⊥ ≤ hτ.measurableSpace
refine_3 : SigmaFinite (m0 := (↑f : ι → MeasurableSpace Ω) ⊥) (μ.trim ⋯)
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
refine @sigmaFiniteTrim_mono _ _ ?_ _ _ _ ?_ ?_

Premises used: MeasureTheory.sigmaFiniteTrim_mono
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι_1 : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst : SemilatticeSup ι
inst_1 : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst_2 : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
⊢ MeasurableSpace Ω

Tactic:
exact f ⊥

Premises used: MeasureTheory.Filtration.seq, Bot.bot
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι_1 : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst : SemilatticeSup ι
inst_1 : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst_2 : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
⊢ (↑f : ι → MeasurableSpace Ω) ⊥ ≤ hτ.measurableSpace

Tactic:
hτ.le_measurableSpace_of_const_le fun _ => bot_le

Premises used: bot_le, MeasureTheory.IsStoppingTime.le_measurableSpace_of_const_le
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι_1 : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst : SemilatticeSup ι
inst_1 : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst_2 : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
⊢ (↑f : ι → MeasurableSpace Ω) ⊥ ≤ hτ.measurableSpace

Tactic:
exact hτ.le_measurableSpace_of_const_le fun _ => bot_le

Premises used: bot_le, MeasureTheory.IsStoppingTime.le_measurableSpace_of_const_le
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι_1 : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst : SemilatticeSup ι
inst_1 : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst_2 : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
⊢ SigmaFinite (m0 := (↑f : ι → MeasurableSpace Ω) ⊥) (μ.trim ⋯)

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

Tactic:
⟨f.le i _ (hτ i), fun j ↦ ?_⟩

Premises used: MeasurableSet, And.intro, MeasureTheory.Filtration.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 : ι
refine : ∀ (j : ι), MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}

Tactic:
refine ⟨f.le i _ (hτ i), fun j ↦ ?_⟩
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i j : ι
h :
  ∀ (ω : Ω),
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)}) ω ↔
      Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑(min i j) : WithTop ι)} ω
⊢ Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
    {ω : Ω | τ ω ≤ (↑(min i j) : 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 j : ι
ω : Ω
⊢ Membership.mem (γ := Set Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)}) ω ↔
    Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑(min i j) : WithTop ι)} ω

Tactic:
simp [Set.mem_inter_iff, Set.mem_setOf_eq]

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

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

Tactic:
f.mono (min_le_right i j) _ (hτ _)

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

Tactic:
exact f.mono (min_le_right i j) _ (hτ _)

Premises used: min_le_right, MeasureTheory.Filtration.mono
-- 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
-- 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
-- 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: MeasurableSet.compl, 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 τ
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: MeasurableSet.compl, 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 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
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 ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}

Tactic:
hτ.measurableSet_eq i

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

Tactic:
exact hτ.measurableSet_eq i

Premises used: MeasureTheory.IsStoppingTime.measurableSet_eq