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 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
h : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})
rw : s ∩ {ω : Ω | τ ω ≤ π ω} = s ∩ ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ π ω})
rw₁ rw₂ : s ∩ {ω : Ω | τ ω ≤ π ω} = s ∩ {ω : Ω | τ ω ≤ π ω}
⊢ s ∩ {ω : Ω | τ ω ≤ π ω} = s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ π ω}

Tactic:
rw [Set.inter_assoc, Set.inter_self]

Premises used: Set.inter_self, Set.inter_assoc
-- 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 Ω
h : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})
⊢ s ∩ {ω : Ω | τ ω ≤ π ω} = s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ π ω}

Tactic:
have : s ∩ {ω | τ ω ≤ π ω} = s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ π ω} := by
      rw [Set.inter_assoc, Set.inter_self]
-- 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 Ω
h : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})
this : s ∩ {ω : Ω | τ ω ≤ π ω} = s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ π ω}
mp : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ π ω})
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})

Tactic:
rw [this]
-- 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 Ω
h : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})
this : s ∩ {ω : Ω | τ ω ≤ π ω} = s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ π ω}
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ π ω})

Tactic:
measurableSet_inter_le _ hπ _ h

Premises used: MeasureTheory.IsStoppingTime.measurableSet_inter_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 Ω
h : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})
this : s ∩ {ω : Ω | τ ω ≤ π ω} = s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ π ω}
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ π ω})

Tactic:
exact measurableSet_inter_le _ hπ _ h

Premises used: MeasureTheory.IsStoppingTime.measurableSet_inter_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 Ω
h : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω}) ∧ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})

Tactic:
rw [measurableSet_min_iff hτ hπ] at h

Premises used: MeasureTheory.IsStoppingTime.measurableSet_min_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 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
h : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω}) ∧ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})

Tactic:
h.1

Premises used: And.left
-- 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 Ω
h : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω}) ∧ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})

Tactic:
exact h.1

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

Tactic:
rw [IsStoppingTime.measurableSet_min_iff hτ (isStoppingTime_const _ i),
    IsStoppingTime.measurableSpace_const, IsStoppingTime.measurableSet]

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

Tactic:
⟨fun h => ⟨h, ?_⟩, fun h ↦ h.1⟩

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

Tactic:
refine ⟨fun h => ⟨h, ?_⟩, fun h ↦ h.1⟩
-- 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 : ι
h :
  MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}) ∧
    ∀ (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 : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
h :
  MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}) ∧
    ∀ (i_1 : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑i_1 : WithTop ι)})
h' : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
rwa :
  ∀ (h' : MeasurableSet (s ∩ ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}))),
    MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (h' : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})

Tactic:
rwa [Set.inter_assoc, Set.inter_self] at h'

Premises used: Set.inter_self, Set.inter_assoc
-- 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 π
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ π ω} ∧
    ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})

Tactic:
⟨measurableSet_le hτ.measurable' hπ.measurable', fun j ↦ ?_⟩

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

Tactic:
refine ⟨measurableSet_le hτ.measurable' hπ.measurable', fun j ↦ ?_⟩
-- 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 π
j : ι
h :
  ∀ (x : Ω),
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)}) x ↔
      Membership.mem (γ := Set Ω)
        ({ω : Ω | min (τ ω) (↑j : WithTop ι) ≤ min (π ω) (↑j : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)}) x
⊢ Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
    ({ω : Ω | min (τ ω) (↑j : WithTop ι) ≤ min (π ω) (↑j : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})

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 π
j : ι
x : Ω
⊢ Membership.mem (γ := Set Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)}) x ↔
    Membership.mem (γ := Set Ω)
      ({ω : Ω | min (τ ω) (↑j : WithTop ι) ≤ min (π ω) (↑j : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)}) x

Tactic:
simpa using fun a b ↦ Std.IsPreorder.le_trans _ _ _ a b

