awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : SecondCountableTopology ι
hτ : IsStoppingTime f τ
⊢ Measurable τ

Tactic:
hτ.measurable.mono (measurableSpace_le hτ) le_rfl

Premises used: le_rfl, MeasureTheory.IsStoppingTime.measurable, MeasureTheory.IsStoppingTime.measurableSpace_le, Measurable.mono
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : SecondCountableTopology ι
hτ : IsStoppingTime f τ
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = ⊤}

Tactic:
(measurableSet_singleton _).preimage hτ.measurable'

Premises used: MeasurableSet.preimage, MeasurableSingletonClass.measurableSet_singleton, Set.Mem, setOf, MeasureTheory.IsStoppingTime.measurable', Set.preimage, Set.singleton
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : SecondCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑i : WithTop ι)
⊢ Measurable τ

Tactic:
hτ.measurable.mono (measurableSpace_le_of_le_const _ hτ_le) le_rfl

Premises used: le_rfl, MeasureTheory.IsStoppingTime.measurableSpace_le_of_le_const, MeasureTheory.IsStoppingTime.measurable, Measurable.mono
-- 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 π
⊢ ⋯.measurableSpace = hτ.measurableSpace ⊓ hπ.measurableSpace

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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 π
refine_1 : ⋯.measurableSpace ≤ hτ.measurableSpace ⊓ hπ.measurableSpace
refine_2 : hτ.measurableSpace ⊓ hπ.measurableSpace ≤ ⋯.measurableSpace
⊢ ⋯.measurableSpace = hτ.measurableSpace ⊓ hπ.measurableSpace

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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 π
⊢ ⋯.measurableSpace ≤ hτ.measurableSpace ⊓ hπ.measurableSpace

Tactic:
le_inf (measurableSpace_mono _ hτ fun _ => min_le_left _ _)
      (measurableSpace_mono _ hπ fun _ => min_le_right _ _)

Premises used: MeasureTheory.IsStoppingTime.measurableSpace_mono, le_inf, min_le_left, min_le_right
-- 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 π
⊢ ⋯.measurableSpace ≤ hτ.measurableSpace ⊓ hπ.measurableSpace

Tactic:
exact le_inf (measurableSpace_mono _ hτ fun _ => min_le_left _ _)
      (measurableSpace_mono _ hπ fun _ => min_le_right _ _)

Premises used: MeasureTheory.IsStoppingTime.measurableSpace_mono, le_inf, min_le_left, min_le_right
-- 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 π
s : Set Ω
i : WithTop ι
h :
  ∀ (ω : Ω),
    Membership.mem (γ := Set Ω) {ω : Ω | min (τ ω) (π ω) ≤ i} ω ↔
      Membership.mem (γ := Set Ω) ({ω : Ω | τ ω ≤ i} ∪ {ω : Ω | π ω ≤ i}) ω
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | min (τ ω) (π ω) ≤ i} ({ω : Ω | τ ω ≤ i} ∪ {ω : Ω | π ω ≤ i})

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

Tactic:
simp
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
⊢ ∀ (i : WithTop ι), Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | min (τ ω) (π ω) ≤ i} ({ω : Ω | τ ω ≤ i} ∪ {ω : Ω | π ω ≤ i})

Tactic:
have : ∀ i, {ω | min (τ ω) (π ω) ≤ i} = {ω | τ ω ≤ i} ∪ {ω | π ω ≤ i} := by
      intro i; 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 τ
hπ : IsStoppingTime f π
s : Set Ω
this :
  ∀ (i : WithTop ι), Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | min (τ ω) (π ω) ≤ i} ({ω : Ω | τ ω ≤ i} ∪ {ω : Ω | π ω ≤ i})
refine_2 :
  ((MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})) ∧
      MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)})) →
    MeasurableSet s ∧
      ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∪ s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)})
⊢ ((MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})) ∧
      MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)})) →
    MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | min (τ ω) (π ω) ≤ (↑i : WithTop ι)})

Tactic:
simp_rw [this, Set.inter_union_distrib_left]

Premises used: Set.inter_union_distrib_left
-- 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 π
s : Set Ω
this :
  ∀ (i : WithTop ι), Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | min (τ ω) (π ω) ≤ i} ({ω : Ω | τ ω ≤ i} ∪ {ω : Ω | π ω ≤ i})
⊢ ((MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})) ∧
      MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)})) →
    MeasurableSet s ∧
      ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∪ s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)})

Tactic:
fun h ↦ ⟨h.1.1, fun i ↦ (h.left.2 i).union (h.right.2 i)⟩

Premises used: And.right, And.left, And.intro, 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 π
s : Set Ω
this :
  ∀ (i : WithTop ι), Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | min (τ ω) (π ω) ≤ i} ({ω : Ω | τ ω ≤ i} ∪ {ω : Ω | π ω ≤ i})
⊢ ((MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})) ∧
      MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)})) →
    MeasurableSet s ∧
      ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∪ s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)})

