awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : ι
⊢ MeasurableSet (sᶜ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
have rw : MeasurableSet ((sᶜ ∪ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ) ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
Tactic: rw [(_ : sᶜ ∩ {ω | τ ω ≤ i} = (sᶜ ∪ {ω | τ ω ≤ i}ᶜ) ∩ {ω | τ ω ≤ i})]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : ι
rw : MeasurableSet ((sᶜ ∪ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ) ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
⊢ MeasurableSet (sᶜ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
have rw₁ : sᶜ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} = (sᶜ ∪ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ) ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
Tactic: rw [(_ : sᶜ ∩ {ω | τ ω ≤ i} = (sᶜ ∪ {ω | τ ω ≤ i}ᶜ) ∩ {ω | τ ω ≤ i})]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : ι
⊢ MeasurableSet ((sᶜ ∪ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ) ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
have refine_1 : MeasurableSet (sᶜ ∪ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ)
Tactic: refine MeasurableSet.inter ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : ι
refine_1 : MeasurableSet (sᶜ ∪ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ)
⊢ MeasurableSet ((sᶜ ∪ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ) ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
have refine_2 : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
Tactic: refine MeasurableSet.inter ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : ι
⊢ MeasurableSet (sᶜ ∪ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ)
have refine_1 : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})ᶜ
Tactic: rw [← Set.compl_inter]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
hs : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
i : ι
⊢ sᶜ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} = (sᶜ ∪ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ) ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
have rw : sᶜ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} =
  sᶜ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∪ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}ᶜ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
Tactic: rw [Set.union_inter_distrib_right]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : ℕ → Set Ω
hs : ∀ (i : ℕ), MeasurableSet (s i) ∧ ∀ (i_1 : ι), MeasurableSet (s i ∩ {ω : Ω | τ ω ≤ (↑i_1 : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) (⋃ (i : ℕ), s i) ∧
    ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) ((⋃ (i : ℕ), s i) ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
have refine : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) ((⋃ (i : ℕ), s i) ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
Tactic: refine ⟨MeasurableSet.iUnion fun i ↦ (hs i).1, fun i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : ℕ → Set Ω
hs : ∀ (i : ℕ), MeasurableSet (s i) ∧ ∀ (i_1 : ι), MeasurableSet (s i ∩ {ω : Ω | τ ω ≤ (↑i_1 : WithTop ι)})
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) ((⋃ (i : ℕ), s i) ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
have hs₁ : ∀ (i : ℕ) (i_1 : ι), MeasurableSet (s i ∩ {ω : Ω | τ ω ≤ (↑i_1 : WithTop ι)})
Tactic: replace hs := fun i ↦ (hs i).2
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : ℕ → Set Ω
i : ι
hs : ∀ (i : ℕ) (i_1 : ι), MeasurableSet (s i ∩ {ω : Ω | τ ω ≤ (↑i_1 : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) ((⋃ (i : ℕ), s i) ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
have hs₁ : ∀ (b : ι) (a : ℕ), MeasurableSet (s a ∩ {ω : Ω | τ ω ≤ (↑b : WithTop ι)})
Tactic: rw [forall_comm] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : ℕ → Set Ω
i : ι
hs : ∀ (b : ι) (a : ℕ), MeasurableSet (s a ∩ {ω : Ω | τ ω ≤ (↑b : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) ((⋃ (i : ℕ), s i) ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
have rw : MeasurableSet.{u_1} (α := Ω) (⋃ (i_1 : ℕ), s i_1 ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
Tactic: rw [Set.iUnion_inter]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
⊢ hτ.measurableSpace ≤ hπ.measurableSpace
have refine : ∀ (s : Set Ω) (hs : MeasurableSet s) (i : ι), MeasurableSet (s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)})
Tactic: refine fun s hs ↦ ⟨hs.1, fun i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
s : Set Ω
hs : MeasurableSet s
i : ι
⊢ MeasurableSet (s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)})
have rw : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)})
Tactic: rw [(_ : s ∩ {ω | π ω ≤ i} = s ∩ {ω | τ ω ≤ i} ∩ {ω | π ω ≤ i})]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
s : Set Ω
hs : MeasurableSet s
i : ι
rw : MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)})
⊢ MeasurableSet (s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)})
have rw₁ : s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)} = s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)}
Tactic: rw [(_ : s ∩ {ω | π ω ≤ i} = s ∩ {ω | τ ω ≤ i} ∩ {ω | π ω ≤ i})]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
s : Set Ω
hs : MeasurableSet s
i : ι
⊢ s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)} = s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)}
have h : ∀ (x : Ω),
  x ∈ s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)} ↔ x ∈ s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)}
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
s : Set Ω
hs : MeasurableSet s
i : ι
x : Ω
⊢ x ∈ s ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)} ↔ x ∈ s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | π ω ≤ (↑i : WithTop ι)}
have h : π x ≤ (↑i : WithTop ι) → x ∈ s → τ x ≤ (↑i : WithTop ι)
Tactic: simp only [Set.mem_inter_iff, iff_self_and, and_congr_left_iff, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
i : ι
⊢ ⋯.measurableSpace = (↑f : ι → MeasurableSpace Ω) i
have h : ∀ (s : Set Ω), MeasurableSet s ↔ MeasurableSet s
Tactic: ext1 s
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
⊢ (MeasurableSet s ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑i_1 : WithTop ι)})) ↔ MeasurableSet s
have h : (MeasurableSet s ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑i_1 : WithTop ι)})) → MeasurableSet s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h :
  (MeasurableSet s ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑i_1 : WithTop ι)})) → MeasurableSet s
