awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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}
⊢ ω ∈ s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ↔
    ω ∈ s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
have neg : ∀ (hτi : ¬τ ω ≤ i),
  ω ∈ s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ↔
    ω ∈ s ∩ {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | min (τ ω) (π ω) ≤ i} ∩ {ω : Ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
Tactic: by_cases hτi : τ ω ≤ i
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
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 ι)})
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω}) ∧
    ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ (↑i : WithTop ι)})
have h_eq : ∀ (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
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | min (τ ω) (π ω) ≤ (↑i : WithTop ι)})
have simp_rw : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω}) ∧
  ∀ (i : ι),
    MeasurableSet
      (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | min (τ ω) (π ω) ≤ (↑i : WithTop ι)} ∩
        {ω : Ω | min (τ ω) (↑i : WithTop ι) ≤ min (min (τ ω) (π ω)) (↑i : WithTop ι)})
Tactic: simp_rw [h_eq]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)})
have refine : ∀ (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 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)})
have refine : MeasurableSet.{u_1} (α := Ω) {ω : Ω | min (τ ω) (↑i : WithTop ι) ≤ min (min (τ ω) (π ω)) (↑i : WithTop ι)}
Tactic: refine ((hs.2 i).inter ((hτ.min hπ) i)).inter ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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.{u_1} (α := Ω) {ω : Ω | min (τ ω) (↑i : WithTop ι) ≤ min (min (τ ω) (π ω)) (↑i : WithTop ι)}
have apply : Measurable.{u_1, u_3} (β := WithTop ι) fun (a : Ω) ↦ min (τ a) (↑i : WithTop ι)
Tactic: apply @measurableSet_le _ _ _ _ _ (Filtration.seq f i) _ _ _ _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | min (τ ω) (↑i : WithTop ι) ≤ min (min (τ ω) (π ω)) (↑i : WithTop ι)}
have apply₁ : Measurable.{u_1, u_3} (β := WithTop ι) fun (a : Ω) ↦ min (min (τ a) (π a)) (↑i : WithTop ι)
Tactic: apply @measurableSet_le _ _ _ _ _ (Filtration.seq f i) _ _ _ _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 Ω
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω}) ↔ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})
have mp : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω}) → MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ∩ {ω : Ω | τ ω ≤ π ω})
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω}) ↔ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})
have mpr : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω}) → MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ π ω}
have rw : s ∩ {ω : Ω | τ ω ≤ π ω} = s ∩ ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ π ω})
Tactic: rw [Set.inter_assoc, Set.inter_self]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ∩ ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ π ω})
⊢ s ∩ {ω : Ω | τ ω ≤ π ω} = s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ π ω}
have rw₁ : s ∩ {ω : Ω | τ ω ≤ π ω} = s ∩ {ω : Ω | τ ω ≤ π ω}
Tactic: rw [Set.inter_assoc, Set.inter_self]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
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 ∩ {ω : Ω | τ ω ≤ π ω})
have this : s ∩ {ω : Ω | τ ω ≤ π ω} = s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ π ω}
Tactic: have : s ∩ {ω | τ ω ≤ π ω} = s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ π ω} := by
      rw [Set.inter_assoc, Set.inter_self]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ∩ {ω : Ω | τ ω ≤ π ω})
have mp : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ π ω})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
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 ∩ {ω : Ω | τ ω ≤ π ω})
have h₁ : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω}) ∧ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})
Tactic: rw [measurableSet_min_iff hτ hπ] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)}) ↔ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
have 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 ι)})
Tactic: rw [IsStoppingTime.measurableSet_min_iff hτ (isStoppingTime_const _ i),
    IsStoppingTime.measurableSpace_const, IsStoppingTime.measurableSet]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)})
have refine : ∀
  (h :
    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⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
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 ι)})
have h' : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
Tactic: have h' := h.2 i
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)})
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
have rwa : ∀ (h' : MeasurableSet (s ∩ ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}))),
  MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
Tactic: rwa [Set.inter_assoc, Set.inter_self] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)})
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
have rwa₁ : ∀ (h' : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
Tactic: rwa [Set.inter_assoc, Set.inter_self] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)})
have refine : ∀ (j : ι), MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
Tactic: refine ⟨measurableSet_le hτ.measurable' hπ.measurable', fun j ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)})
have h : ∀ (x : Ω),
  Membership.mem (γ := Set Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)}) x ↔
    Membership.mem (γ := Set Ω)
      ({ω : Ω | min (τ ω) (↑j : WithTop ι) ≤ min (π ω) (↑j : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
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 : ι
⊢ MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
have this : 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
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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} (α := Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
have rw : MeasurableSet.{u_1} (α := Ω)
  ({ω : Ω | min (τ ω) (↑j : WithTop ι) ≤ min (π ω) (↑j : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)})
have refine : MeasurableSet.{u_1} (α := Ω) {ω : Ω | min (τ ω) (↑j : WithTop ι) ≤ min (π ω) (↑j : WithTop ι)}
Tactic: refine MeasurableSet.inter ?_ (hτ.measurableSet_le j)
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)}
have apply : Measurable.{u_1, u_3} (β := WithTop ι) fun (a : Ω) ↦ min (τ a) (↑j : WithTop ι)
Tactic: apply @measurableSet_le _ _ _ _ _ (Filtration.seq f j) _ _ _ _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 ι)
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | min (τ ω) (↑j : WithTop ι) ≤ min (π ω) (↑j : WithTop ι)}
have apply₁ : Measurable.{u_1, u_3} (β := WithTop ι) fun (a : Ω) ↦ min (π a) (↑j : WithTop ι)
Tactic: apply @measurableSet_le _ _ _ _ _ (Filtration.seq f j) _ _ _ _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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} (α := Ω) {ω : Ω | τ ω ≤ π ω}
have rw : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ π ω}
Tactic: rw [← Set.univ_inter {ω : Ω | τ ω ≤ π ω}, ← hτ.measurableSet_inter_le_iff hπ, Set.univ_inter]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
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} (α := Ω) {ω : Ω | τ ω ≤ π ω}
have this : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ π ω}
Tactic: have : MeasurableSet[(hτ.min hπ).measurableSpace] {ω | τ ω ≤ π ω} :=
    measurableSet_stopping_time_le_min hτ hπ
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
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} (α := Ω) {ω : Ω | τ ω ≤ π ω}
have this₁ : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ π ω} ∧ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ π ω}
Tactic: rw [measurableSet_min_iff hτ hπ] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 Ω) {ω : Ω | τ ω = π ω} ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | π ω ≤ τ ω})
have h : ∀ (x : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | τ ω = π ω} x ↔
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | π ω ≤ τ ω}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
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 π
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = π ω}
have this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = π ω} ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | π ω ≤ τ ω})
Tactic: have : {ω | τ ω = π ω} = {ω | τ ω ≤ π ω} ∩ {ω | π ω ≤ τ ω} := by
    ext; simp only [Set.mem_setOf_eq, le_antisymm_iff, Set.mem_inter_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
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 Ω) {ω : Ω | τ ω = π ω} ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | π ω ≤ τ ω})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = π ω}
have rw : MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | π ω ≤ τ ω})
Tactic: rw [this]