Tactic:
exact fun h ↦ ⟨h.1.1, fun i ↦ (h.left.2 i).union (h.right.2 i)⟩
-- 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 π
s : Set Ω
rw : MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s
⊢ MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s

Tactic:
rw [measurableSpace_min hτ hπ]

Premises used: MeasureTheory.IsStoppingTime.measurableSpace_min
-- 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 π
s : Set Ω
⊢ MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s

Tactic:
rfl
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
rw : hτ.measurableSpace ⊓ ⋯.measurableSpace = hτ.measurableSpace ⊓ (↑f : ι → MeasurableSpace Ω) i
rw₁ rw₂ : hτ.measurableSpace ⊓ (↑f : ι → MeasurableSpace Ω) i = hτ.measurableSpace ⊓ (↑f : ι → MeasurableSpace Ω) i
⊢ ⋯.measurableSpace = hτ.measurableSpace ⊓ (↑f : ι → MeasurableSpace Ω) i

Tactic:
rw [hτ.measurableSpace_min (isStoppingTime_const _ i), measurableSpace_const]

Premises used: MeasureTheory.IsStoppingTime.measurableSpace_min, MeasureTheory.isStoppingTime_const, MeasureTheory.IsStoppingTime.measurableSpace_const
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
rw : MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s
⊢ MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s

Tactic:
rw [measurableSpace_min_const hτ]

Premises used: MeasureTheory.IsStoppingTime.measurableSpace_min_const
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
⊢ MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s

Tactic:
apply MeasurableSpace.measurableSet_inf

Premises used: MeasurableSpace.measurableSet_inf
-- 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 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})

Tactic:
simp_rw [IsStoppingTime.measurableSet] at hs ⊢

Premises used: MeasureTheory.IsStoppingTime.measurableSet
-- 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 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : WithTop ι
h :
  ∀ (ω : Ω),
    ω ∈ s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ↔
      ω ∈ s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
⊢ s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} =
    s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}

Tactic:
ext ω
-- 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 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : WithTop ι
ω : Ω
pos :
  ∀ (hτi : τ ω ≤ i),
    ω ∈ s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ↔
      ω ∈ s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
neg :
  ∀ (hτi : ¬τ ω ≤ i),
    ω ∈ s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ↔
      ω ∈ s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
⊢ ω ∈ s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ↔
    ω ∈ s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}

Tactic:
by_cases hτi : τ ω ≤ i
-- 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 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : WithTop ι
ω : Ω
hτi : τ ω ≤ i
⊢ ω ∈ s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ↔
    ω ∈ s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}

Tactic:
grind
-- 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 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : WithTop ι
ω : Ω
hτi : ¬τ ω ≤ i
⊢ ω ∈ s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ↔
    ω ∈ s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}

Tactic:
grind
-- 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 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
⊢ ∀ (i : WithTop ι),
    s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} =
      s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}

Tactic:
have h_eq i : s ∩ {ω | τ ω ≤ π ω} ∩ {ω | min (τ ω) (π ω) ≤ i} =
      s ∩ {ω | τ ω ≤ i} ∩ {ω | min (τ ω) (π ω) ≤ i} ∩
        {ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i} := by
    ext ω
    by_cases hτi : τ ω ≤ i <;> grind
-- 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 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
h_eq :
  ∀ (i : WithTop ι),
    s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} =
      s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
simp_rw :
  MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω}) ∧
    ∀ (i : ι),
      MeasurableSet
        (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | min (τ ω) (π ω) ≤ (↑i : WithTop ι)} ∩
          {ω : Ω | min (τ ω) (↑i : WithTop ι) ≤ min (min (τ ω) (π ω)) (↑i : WithTop ι)})
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω}) ∧
    ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ (↑i : WithTop ι)})

Tactic:
simp_rw [h_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 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
h_eq :
  ∀ (i : WithTop ι),
    s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} =
      s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω}) ∧
    ∀ (i : ι),
      MeasurableSet
        (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | min (τ ω) (π ω) ≤ (↑i : WithTop ι)} ∩
          {ω : Ω | min (τ ω) (↑i : WithTop ι) ≤ min (min (τ ω) (π ω)) (↑i : WithTop ι)})

Tactic:
⟨hs.1.inter (measurableSet_le hτ.measurable' hπ.measurable'), fun i ↦ ?_⟩

Premises used: measurableSet_le, MeasureTheory.IsStoppingTime.measurable', And.left, And.intro, MeasurableSet.inter
-- 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 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
h_eq :
  ∀ (i : WithTop ι),
    s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} =
      s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
refine :
  ∀ (i : ι),
    MeasurableSet
      (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | min (τ ω) (π ω) ≤ (↑i : WithTop ι)} ∩
        {ω : Ω | min (τ ω) (↑i : WithTop ι) ≤ min (min (τ ω) (π ω)) (↑i : WithTop ι)})
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω}) ∧
    ∀ (i : ι),
      MeasurableSet
        (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | min (τ ω) (π ω) ≤ (↑i : WithTop ι)} ∩
          {ω : Ω | min (τ ω) (↑i : WithTop ι) ≤ min (min (τ ω) (π ω)) (↑i : WithTop ι)})

