awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Add ι
inst_1 : LinearOrder ι
inst_2 : CanonicallyOrderedAdd ι
inst_3 : Countable ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
a b : ι
⊢ a + b ≤ j ↔ ∃ (i : (↑(Set.Iic j) : Type u_3)), b = (↑i : ι) ∧ a + (↑i : ι) ≤ j

Tactic:
simpa using le_of_add_le_right

Premises used: le_of_add_le_right
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Add ι
inst_1 : LinearOrder ι
inst_2 : CanonicallyOrderedAdd ι
inst_3 : Countable ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
a : ι
h :
  ∀ (x : WithTop ι),
    (↑a : WithTop ι) + x ≤ (↑j : WithTop ι) ↔
      ∃ (i : (↑(Set.Iic j) : Type u_3)),
        x = (↑(↑i : ι) : WithTop ι) ∧ (↑a : WithTop ι) + (↑(↑i : ι) : WithTop ι) ≤ (↑j : WithTop ι)
⊢ (↑a : WithTop ι) + π ω ≤ (↑j : WithTop ι) ↔
    ∃ (i : (↑(Set.Iic j) : Type u_3)),
      π ω = (↑(↑i : ι) : WithTop ι) ∧ (↑a : WithTop ι) + (↑(↑i : ι) : WithTop ι) ≤ (↑j : WithTop ι)

Tactic:
cases π ω with
      | top => simp
      | coe b => norm_cast; simpa using le_of_add_le_right

Premises used: le_of_add_le_right, WithTop.top, WithTop.coe
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Add ι
inst_1 : LinearOrder ι
inst_2 : CanonicallyOrderedAdd ι
inst_3 : Countable ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
h :
  ∀ (x : WithTop ι),
    x + π ω ≤ (↑j : WithTop ι) ↔
      ∃ (i : (↑(Set.Iic j) : Type u_3)), π ω = (↑(↑i : ι) : WithTop ι) ∧ x + (↑(↑i : ι) : WithTop ι) ≤ (↑j : WithTop ι)
⊢ τ ω + π ω ≤ (↑j : WithTop ι) ↔
    ∃ (i : (↑(Set.Iic j) : Type u_3)), π ω = (↑(↑i : ι) : WithTop ι) ∧ τ ω + (↑(↑i : ι) : WithTop ι) ≤ (↑j : WithTop ι)

Tactic:
cases τ ω with
    | top => simp
    | coe a =>
      cases π ω with
      | top => simp
      | coe b => norm_cast; simpa using le_of_add_le_right

Premises used: le_of_add_le_right, WithTop.top, WithTop.coe
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Add ι
inst_1 : LinearOrder ι
inst_2 : CanonicallyOrderedAdd ι
inst_3 : Countable ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (τ + π) ω ≤ (↑j : WithTop ι)}
    (⋃ (k : (↑(Set.Iic j) : Type u_3)),
      {ω : Ω | π ω = (↑(↑k : ι) : WithTop ι)} ∩ {ω : Ω | τ ω + (↑(↑k : ι) : WithTop ι) ≤ (↑j : WithTop ι)})

