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 ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ι
simp_rw : MeasurableSet.{u_1} (α := Ω) ({a : Ω | τ a ≤ (↑i : WithTop ι)} ∩ {a : Ω | π a ≤ (↑i : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (fun (ω : Ω) ↦ max (τ ω) (π ω)) ω ≤ (↑i : WithTop ι)}

Tactic:
simp_rw [max_le_iff, Set.setOf_and]

Premises used: Set.setOf_and, max_le_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π : IsStoppingTime f π
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) ({a : Ω | τ a ≤ (↑i : WithTop ι)} ∩ {a : Ω | π a ≤ (↑i : WithTop ι)})

Tactic:
(hτ i).inter (hπ i)

Premises used: setOf, MeasurableSet.inter
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) ({a : Ω | τ a ≤ (↑i : WithTop ι)} ∩ {a : Ω | π a ≤ (↑i : WithTop ι)})

Tactic:
exact (hτ i).inter (hπ i)

Premises used: MeasurableSet.inter
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
⊢ IsStoppingTime f fun (ω : Ω) ↦ max (τ ω) (↑i : WithTop ι)

Tactic:
hτ.max (isStoppingTime_const f i)

Premises used: MeasureTheory.isStoppingTime_const, MeasureTheory.IsStoppingTime.max
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ι
simp_rw : MeasurableSet.{u_1} (α := Ω) ({a : Ω | τ a ≤ (↑i : WithTop ι)} ∪ {a : Ω | π a ≤ (↑i : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (fun (ω : Ω) ↦ min (τ ω) (π ω)) ω ≤ (↑i : WithTop ι)}

Tactic:
simp_rw [min_le_iff, Set.setOf_or]

Premises used: min_le_iff, Set.setOf_or
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) ({a : Ω | τ a ≤ (↑i : WithTop ι)} ∪ {a : Ω | π a ≤ (↑i : WithTop ι)})

Tactic:
(hτ i).union (hπ i)

Premises used: setOf, MeasurableSet.union
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) ({a : Ω | τ a ≤ (↑i : WithTop ι)} ∪ {a : Ω | π a ≤ (↑i : WithTop ι)})

Tactic:
exact (hτ i).union (hπ i)

Premises used: MeasurableSet.union
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
⊢ IsStoppingTime f fun (ω : Ω) ↦ min (τ ω) (↑i : WithTop ι)

Tactic:
hτ.min (isStoppingTime_const f i)

Premises used: MeasureTheory.IsStoppingTime.min, MeasureTheory.isStoppingTime_const
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : DenselyOrdered ι
inst_4 : FirstCountableTopology ι
inst_5 : NoMaxOrder ι
κ : Type u_4
f : Filtration ι m
τ : κ → Ω → WithTop ι
s : Set κ
hs : s.Countable
inst_6 : f.IsRightContinuous
hτ : ∀ n ∈ s, IsStoppingTime f (τ n)
⊢ IsStoppingTime f fun (ω : Ω) ↦ ⨅ n ∈ s, τ n ω

Tactic:
isStoppingTime_of_measurableSet_lt_of_isRightContinuous <|
    fun i ↦ MeasurableSet.of_compl ?_

Premises used: MeasurableSet.of_compl, MeasureTheory.isStoppingTime_of_measurableSet_lt_of_isRightContinuous
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : DenselyOrdered ι
inst_4 : FirstCountableTopology ι
inst_5 : NoMaxOrder ι
κ : Type u_4
f : Filtration ι m
τ : κ → Ω → WithTop ι
s : Set κ
hs : s.Countable
inst_6 : f.IsRightContinuous
hτ : ∀ n ∈ s, IsStoppingTime f (τ n)
refine : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | ⨅ n ∈ s, τ n ω < (↑i : WithTop ι)}ᶜ
⊢ IsStoppingTime f fun (ω : Ω) ↦ ⨅ n ∈ s, τ n ω

Tactic:
refine isStoppingTime_of_measurableSet_lt_of_isRightContinuous <|
    fun i ↦ MeasurableSet.of_compl ?_

Premises used: MeasurableSet.of_compl, MeasureTheory.isStoppingTime_of_measurableSet_lt_of_isRightContinuous
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : DenselyOrdered ι
inst_4 : FirstCountableTopology ι
inst_5 : NoMaxOrder ι
κ : Type u_4
f : Filtration ι m
τ : κ → Ω → WithTop ι
s : Set κ
hs : s.Countable
inst_6 : f.IsRightContinuous
hτ : ∀ n ∈ s, IsStoppingTime f (τ n)
i : ι
rw : MeasurableSet.{u_1} (α := Ω) (⋂ n ∈ s, {ω : Ω | (↑i : WithTop ι) ≤ τ n ω})
rw₁ :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | ⨅ n ∈ s, τ n ω < (↑i : WithTop ι)}ᶜ (⋂ n ∈ s, {ω : Ω | (↑i : WithTop ι) ≤ τ n ω})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | ⨅ n ∈ s, τ n ω < (↑i : WithTop ι)}ᶜ