Tactic:
refine ⟨hs.1.inter (measurableSet_le hτ.measurable' hπ.measurable'), fun i ↦ ?_⟩
-- 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 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
h_eq :
  ∀ (i : WithTop ι),
    s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} =
      s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
i : ι
⊢ MeasurableSet
    (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | min (τ ω) (π ω) ≤ (↑i : WithTop ι)} ∩
      {ω : Ω | min (τ ω) (↑i : WithTop ι) ≤ min (min (τ ω) (π ω)) (↑i : WithTop ι)})

Tactic:
((hs.2 i).inter ((hτ.min hπ) i)).inter ?_

Premises used: MeasureTheory.IsStoppingTime.min, setOf, And.right, MeasurableSet.inter
-- 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 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
h_eq :
  ∀ (i : WithTop ι),
    s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} =
      s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
i : ι
refine : MeasurableSet.{u_1} (α := Ω) {ω : Ω | min (τ ω) (↑i : WithTop ι) ≤ min (min (τ ω) (π ω)) (↑i : WithTop ι)}
⊢ MeasurableSet
    (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | min (τ ω) (π ω) ≤ (↑i : WithTop ι)} ∩
      {ω : Ω | min (τ ω) (↑i : WithTop ι) ≤ min (min (τ ω) (π ω)) (↑i : WithTop ι)})

Tactic:
refine ((hs.2 i).inter ((hτ.min hπ) i)).inter ?_

Premises used: MeasureTheory.IsStoppingTime.min, And.right, MeasurableSet.inter
-- 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 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
h_eq :
  ∀ (i : WithTop ι),
    s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} =
      s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
i : ι
apply : Measurable.{u_1, u_3} (β := WithTop ι) fun (a : Ω) ↦ min (τ a) (↑i : WithTop ι)
apply₁ : Measurable.{u_1, u_3} (β := WithTop ι) fun (a : Ω) ↦ min (min (τ a) (π a)) (↑i : WithTop ι)
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | min (τ ω) (↑i : WithTop ι) ≤ min (min (τ ω) (π ω)) (↑i : WithTop ι)}

Tactic:
apply @measurableSet_le _ _ _ _ _ (Filtration.seq f i) _ _ _ _ _ ?_ ?_

Premises used: 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 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
h_eq :
  ∀ (i : WithTop ι),
    s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} =
      s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
i : ι
⊢ Measurable.{u_1, u_3} (β := WithTop ι) fun (a : Ω) ↦ min (τ a) (↑i : WithTop ι)

Tactic:
(hτ.min_const i).measurable_of_le fun _ => min_le_right _ _

Premises used: WithTop.some, MeasureTheory.IsStoppingTime.min_const, min_le_right, MeasureTheory.IsStoppingTime.measurable_of_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 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
h_eq :
  ∀ (i : WithTop ι),
    s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} =
      s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
i : ι
⊢ Measurable.{u_1, u_3} (β := WithTop ι) fun (a : Ω) ↦ min (τ a) (↑i : WithTop ι)

Tactic:
exact (hτ.min_const i).measurable_of_le fun _ => min_le_right _ _

Premises used: WithTop.some, MeasureTheory.IsStoppingTime.min_const, min_le_right, MeasureTheory.IsStoppingTime.measurable_of_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 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
h_eq :
  ∀ (i : WithTop ι),
    s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} =
      s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
i : ι
⊢ Measurable.{u_1, u_3} (β := WithTop ι) fun (a : Ω) ↦ min (min (τ a) (π a)) (↑i : WithTop ι)

Tactic:
((hτ.min hπ).min_const i).measurable_of_le fun _ => min_le_right _ _

Premises used: MeasureTheory.IsStoppingTime.min, WithTop.some, MeasureTheory.IsStoppingTime.min_const, min_le_right, MeasureTheory.IsStoppingTime.measurable_of_le, Min.min
-- 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 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
h_eq :
  ∀ (i : WithTop ι),
    s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} =
      s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
i : ι
⊢ Measurable.{u_1, u_3} (β := WithTop ι) fun (a : Ω) ↦ min (min (τ a) (π a)) (↑i : WithTop ι)

Tactic:
exact ((hτ.min hπ).min_const i).measurable_of_le fun _ => min_le_right _ _

Premises used: MeasureTheory.IsStoppingTime.min, WithTop.some, MeasureTheory.IsStoppingTime.min_const, min_le_right, MeasureTheory.IsStoppingTime.measurable_of_le, Min.min
-- 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 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
mp : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω}) → MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})
mpr : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω}) → MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω}) ↔ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})

Tactic:
constructor