Tactic:
have h : {ω | (τ + π) ω ≤ j} = ⋃ k : Set.Iic j, {ω | π ω = k} ∩ {ω | τ ω + k ≤ j} := by
    ext ω
    simp only [Pi.add_apply, Set.mem_setOf_eq, Set.mem_iUnion, Set.mem_inter_iff]
    cases τ ω with
    | top => simp
    | coe a =>
      cases π ω with
      | top => simp
      | coe b => norm_cast; simpa using le_of_add_le_right
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Add ι
inst_1 : LinearOrder ι
inst_2 : CanonicallyOrderedAdd ι
inst_3 : Countable ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
h :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (τ + π) ω ≤ (↑j : WithTop ι)}
    (⋃ (k : (↑(Set.Iic j) : Type u_3)),
      {ω : Ω | π ω = (↑(↑k : ι) : WithTop ι)} ∩ {ω : Ω | τ ω + (↑(↑k : ι) : WithTop ι) ≤ (↑j : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (τ + π) ω ≤ (↑j : WithTop ι)}

Tactic:
h ▸ MeasurableSet.iUnion fun k => (hπ.measurableSet_eq_le k.2).inter (hτ.add_const' k.1 j)

Premises used: MeasureTheory.IsStoppingTime.add_const', MeasureTheory.IsStoppingTime.measurableSet_eq_le, Eq.rec, MeasurableSet.iUnion, Eq.symm, Subtype.val, Subtype.property, MeasurableSet.inter
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Add ι
inst_1 : LinearOrder ι
inst_2 : CanonicallyOrderedAdd ι
inst_3 : Countable ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
h :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (τ + π) ω ≤ (↑j : WithTop ι)}
    (⋃ (k : (↑(Set.Iic j) : Type u_3)),
      {ω : Ω | π ω = (↑(↑k : ι) : WithTop ι)} ∩ {ω : Ω | τ ω + (↑(↑k : ι) : WithTop ι) ≤ (↑j : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (τ + π) ω ≤ (↑j : WithTop ι)}

Tactic:
exact h ▸ MeasurableSet.iUnion fun k => (hπ.measurableSet_eq_le k.2).inter (hτ.add_const' k.1 j)
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
⊢ MeasurableSet.{u_1} (α := Ω) ∅ ∧ ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) (∅ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})

Tactic:
simp
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
⊢ MeasurableSet sᶜ ∧ ∀ (i : ι), MeasurableSet (sᶜ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})

Tactic:
⟨hs.1.compl, fun i ↦ ?_⟩

Premises used: MeasurableSet.compl, And.left, And.intro
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
refine : ∀ (i : ι), MeasurableSet (sᶜ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
⊢ MeasurableSet sᶜ ∧ ∀ (i : ι), MeasurableSet (sᶜ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})

Tactic:
refine ⟨hs.1.compl, fun i ↦ ?_⟩
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : ι
rw : MeasurableSet ((sᶜ ∪ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ) ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
rw₁ :
  sᶜ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} = (sᶜ ∪ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ) ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
⊢ MeasurableSet (sᶜ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})

Tactic:
rw [(_ : sᶜ ∩ {ω | τ ω ≤ i} = (sᶜ ∪ {ω | τ ω ≤ i}ᶜ) ∩ {ω | τ ω ≤ i})]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : ι
⊢ MeasurableSet ((sᶜ ∪ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ) ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})

Tactic:
MeasurableSet.inter ?_ ?_

Premises used: MeasurableSet.inter
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : ι
refine_1 : MeasurableSet (sᶜ ∪ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ)
refine_2 : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
⊢ MeasurableSet ((sᶜ ∪ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ) ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})

Tactic:
refine MeasurableSet.inter ?_ ?_

Premises used: MeasurableSet.inter
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : ι
refine_1 : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})ᶜ
⊢ MeasurableSet (sᶜ ∪ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ)

Tactic:
rw [← Set.compl_inter]

Premises used: Set.compl_inter
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : ι
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})ᶜ

Tactic:
(hs.2 i).compl

Premises used: MeasurableSet.compl, And.right
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : ι
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})ᶜ

Tactic:
exact (hs.2 i).compl

Premises used: MeasurableSet.compl, And.right
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}

Tactic:
hτ i
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}

Tactic:
exact hτ i
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : ι
rw :
  sᶜ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} =
    sᶜ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∪ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
⊢ sᶜ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} = (sᶜ ∪ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ) ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}

Tactic:
rw [Set.union_inter_distrib_right]

Premises used: Set.union_inter_distrib_right
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : ι
⊢ sᶜ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} =
    sᶜ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∪ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}

Tactic:
simp only [Set.compl_inter_self, Set.union_empty]

Premises used: Set.union_empty, Set.compl_inter_self
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : ℕ → Set Ω
hs : ∀ (i : ℕ), MeasurableSet (s i) ∧ ∀ (i_1 : ι), MeasurableSet (s i ∩ {ω : Ω | τ ω ≤ (↑i_1 : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) (⋃ (i : ℕ), s i) ∧
    ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) ((⋃ (i : ℕ), s i) ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})

Tactic:
⟨MeasurableSet.iUnion fun i ↦ (hs i).1, fun i ↦ ?_⟩