Tactic:
rw [(_ : {ω | ⨅ n ∈ s, τ n ω < i}ᶜ = ⋂ n ∈ s, {ω | i ≤ τ n ω})]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : DenselyOrdered ι
inst_4 : FirstCountableTopology ι
inst_5 : NoMaxOrder ι
κ : Type u_4
f : Filtration ι m
τ : κ → Ω → WithTop ι
s : Set κ
hs : s.Countable
inst_6 : f.IsRightContinuous
hτ : ∀ n ∈ s, IsStoppingTime f (τ n)
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) (⋂ n ∈ s, {ω : Ω | (↑i : WithTop ι) ≤ τ n ω})

Tactic:
MeasurableSet.biInter hs <| fun n hn ↦ (hτ n hn).measurableSet_ge i

Premises used: MeasureTheory.IsStoppingTime.measurableSet_ge, MeasurableSet.biInter
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : DenselyOrdered ι
inst_4 : FirstCountableTopology ι
inst_5 : NoMaxOrder ι
κ : Type u_4
f : Filtration ι m
τ : κ → Ω → WithTop ι
s : Set κ
hs : s.Countable
inst_6 : f.IsRightContinuous
hτ : ∀ n ∈ s, IsStoppingTime f (τ n)
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) (⋂ n ∈ s, {ω : Ω | (↑i : WithTop ι) ≤ τ n ω})

Tactic:
exact MeasurableSet.biInter hs <| fun n hn ↦ (hτ n hn).measurableSet_ge i

Premises used: MeasureTheory.IsStoppingTime.measurableSet_ge, MeasurableSet.biInter
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : DenselyOrdered ι
inst_4 : FirstCountableTopology ι
inst_5 : NoMaxOrder ι
κ : Type u_4
f : Filtration ι m
τ : κ → Ω → WithTop ι
s : Set κ
hs : s.Countable
inst_6 : f.IsRightContinuous
hτ : ∀ n ∈ s, IsStoppingTime f (τ n)
i : ι
h :
  ∀ (ω : Ω),
    Membership.mem (γ := Set Ω) {ω : Ω | ⨅ n ∈ s, τ n ω < (↑i : WithTop ι)}ᶜ ω ↔
      Membership.mem (γ := Set Ω) (⋂ n ∈ s, {ω : Ω | (↑i : WithTop ι) ≤ τ n ω}) ω
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | ⨅ n ∈ s, τ n ω < (↑i : WithTop ι)}ᶜ (⋂ n ∈ s, {ω : Ω | (↑i : WithTop ι) ≤ τ n ω})

Tactic:
ext ω
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : DenselyOrdered ι
inst_4 : FirstCountableTopology ι
inst_5 : NoMaxOrder ι
κ : Type u_4
f : Filtration ι m
τ : κ → Ω → WithTop ι
s : Set κ
hs : s.Countable
inst_6 : f.IsRightContinuous
hτ : ∀ n ∈ s, IsStoppingTime f (τ n)
i : ι
ω : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | ⨅ n ∈ s, τ n ω < (↑i : WithTop ι)}ᶜ ω ↔
    Membership.mem (γ := Set Ω) (⋂ n ∈ s, {ω : Ω | (↑i : WithTop ι) ≤ τ n ω}) ω

Tactic:
simp
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : DenselyOrdered ι
inst_4 : FirstCountableTopology ι
inst_5 : NoMaxOrder ι
κ : Type u_4
inst_6 : Countable κ
f : Filtration ι m
τ : κ → Ω → WithTop ι
inst_7 : f.IsRightContinuous
hτ : ∀ (n : κ), IsStoppingTime f (τ n)
⊢ IsStoppingTime f fun (ω : Ω) ↦ ⨅ (n : κ), ⨅ (_ : Membership.mem (γ := Set κ) Set.univ n), τ n ω

Tactic:
IsStoppingTime.biInf (κ := κ) Set.countable_univ (fun n _ => hτ n)