Premises used: Std.IsPreorder.le_trans
-- 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 π
j : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
    ({ω : Ω | min (τ ω) (↑j : WithTop ι) ≤ min (π ω) (↑j : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})

Tactic:
have : {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ j} = {ω | min (τ ω) j ≤ min (π ω) j} ∩ {ω | τ ω ≤ j} := by
    ext
    simpa using fun a b ↦ Std.IsPreorder.le_trans _ _ _ a b
-- 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 π
j : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
    ({ω : Ω | min (τ ω) (↑j : WithTop ι) ≤ min (π ω) (↑j : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
rw :
  MeasurableSet.{u_1} (α := Ω)
    ({ω : Ω | min (τ ω) (↑j : WithTop ι) ≤ min (π ω) (↑j : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ (↑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 ι
inst_1 : TopologicalSpace ι
inst_2 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
    ({ω : Ω | min (τ ω) (↑j : WithTop ι) ≤ min (π ω) (↑j : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω)
    ({ω : Ω | min (τ ω) (↑j : WithTop ι) ≤ min (π ω) (↑j : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})

Tactic:
MeasurableSet.inter ?_ (hτ.measurableSet_le j)

Premises used: MeasureTheory.IsStoppingTime.measurableSet_le, 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 π
j : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
    ({ω : Ω | min (τ ω) (↑j : WithTop ι) ≤ min (π ω) (↑j : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
refine : MeasurableSet.{u_1} (α := Ω) {ω : Ω | min (τ ω) (↑j : WithTop ι) ≤ min (π ω) (↑j : WithTop ι)}
⊢ MeasurableSet.{u_1} (α := Ω)
    ({ω : Ω | min (τ ω) (↑j : WithTop ι) ≤ min (π ω) (↑j : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})

Tactic:
refine MeasurableSet.inter ?_ (hτ.measurableSet_le j)

Premises used: MeasureTheory.IsStoppingTime.measurableSet_le, 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 π
j : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
    ({ω : Ω | min (τ ω) (↑j : WithTop ι) ≤ min (π ω) (↑j : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
apply : Measurable.{u_1, u_3} (β := WithTop ι) fun (a : Ω) ↦ min (τ a) (↑j : WithTop ι)
apply₁ : Measurable.{u_1, u_3} (β := WithTop ι) fun (a : Ω) ↦ min (π a) (↑j : WithTop ι)
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | min (τ ω) (↑j : WithTop ι) ≤ min (π ω) (↑j : WithTop ι)}

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

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 π
j : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
    ({ω : Ω | min (τ ω) (↑j : WithTop ι) ≤ min (π ω) (↑j : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
⊢ Measurable.{u_1, u_3} (β := WithTop ι) fun (a : Ω) ↦ min (τ a) (↑j : WithTop ι)

Tactic:
(hτ.min_const j).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 π
j : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
    ({ω : Ω | min (τ ω) (↑j : WithTop ι) ≤ min (π ω) (↑j : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
⊢ Measurable.{u_1, u_3} (β := WithTop ι) fun (a : Ω) ↦ min (τ a) (↑j : WithTop ι)

Tactic:
exact (hτ.min_const j).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 π
j : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
    ({ω : Ω | min (τ ω) (↑j : WithTop ι) ≤ min (π ω) (↑j : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
⊢ Measurable.{u_1, u_3} (β := WithTop ι) fun (a : Ω) ↦ min (π a) (↑j : WithTop ι)

Tactic:
(hπ.min_const j).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 π
j : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
    ({ω : Ω | min (τ ω) (↑j : WithTop ι) ≤ min (π ω) (↑j : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
⊢ Measurable.{u_1, u_3} (β := WithTop ι) fun (a : Ω) ↦ min (π a) (↑j : WithTop ι)

Tactic:
exact (hπ.min_const j).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 π
rw : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ π ω}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ π ω}

Tactic:
rw [← Set.univ_inter {ω : Ω | τ ω ≤ π ω}, ← hτ.measurableSet_inter_le_iff hπ, Set.univ_inter]

Premises used: MeasureTheory.IsStoppingTime.measurableSet_inter_le_iff, setOf, LE.le, Set.univ_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 π
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ π ω}

Tactic:
measurableSet_le_stopping_time hτ hπ

Premises used: MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time
-- 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 π
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ π ω}

Tactic:
exact measurableSet_le_stopping_time hτ hπ

Premises used: MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time
-- 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 π
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ π ω}

Tactic:
have : MeasurableSet[(hτ.min hπ).measurableSpace] {ω | τ ω ≤ π ω} :=
    measurableSet_stopping_time_le_min hτ hπ
-- 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 π
this : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ π ω}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ π ω} ∧ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ π ω}

Tactic:
rw [measurableSet_min_iff hτ hπ] at this

Premises used: MeasureTheory.IsStoppingTime.measurableSet_min_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 : SecondCountableTopology ι
inst_3 : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
this : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ π ω} ∧ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ π ω}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ π ω}

Tactic:
this.2

Premises used: And.right
-- 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 π
this : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ π ω} ∧ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ π ω}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ π ω}

Tactic:
exact this.2

Premises used: And.right
-- 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 τ
hπ : IsStoppingTime f π
h :
  ∀ (x : Ω),
    Membership.mem (γ := Set Ω) {ω : Ω | τ ω = π ω} x ↔
      Membership.mem (γ := Set Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | π ω ≤ τ ω}) x
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = π ω} ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | π ω ≤ τ ω})

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 : OrderTopology ι
inst_3 : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
x : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | τ ω = π ω} x ↔
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | π ω ≤ τ ω}) x

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

Premises used: Set.mem_inter_iff, Set.mem_setOf_eq, le_antisymm_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 : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = π ω} ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | π ω ≤ τ ω})

Tactic:
have : {ω | τ ω = π ω} = {ω | τ ω ≤ π ω} ∩ {ω | π ω ≤ τ ω} := by
    ext; simp only [Set.mem_setOf_eq, le_antisymm_iff, Set.mem_inter_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 : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = π ω} ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | π ω ≤ τ ω})
rw : MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | π ω ≤ τ ω})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = π ω}

Tactic:
rw [this]