Premises used: And.left, And.intro, MeasurableSet.iUnion
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : ℕ → Set Ω
hs : ∀ (i : ℕ), MeasurableSet (s i) ∧ ∀ (i_1 : ι), MeasurableSet (s i ∩ {ω : Ω | τ ω ≤ (↑i_1 : WithTop ι)})
refine : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) ((⋃ (i : ℕ), s i) ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) (⋃ (i : ℕ), s i) ∧
    ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) ((⋃ (i : ℕ), s i) ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})

Tactic:
refine ⟨MeasurableSet.iUnion fun i ↦ (hs i).1, fun i ↦ ?_⟩
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : ℕ → Set Ω
hs : ∀ (i : ℕ), MeasurableSet (s i) ∧ ∀ (i_1 : ι), MeasurableSet (s i ∩ {ω : Ω | τ ω ≤ (↑i_1 : WithTop ι)})
i : ι
⊢ ∀ (i : ℕ) (i_1 : ι), MeasurableSet (s i ∩ {ω : Ω | τ ω ≤ (↑i_1 : WithTop ι)})

Tactic:
replace hs := fun i ↦ (hs i).2
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : ℕ → Set Ω
i : ι
hs : ∀ (i : ℕ) (i_1 : ι), MeasurableSet (s i ∩ {ω : Ω | τ ω ≤ (↑i_1 : WithTop ι)})
⊢ ∀ (b : ι) (a : ℕ), MeasurableSet (s a ∩ {ω : Ω | τ ω ≤ (↑b : WithTop ι)})

Tactic:
rw [forall_comm] at hs

Premises used: forall_comm
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : ℕ → Set Ω
i : ι
hs : ∀ (b : ι) (a : ℕ), MeasurableSet (s a ∩ {ω : Ω | τ ω ≤ (↑b : WithTop ι)})
rw : MeasurableSet.{u_1} (α := Ω) (⋃ (i_1 : ℕ), s i_1 ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) ((⋃ (i : ℕ), s i) ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})

Tactic:
rw [Set.iUnion_inter]

Premises used: Set.iUnion_inter
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : ℕ → Set Ω
i : ι
hs : ∀ (b : ι) (a : ℕ), MeasurableSet (s a ∩ {ω : Ω | τ ω ≤ (↑b : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) (⋃ (i_1 : ℕ), s i_1 ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})

Tactic:
MeasurableSet.iUnion (hs i)

Premises used: MeasurableSet.iUnion
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : ℕ → Set Ω
i : ι
hs : ∀ (b : ι) (a : ℕ), MeasurableSet (s a ∩ {ω : Ω | τ ω ≤ (↑b : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) (⋃ (i_1 : ℕ), s i_1 ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})

Tactic:
exact MeasurableSet.iUnion (hs i)

Premises used: MeasurableSet.iUnion
-- 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 Ω
⊢ MeasurableSet s ↔ MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})

Tactic:
Iff.rfl

Premises used: MeasurableSet, Iff.rfl
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
⊢ hτ.measurableSpace ≤ hπ.measurableSpace

Tactic:
fun s hs ↦ ⟨hs.1, fun i ↦ ?_⟩

Premises used: MeasurableSet, And.left, And.intro
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
refine : ∀ (s : Set Ω) (hs : MeasurableSet s) (i : ι), MeasurableSet (s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)})
⊢ hτ.measurableSpace ≤ hπ.measurableSpace

Tactic:
refine fun s hs ↦ ⟨hs.1, fun i ↦ ?_⟩
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
s : Set Ω
hs : MeasurableSet s
i : ι
rw : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)})
rw₁ : s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)} = s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)}
⊢ MeasurableSet (s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)})

Tactic:
rw [(_ : s ∩ {ω | π ω ≤ i} = s ∩ {ω | τ ω ≤ i} ∩ {ω | π ω ≤ i})]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
s : Set Ω
hs : MeasurableSet s
i : ι
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)})

Tactic:
(hs.2 i).inter (hπ i)

Premises used: And.right, MeasurableSet.inter
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
s : Set Ω
hs : MeasurableSet s
i : ι
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)})

Tactic:
exact (hs.2 i).inter (hπ i)

Premises used: And.right, MeasurableSet.inter
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
s : Set Ω
hs : MeasurableSet s
i : ι
h :
  ∀ (x : Ω),
    x ∈ s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)} ↔
      x ∈ s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)}