Premises used: Set.countable_univ, MeasureTheory.IsStoppingTime.biInf
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : DenselyOrdered ι
inst_4 : FirstCountableTopology ι
inst_5 : NoMaxOrder ι
κ : Type u_4
inst_6 : Countable κ
f : Filtration ι m
τ : κ → Ω → WithTop ι
inst_7 : f.IsRightContinuous
hτ : ∀ (n : κ), IsStoppingTime f (τ n)
h :
  ∀ (x : Ω),
    Eq.{u_3 + 1} (α := WithTop ι) (⨅ (n : κ), τ n x) (⨅ (n : κ), ⨅ (_ : Membership.mem (γ := Set κ) Set.univ n), τ n x)
⊢ IsStoppingTime f fun (ω : Ω) ↦ ⨅ (n : κ), τ n ω

Tactic:
convert! IsStoppingTime.biInf (κ := κ) Set.countable_univ (fun n _ => hτ n) using 2

Premises used: Set.countable_univ, MeasureTheory.IsStoppingTime.biInf
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : DenselyOrdered ι
inst_4 : FirstCountableTopology ι
inst_5 : NoMaxOrder ι
κ : Type u_4
inst_6 : Countable κ
f : Filtration ι m
τ : κ → Ω → WithTop ι
inst_7 : f.IsRightContinuous
hτ : ∀ (n : κ), IsStoppingTime f (τ n)
x : Ω
⊢ Eq.{u_3 + 1} (α := WithTop ι) (⨅ (n : κ), τ n x) (⨅ (n : κ), ⨅ (_ : Membership.mem (γ := Set κ) Set.univ n), τ n x)

Tactic:
simp
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : AddGroup ι
inst_1 : Preorder ι
inst_2 : AddRightMono ι
inst_3 : AddLeftMono ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
h :
  ∀ (ω : Ω),
    Membership.mem (γ := Set Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)} ω ↔
      Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑(j - i) : WithTop ι)} ω
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)} {ω : Ω | τ ω ≤ (↑(j - i) : WithTop ι)}

Tactic:
ext ω
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : AddGroup ι
inst_1 : Preorder ι
inst_2 : AddRightMono ι
inst_3 : AddLeftMono ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
ω : Ω
⊢ ⊤ + (↑i : WithTop ι) ≤ (↑j : WithTop ι) ↔ ⊤ ≤ (↑(j - i) : WithTop ι)

Tactic:
simp
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : AddGroup ι
inst_1 : Preorder ι
inst_2 : AddRightMono ι
inst_3 : AddLeftMono ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
ω : Ω
a : ι
h : a + i ≤ j ↔ a ≤ j - i
⊢ (↑a : WithTop ι) + (↑i : WithTop ι) ≤ (↑j : WithTop ι) ↔ (↑a : WithTop ι) ≤ (↑(j - i) : WithTop ι)

Tactic:
norm_cast
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : AddGroup ι
inst_1 : Preorder ι
inst_2 : AddRightMono ι
inst_3 : AddLeftMono ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
ω : Ω
a : ι
⊢ a + i ≤ j ↔ a ≤ j - i

Tactic:
simp_rw [← le_sub_iff_add_le]

Premises used: le_sub_iff_add_le
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : AddGroup ι
inst_1 : Preorder ι
inst_2 : AddRightMono ι
inst_3 : AddLeftMono ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
ω : Ω
h : ∀ (x : WithTop ι), x + (↑i : WithTop ι) ≤ (↑j : WithTop ι) ↔ x ≤ (↑(j - i) : WithTop ι)
⊢ τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι) ↔ τ ω ≤ (↑(j - i) : WithTop ι)

Tactic:
cases τ ω with
    | top => simp
    | coe a => norm_cast; simp_rw [← le_sub_iff_add_le]

Premises used: WithTop.top, le_sub_iff_add_le, WithTop.coe
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : AddGroup ι
inst_1 : Preorder ι
inst_2 : AddRightMono ι
inst_3 : AddLeftMono ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)} {ω : Ω | τ ω ≤ (↑(j - i) : WithTop ι)}

Tactic:
have h_eq : {ω | τ ω + i ≤ j} = {ω | τ ω ≤ j - i} := by
    ext ω
    simp only [Set.mem_setOf_eq, coe_sub]
    cases τ ω with
    | top => simp
    | coe a => norm_cast; simp_rw [← le_sub_iff_add_le]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : AddGroup ι
inst_1 : Preorder ι
inst_2 : AddRightMono ι
inst_3 : AddLeftMono ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
h_eq :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)} {ω : Ω | τ ω ≤ (↑(j - i) : WithTop ι)}
rw : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑(j - i) : WithTop ι)}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)}