⊢ (MeasurableSet s ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑i_1 : WithTop ι)})) ↔ MeasurableSet s
have h₁ : MeasurableSet s → MeasurableSet s ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑i_1 : WithTop ι)})
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet s ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑i_1 : WithTop ι)})
⊢ MeasurableSet s
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 : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet s
⊢ MeasurableSet s ∧ ∀ (i_1 : ι), MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑i_1 : WithTop ι)})
have h₁ : ∀ (j : ι), MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)})
Tactic: refine ⟨f.le i _ h, fun j ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet s
j : ι
⊢ MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)})
have pos : ∀ (hij : i ≤ j), MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)})
Tactic: by_cases hij : i ≤ j
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet s
j : ι
pos : ∀ (hij : i ≤ j), MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)})
⊢ MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)})
have neg : ∀ (hij : ¬i ≤ j), MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)})
Tactic: by_cases hij : i ≤ j
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet s
j : ι
hij : i ≤ j
⊢ MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)})
have pos : MeasurableSet (s ∩ {ω : Ω | i ≤ j})
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet s
j : ι
hij : i ≤ j
⊢ MeasurableSet (s ∩ {ω : Ω | i ≤ j})
have pos : MeasurableSet s
Tactic: simp only [hij, Set.setOf_true, Set.inter_univ]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet s
j : ι
hij : ¬i ≤ j
⊢ MeasurableSet (s ∩ {ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)})
have neg : MeasurableSet (s ∩ {ω : Ω | i ≤ j})
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
j : WithTop ι
⊢ Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
    ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})
have h : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j}) ω ↔
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j}) ω
Tactic: ext1 ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
j : WithTop ι
ω : Ω
⊢ Membership.mem (γ := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j}) ω ↔
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j}) ω
have h : τ ω = (↑i : WithTop ι) → (τ ω ≤ j ↔ (↑i : WithTop ι) ≤ j)
Tactic: simp only [Set.mem_inter_iff, Set.mem_setOf_eq, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
j : WithTop ι
ω : Ω
hxi : τ ω = (↑i : WithTop ι)
⊢ τ ω ≤ j ↔ (↑i : WithTop ι) ≤ j
have h : (↑i : WithTop ι) ≤ j ↔ (↑i : WithTop ι) ≤ j
Tactic: rw [hxi]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)}) ↔ MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
have this : ∀ (j : WithTop ι),
  Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
    ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})
Tactic: have : ∀ j, {ω : Ω | τ ω = i} ∩ {ω : Ω | τ ω ≤ j} = {ω : Ω | τ ω = i} ∩ {_ω | i ≤ j} := by
    intro j
    ext1 ω
    simp only [Set.mem_inter_iff, Set.mem_setOf_eq, and_congr_right_iff]
    intro hxi
    rw [hxi]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this :
  ∀ (j : WithTop ι),
    Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
      ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)}) ↔ MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
have mp : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)}) → MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this :
  ∀ (j : WithTop ι),
    Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
      ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})
mp : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)}) → MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)}) ↔ MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
have mpr : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)}) → MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this :
  ∀ (j : WithTop ι),
    Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
      ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})
h : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
have mpr : ∀ (j : ι), MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
Tactic: refine ⟨f.le i _ h, fun j ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this :
  ∀ (j : WithTop ι),
    Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
      ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})
h : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
j : ι
⊢ MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
have mpr : MeasurableSet (s ∩ ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)}))
Tactic: rw [Set.inter_assoc, this]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this :
  ∀ (j : WithTop ι),
    Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
      ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})
h : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
j : ι
⊢ MeasurableSet (s ∩ ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)}))
have pos : ∀ (hij : i ≤ j), MeasurableSet (s ∩ ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)}))
Tactic: by_cases hij : i ≤ j
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this :
  ∀ (j : WithTop ι),
    Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
      ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})
h : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
j : ι
pos :
  ∀ (hij : i ≤ j),
    MeasurableSet (s ∩ ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)}))
⊢ MeasurableSet (s ∩ ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)}))
have neg : ∀ (hij : ¬i ≤ j),
  MeasurableSet (s ∩ ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)}))
Tactic: by_cases hij : i ≤ j
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this :
  ∀ (j : WithTop ι),
    Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
      ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})
h : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
j : ι
hij : i ≤ j
⊢ MeasurableSet (s ∩ ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ (↑j : WithTop ι)}))
have pos : MeasurableSet (s ∩ ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | i ≤ j}))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this :
  ∀ (j : WithTop ι),
    Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ j})
      ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | (↑i : WithTop ι) ≤ j})
h : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
j : ι
hij : i ≤ j
⊢ MeasurableSet (s ∩ ({ω : Ω | τ ω = (↑i : WithTop ι)} ∩ {_ω : Ω | i ≤ j}))
have pos : MeasurableSet (s ∩ {ω : Ω | τ ω = (↑i : WithTop ι)})
Tactic: simp only [hij, Set.setOf_true, Set.inter_univ]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι_1 : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst : SemilatticeSup ι
inst_1 : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst_2 : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
refine_1 : MeasurableSpace Ω
⊢ SigmaFinite (μ.trim ⋯)
have refine_2 : (↑f : ι → MeasurableSpace Ω) ⊥ ≤ hτ.measurableSpace
Tactic: refine @sigmaFiniteTrim_mono _ _ ?_ _ _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι_1 : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst : SemilatticeSup ι
inst_1 : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst_2 : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
refine_1 : MeasurableSpace Ω
refine_2 : (↑f : ι → MeasurableSpace Ω) ⊥ ≤ hτ.measurableSpace
⊢ SigmaFinite (μ.trim ⋯)
have refine_3 : SigmaFinite (m0 := (↑f : ι → MeasurableSpace Ω) ⊥) (μ.trim sorry)
Tactic: refine @sigmaFiniteTrim_mono _ _ ?_ _ _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι_1 : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst : SemilatticeSup ι
inst_1 : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst_2 : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
refine_1 : MeasurableSpace Ω
⊢ SigmaFinite (μ.trim ⋯)
have refine_2 : (↑f : ι → MeasurableSpace Ω) ⊥ ≤ hτ.measurableSpace
Tactic: refine @sigmaFiniteTrim_mono _ _ ?_ _ _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι_1 : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst : SemilatticeSup ι
inst_1 : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst_2 : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ (↑n : WithTop ι)
refine_1 : MeasurableSpace Ω
refine_2 : (↑f : ι → MeasurableSpace Ω) ⊥ ≤ hτ.measurableSpace
⊢ SigmaFinite (μ.trim ⋯)
have refine_3 : SigmaFinite (m0 := (↑f : ι → MeasurableSpace Ω) ⊥) (μ.trim sorry)
Tactic: refine @sigmaFiniteTrim_mono _ _ ?_ _ _ _ ?_ ?_
-- 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 τ
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
have refine : ∀ (j : ι), MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
Tactic: refine ⟨f.le i _ (hτ i), 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 ι
hτ : IsStoppingTime f τ
i j : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
    {ω : Ω | τ ω ≤ (↑(min i j) : WithTop ι)}
have h : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)}) ω ↔
    Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑(min i j) : WithTop ι)} ω
Tactic: ext1 ω
-- 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 τ
i j : ι
⊢ MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
have this : Eq.{u_1 + 1} (α := Set Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≤ (↑j : WithTop ι)})
  {ω : Ω | τ ω ≤ (↑(min i j) : WithTop ι)}
Tactic: have : {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | τ ω ≤ j} = {ω : Ω | τ ω ≤ min i j} := by
    ext1 ω
    simp [Set.mem_inter_iff, Set.mem_setOf_eq]