⊢ s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)} = s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)}

Tactic:
ext
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
s : Set Ω
hs : MeasurableSet s
i : ι
x : Ω
h : π x ≤ (↑i : WithTop ι) → x ∈ s → τ x ≤ (↑i : WithTop ι)
⊢ x ∈ s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)} ↔ x ∈ s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)}

Tactic:
simp only [Set.mem_inter_iff, iff_self_and, and_congr_left_iff, Set.mem_setOf_eq]

Premises used: Set.mem_inter_iff, iff_self_and, Set.mem_setOf_eq, and_congr_left_iff
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
s : Set Ω
hs : MeasurableSet s
i : ι
x : Ω
hle' : π x ≤ (↑i : WithTop ι)
h : x ∈ s → τ x ≤ (↑i : WithTop ι)
⊢ x ∈ s → τ x ≤ (↑i : WithTop ι)

Tactic:
_
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
s : Set Ω
hs : MeasurableSet s
i : ι
x : Ω
hle' : π x ≤ (↑i : WithTop ι)
h : x ∈ s
⊢ τ x ≤ (↑i : WithTop ι)

Tactic:
le_trans (hle _) hle'

Premises used: 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 τ
hπ : IsStoppingTime f π
hle : τ ≤ π
s : Set Ω
hs : MeasurableSet s
i : ι
x : Ω
hle' : π x ≤ (↑i : WithTop ι)
h : x ∈ s
⊢ τ x ≤ (↑i : WithTop ι)

Tactic:
exact le_trans (hle _) hle'

Premises used: 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 τ
⊢ hτ.measurableSpace ≤ m

Tactic:
fun _ hs ↦ hs.1

Premises used: And.left
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
i : ι
h : ∀ (s : Set Ω), MeasurableSet s ↔ MeasurableSet s
⊢ ⋯.measurableSpace = (↑f : ι → MeasurableSpace Ω) i

Tactic:
ext1 s
-- 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 ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑i_1 : WithTop ι)})) → MeasurableSet s
h₁ :
  MeasurableSet s → MeasurableSet s ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑i_1 : WithTop ι)})
⊢ (MeasurableSet s ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑i_1 : WithTop ι)})) ↔ MeasurableSet s

Tactic:
constructor
-- 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 ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑i_1 : WithTop ι)})
⊢ MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑i : WithTop ι)})

Tactic:
have h' := h.2 i
-- 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 ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑i_1 : WithTop ι)})
h' : MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑i : WithTop ι)})
⊢ MeasurableSet s

Tactic:
simpa only [le_refl, Set.setOf_true, Set.inter_univ] using h'

Premises used: le_refl, 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
i : ι
s : Set Ω
h : MeasurableSet s
⊢ MeasurableSet s ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑i_1 : WithTop ι)})

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

Premises used: And.intro, MeasureTheory.Filtration.le
-- 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
h₁ : ∀ (j : ι), MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)})
⊢ MeasurableSet s ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑i_1 : 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
i : ι
s : Set Ω
h : MeasurableSet s
j : ι
pos : ∀ (hij : i ≤ j), MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)})
neg : ∀ (hij : ¬i ≤ j), MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)})
⊢ MeasurableSet (s ∩ {ω : Ω | (↑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
i : ι
s : Set Ω
h : MeasurableSet s
j : ι
hij : i ≤ j
pos : MeasurableSet (s ∩ {ω : Ω | i ≤ j})
⊢ MeasurableSet (s ∩ {ω : Ω | (↑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
i : ι
s : Set Ω
h : MeasurableSet s
j : ι
hij : i ≤ j
pos : MeasurableSet s
⊢ MeasurableSet (s ∩ {ω : Ω | 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
i : ι
s : Set Ω
h : MeasurableSet s
j : ι
hij : i ≤ j
⊢ MeasurableSet s

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
i : ι
s : Set Ω
h : MeasurableSet s
j : ι
hij : i ≤ j
⊢ MeasurableSet s

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
i : ι
s : Set Ω
h : MeasurableSet s
j : ι
hij : ¬i ≤ j
neg : MeasurableSet (s ∩ {ω : Ω | i ≤ j})
⊢ MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)})

Tactic:
norm_cast