Tactic:
rw [h_eq]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : AddGroup ι
inst_1 : Preorder ι
inst_2 : AddRightMono ι
inst_3 : AddLeftMono ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
h_eq :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)} {ω : Ω | τ ω ≤ (↑(j - i) : WithTop ι)}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑(j - i) : WithTop ι)}

Tactic:
f.mono (sub_le_self j hi) _ (hτ (j - i))

Premises used: HSub.hSub, MeasureTheory.Filtration.mono, sub_le_self
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : AddGroup ι
inst_1 : Preorder ι
inst_2 : AddRightMono ι
inst_3 : AddLeftMono ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
h_eq :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)} {ω : Ω | τ ω ≤ (↑(j - i) : WithTop ι)}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑(j - i) : WithTop ι)}

Tactic:
exact f.mono (sub_le_self j hi) _ (hτ (j - i))

Premises used: HSub.hSub, MeasureTheory.Filtration.mono, sub_le_self
-- 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 τ
i j : ι
h :
  ∀ (ω : Ω),
    Membership.mem (γ := Set Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)} ω ↔
      Membership.mem (γ := Set Ω) (⋃ (k : (↑{k : ι | k + i ≤ j} : Type u_3)), {ω : Ω | τ ω = (↑(↑k : ι) : WithTop ι)}) ω
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)}
    (⋃ (k : (↑{k : ι | k + i ≤ j} : Type u_3)), {ω : Ω | τ ω = (↑(↑k : ι) : WithTop ι)})

Tactic:
ext ω
-- 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 τ
i j : ι
ω : Ω
h :
  τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι) ↔
    ∃ (i_1 : (↑{k : ι | k + i ≤ j} : Type u_3)), τ ω = (↑(↑i_1 : ι) : WithTop ι)
⊢ Membership.mem (γ := Set Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)} ω ↔
    Membership.mem (γ := Set Ω) (⋃ (k : (↑{k : ι | k + i ≤ j} : Type u_3)), {ω : Ω | τ ω = (↑(↑k : ι) : WithTop ι)}) ω

Tactic:
simp only [Set.mem_setOf_eq, Set.mem_iUnion]

Premises used: Set.mem_iUnion, Set.mem_setOf_eq
-- 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 τ
i j : ι
ω : Ω
⊢ ⊤ + (↑i : WithTop ι) ≤ (↑j : WithTop ι) ↔ ∃ (i_1 : (↑{k : ι | k + i ≤ j} : Type u_3)), ⊤ = (↑(↑i_1 : ι) : WithTop ι)

Tactic:
simp
-- 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 τ
i j : ι
ω : Ω
a : ι
h : (↑a : WithTop ι) + (↑i : WithTop ι) ≤ (↑j : WithTop ι) ↔ a + i ≤ j
⊢ (↑a : WithTop ι) + (↑i : WithTop ι) ≤ (↑j : WithTop ι) ↔
    ∃ (i_1 : (↑{k : ι | k + i ≤ j} : Type u_3)), (↑a : WithTop ι) = (↑(↑i_1 : ι) : WithTop ι)

Tactic:
simp
-- 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 τ
i j : ι
ω : Ω
a : ι
h h₁ h₂ h₃ : a + i ≤ j ↔ a + i ≤ j
⊢ (↑a : WithTop ι) + (↑i : WithTop ι) ≤ (↑j : WithTop ι) ↔ a + i ≤ j

Tactic:
norm_cast
-- 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 τ
i j : ι
ω : Ω
h :
  ∀ (x : WithTop ι),
    x + (↑i : WithTop ι) ≤ (↑j : WithTop ι) ↔ ∃ (i_1 : (↑{k : ι | k + i ≤ j} : Type u_3)), x = (↑(↑i_1 : ι) : WithTop ι)
⊢ τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι) ↔
    ∃ (i_1 : (↑{k : ι | k + i ≤ j} : Type u_3)), τ ω = (↑(↑i_1 : ι) : WithTop ι)

Tactic:
cases τ ω with
    | top => simp
    | coe a => simp; norm_cast

Premises used: 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 τ
i j : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)}
    (⋃ (k : (↑{k : ι | k + i ≤ j} : Type u_3)), {ω : Ω | τ ω = (↑(↑k : ι) : WithTop ι)})

Tactic:
have h : {ω | τ ω + i ≤ j} = ⋃ k : {k | k + i ≤ j}, {ω | τ ω = k} := by
    ext ω
    simp only [Set.mem_setOf_eq, Set.mem_iUnion]
    cases τ ω with
    | top => simp
    | coe a => simp; norm_cast
-- 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 τ
i j : ι
h :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)}
    (⋃ (k : (↑{k : ι | k + i ≤ j} : Type u_3)), {ω : Ω | τ ω = (↑(↑k : ι) : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (fun (ω : Ω) ↦ τ ω + (↑i : WithTop ι)) ω ≤ (↑j : WithTop ι)}

Tactic:
h ▸ MeasurableSet.iUnion fun k => hτ.measurableSet_eq_le (le_of_add_le_left k.2)

Premises used: setOf, MeasureTheory.IsStoppingTime.measurableSet_eq_le, Eq.rec, le_of_add_le_left, MeasurableSet.iUnion, Eq.symm, Subtype.property
-- 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 τ
i j : ι
h :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)}
    (⋃ (k : (↑{k : ι | k + i ≤ j} : Type u_3)), {ω : Ω | τ ω = (↑(↑k : ι) : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (fun (ω : Ω) ↦ τ ω + (↑i : WithTop ι)) ω ≤ (↑j : WithTop ι)}

Tactic:
exact h ▸ MeasurableSet.iUnion fun k => hτ.measurableSet_eq_le (le_of_add_le_left k.2)
-- 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 :
  ∀ (ω : Ω),
    Membership.mem (γ := Set Ω) {ω : Ω | (τ + π) ω ≤ (↑j : WithTop ι)} ω ↔
      Membership.mem (γ := Set Ω)
        (⋃ (k : (↑(Set.Iic j) : Type u_3)),
          {ω : Ω | π ω = (↑(↑k : ι) : WithTop ι)} ∩ {ω : Ω | τ ω + (↑(↑k : ι) : WithTop ι) ≤ (↑j : WithTop ι)})
        ω
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (τ + π) ω ≤ (↑j : WithTop ι)}
    (⋃ (k : (↑(Set.Iic j) : Type u_3)),
      {ω : Ω | π ω = (↑(↑k : ι) : WithTop ι)} ∩ {ω : Ω | τ ω + (↑(↑k : ι) : WithTop ι) ≤ (↑j : WithTop ι)})

Tactic:
ext ω
-- 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 :
  τ ω + π ω ≤ (↑j : WithTop ι) ↔
    ∃ (i : (↑(Set.Iic j) : Type u_3)), π ω = (↑(↑i : ι) : WithTop ι) ∧ τ ω + (↑(↑i : ι) : WithTop ι) ≤ (↑j : WithTop ι)
⊢ Membership.mem (γ := Set Ω) {ω : Ω | (τ + π) ω ≤ (↑j : WithTop ι)} ω ↔
    Membership.mem (γ := Set Ω)
      (⋃ (k : (↑(Set.Iic j) : Type u_3)),
        {ω : Ω | π ω = (↑(↑k : ι) : WithTop ι)} ∩ {ω : Ω | τ ω + (↑(↑k : ι) : WithTop ι) ≤ (↑j : WithTop ι)})
      ω

Tactic:
simp only [Pi.add_apply, Set.mem_setOf_eq, Set.mem_iUnion, Set.mem_inter_iff]

Premises used: Set.mem_inter_iff, Set.mem_iUnion, Set.mem_setOf_eq, Pi.add_apply
-- 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 : ι
ω : Ω
⊢ ⊤ + π ω ≤ (↑j : WithTop ι) ↔
    ∃ (i : (↑(Set.Iic j) : Type u_3)), π ω = (↑(↑i : ι) : WithTop ι) ∧ ⊤ + (↑(↑i : ι) : WithTop ι) ≤ (↑j : WithTop ι)

Tactic:
simp
-- 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 : ι
⊢ (↑a : WithTop ι) + ⊤ ≤ (↑j : WithTop ι) ↔
    ∃ (i : (↑(Set.Iic j) : Type u_3)),
      ⊤ = (↑(↑i : ι) : WithTop ι) ∧ (↑a : WithTop ι) + (↑(↑i : ι) : WithTop ι) ≤ (↑j : WithTop ι)

Tactic:
simp
-- 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 : ι
h : a + b ≤ j ↔ ∃ (i : (↑(Set.Iic j) : Type u_3)), b = (↑i : ι) ∧ a + (↑i : ι) ≤ j
⊢ (↑a : WithTop ι) + (↑b : WithTop ι) ≤ (↑j : WithTop ι) ↔
    ∃ (i : (↑(Set.Iic j) : Type u_3)),
      (↑b : WithTop ι) = (↑(↑i : ι) : WithTop ι) ∧ (↑a : WithTop ι) + (↑(↑i : ι) : WithTop ι) ≤ (↑j : WithTop ι)

Tactic:
norm_cast