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 : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
h_exists_lt' : ∀ (u : WithTop ι) (hu : (↑t : WithTop ι) < u), ∃ (i : ℕ), (↑(s i) : WithTop ι) < u
h_eq_iInter :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)} (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
h𝓕_eq_iInf : (↑f : ι → MeasurableSpace Ω) t = ⨅ (m_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1)
k : ℕ
x : Ω
⊢ (∀ (i : ℕ), τ x < (↑(s i) : WithTop ι)) ↔ ∀ (i : ℕ) (i_1 : s i ≤ s k), τ x < (↑(s i) : WithTop ι)
have h : ∀ (h : ∀ (i : ℕ) (i_1 : s i ≤ s k), τ x < (↑(s i) : WithTop ι)) (m : ℕ), τ x < (↑(s m) : WithTop ι)
Tactic: refine ⟨fun h m _ ↦ h m, fun h m ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m_1 : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m_1
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
h_exists_lt' : ∀ (u : WithTop ι) (hu : (↑t : WithTop ι) < u), ∃ (i : ℕ), (↑(s i) : WithTop ι) < u
h_eq_iInter :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)} (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
h𝓕_eq_iInf : (↑f : ι → MeasurableSpace Ω) t = ⨅ (m : ℕ), (↑f : ι → MeasurableSpace Ω) (s m)
k : ℕ
x : Ω
h : ∀ (i : ℕ) (i_1 : s i ≤ s k), τ x < (↑(s i) : WithTop ι)
m : ℕ
⊢ τ x < (↑(s m) : WithTop ι)
have h₁ : ∀ (hmk : s m ≤ s k), τ x < (↑(s m) : WithTop ι)
Tactic: rcases le_total (s m) (s k) with hmk | hkm
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m_1 : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m_1
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
h_exists_lt' : ∀ (u : WithTop ι) (hu : (↑t : WithTop ι) < u), ∃ (i : ℕ), (↑(s i) : WithTop ι) < u
h_eq_iInter :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)} (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
h𝓕_eq_iInf : (↑f : ι → MeasurableSpace Ω) t = ⨅ (m : ℕ), (↑f : ι → MeasurableSpace Ω) (s m)
k : ℕ
x : Ω
h : ∀ (i : ℕ) (i_1 : s i ≤ s k), τ x < (↑(s i) : WithTop ι)
m : ℕ
h₁ : ∀ (hmk : s m ≤ s k), τ x < (↑(s m) : WithTop ι)
⊢ τ x < (↑(s m) : WithTop ι)
have h₂ : ∀ (hkm : s k ≤ s m), τ x < (↑(s m) : WithTop ι)
Tactic: rcases le_total (s m) (s k) with hmk | hkm
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
h_exists_lt' : ∀ (u : WithTop ι) (hu : (↑t : WithTop ι) < u), ∃ (i : ℕ), (↑(s i) : WithTop ι) < u
h_eq_iInter :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)} (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
h𝓕_eq_iInf : (↑f : ι → MeasurableSpace Ω) t = ⨅ (m_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1)
k : ℕ
⊢ MeasurableSet.{u_1} (α := Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
have h_eq_k : Eq.{u_1 + 1} (α := Set Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
  (⋂ (m : ℕ), ⋂ (_ : s m ≤ s k), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
Tactic: have h_eq_k : ⋂ m, {ω | τ ω < s m} = ⋂ (m) (hm : s m ≤ s k), {ω | τ ω < s m} := by
    ext x
    simp only [Set.mem_iInter, Set.mem_setOf_eq]
    refine ⟨fun h m _ ↦ h m, fun h m ↦ ?_⟩
    rcases le_total (s m) (s k) with hmk | hkm
    · exact h m hmk
    · exact (h k le_rfl).trans_le (mod_cast hkm)
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
h_exists_lt' : ∀ (u : WithTop ι) (hu : (↑t : WithTop ι) < u), ∃ (i : ℕ), (↑(s i) : WithTop ι) < u
h_eq_iInter :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)} (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
h𝓕_eq_iInf : (↑f : ι → MeasurableSpace Ω) t = ⨅ (m_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1)
k : ℕ
h_eq_k :
  Eq.{u_1 + 1} (α := Set Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
    (⋂ (m : ℕ), ⋂ (_ : s m ≤ s k), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
have neg : MeasurableSet.{u_1} (α := Ω) (⋂ (m : ℕ), ⋂ (_ : s m ≤ s k), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
Tactic: rw [h_eq_k]
-- 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 τ
hπ : IsStoppingTime f π
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (fun (ω : Ω) ↦ max (τ ω) (π ω)) ω ≤ (↑i : WithTop ι)}
have simp_rw : MeasurableSet.{u_1} (α := Ω) ({a : Ω | τ a ≤ (↑i : WithTop ι)} ∩ {a : Ω | π a ≤ (↑i : WithTop ι)})
Tactic: simp_rw [max_le_iff, Set.setOf_and]
-- 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 τ
hπ : IsStoppingTime f π
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (fun (ω : Ω) ↦ min (τ ω) (π ω)) ω ≤ (↑i : WithTop ι)}
have simp_rw : MeasurableSet.{u_1} (α := Ω) ({a : Ω | τ a ≤ (↑i : WithTop ι)} ∪ {a : Ω | π a ≤ (↑i : WithTop ι)})
Tactic: simp_rw [min_le_iff, Set.setOf_or]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : DenselyOrdered ι
inst_4 : FirstCountableTopology ι
inst_5 : NoMaxOrder ι
κ : Type u_4
f : Filtration ι m
τ : κ → Ω → WithTop ι
s : Set κ
hs : s.Countable
inst_6 : f.IsRightContinuous
hτ : ∀ n ∈ s, IsStoppingTime f (τ n)
⊢ IsStoppingTime f fun (ω : Ω) ↦ ⨅ n ∈ s, τ n ω
have refine : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | ⨅ n ∈ s, τ n ω < (↑i : WithTop ι)}ᶜ
Tactic: refine isStoppingTime_of_measurableSet_lt_of_isRightContinuous <|
    fun i ↦ MeasurableSet.of_compl ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : DenselyOrdered ι
inst_4 : FirstCountableTopology ι
inst_5 : NoMaxOrder ι
κ : Type u_4
f : Filtration ι m
τ : κ → Ω → WithTop ι
s : Set κ
hs : s.Countable
inst_6 : f.IsRightContinuous
hτ : ∀ n ∈ s, IsStoppingTime f (τ n)
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | ⨅ n ∈ s, τ n ω < (↑i : WithTop ι)}ᶜ
have rw : MeasurableSet.{u_1} (α := Ω) (⋂ n ∈ s, {ω : Ω | (↑i : WithTop ι) ≤ τ n ω})
Tactic: rw [(_ : {ω | ⨅ n ∈ s, τ n ω < i}ᶜ = ⋂ n ∈ s, {ω | i ≤ τ n ω})]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : DenselyOrdered ι
inst_4 : FirstCountableTopology ι
inst_5 : NoMaxOrder ι
κ : Type u_4
f : Filtration ι m
τ : κ → Ω → WithTop ι
s : Set κ
hs : s.Countable
inst_6 : f.IsRightContinuous
hτ : ∀ n ∈ s, IsStoppingTime f (τ n)
i : ι
rw : MeasurableSet.{u_1} (α := Ω) (⋂ n ∈ s, {ω : Ω | (↑i : WithTop ι) ≤ τ n ω})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | ⨅ n ∈ s, τ n ω < (↑i : WithTop ι)}ᶜ
have rw₁ : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | ⨅ n ∈ s, τ n ω < (↑i : WithTop ι)}ᶜ (⋂ n ∈ s, {ω : Ω | (↑i : WithTop ι) ≤ τ n ω})
Tactic: rw [(_ : {ω | ⨅ n ∈ s, τ n ω < i}ᶜ = ⋂ n ∈ s, {ω | i ≤ τ n ω})]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : DenselyOrdered ι
inst_4 : FirstCountableTopology ι
inst_5 : NoMaxOrder ι
κ : Type u_4
f : Filtration ι m
τ : κ → Ω → WithTop ι
s : Set κ
hs : s.Countable
inst_6 : f.IsRightContinuous
hτ : ∀ n ∈ s, IsStoppingTime f (τ n)
i : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | ⨅ n ∈ s, τ n ω < (↑i : WithTop ι)}ᶜ (⋂ n ∈ s, {ω : Ω | (↑i : WithTop ι) ≤ τ n ω})
have h : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | ⨅ n ∈ s, τ n ω < (↑i : WithTop ι)}ᶜ ω ↔
    Membership.mem (γ := Set Ω) (⋂ n ∈ s, {ω : Ω | (↑i : WithTop ι) ≤ τ n ω}) ω
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : DenselyOrdered ι
inst_4 : FirstCountableTopology ι
inst_5 : NoMaxOrder ι
κ : Type u_4
inst_6 : Countable κ
f : Filtration ι m
τ : κ → Ω → WithTop ι
inst_7 : f.IsRightContinuous
hτ : ∀ (n : κ), IsStoppingTime f (τ n)
⊢ IsStoppingTime f fun (ω : Ω) ↦ ⨅ (n : κ), τ n ω
have h : ∀ (x : Ω),
  Eq.{u_3 + 1} (α := WithTop ι) (⨅ (n : κ), τ n x) (⨅ (n : κ), ⨅ (_ : Membership.mem (γ := Set κ) Set.univ n), τ n x)
Tactic: convert! IsStoppingTime.biInf (κ := κ) Set.countable_univ (fun n _ => hτ n) using 2
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : AddGroup ι
inst_1 : Preorder ι
inst_2 : AddRightMono ι
inst_3 : AddLeftMono ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)} {ω : Ω | τ ω ≤ (↑(j - i) : WithTop ι)}
have h : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)} ω ↔
    Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑(j - i) : WithTop ι)} ω
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : AddGroup ι
inst_1 : Preorder ι
inst_2 : AddRightMono ι
inst_3 : AddLeftMono ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
ω : Ω
a : ι
⊢ (↑a : WithTop ι) + (↑i : WithTop ι) ≤ (↑j : WithTop ι) ↔ (↑a : WithTop ι) ≤ (↑(j - i) : WithTop ι)
have h : a + i ≤ j ↔ a ≤ j - i
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : AddGroup ι
inst_1 : Preorder ι
inst_2 : AddRightMono ι
inst_3 : AddLeftMono ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
ω : Ω
⊢ τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι) ↔ τ ω ≤ (↑(j - i) : WithTop ι)
have h : ∀ (x : WithTop ι), x + (↑i : WithTop ι) ≤ (↑j : WithTop ι) ↔ x ≤ (↑(j - i) : WithTop ι)
Tactic: cases τ ω with
    | top => simp
    | coe a => norm_cast; simp_rw [← le_sub_iff_add_le]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : AddGroup ι
inst_1 : Preorder ι
inst_2 : AddRightMono ι
inst_3 : AddLeftMono ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)}
have h_eq : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)} {ω : Ω | τ ω ≤ (↑(j - i) : WithTop ι)}
Tactic: have h_eq : {ω | τ ω + i ≤ j} = {ω | τ ω ≤ j - i} := by
    ext ω
    simp only [Set.mem_setOf_eq, coe_sub]
    cases τ ω with
    | top => simp
    | coe a => norm_cast; simp_rw [← le_sub_iff_add_le]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : AddGroup ι
inst_1 : Preorder ι
inst_2 : AddRightMono ι
inst_3 : AddLeftMono ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
h_eq :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)} {ω : Ω | τ ω ≤ (↑(j - i) : WithTop ι)}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)}
have rw : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑(j - i) : WithTop ι)}
Tactic: rw [h_eq]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Add ι
inst_1 : LinearOrder ι
inst_2 : CanonicallyOrderedAdd ι
inst_3 : Countable ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i j : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)}
    (⋃ (k : (↑{k : ι | k + i ≤ j} : Type u_3)), {ω : Ω | τ ω = (↑(↑k : ι) : WithTop ι)})
have h : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)} ω ↔
    Membership.mem (γ := Set Ω) (⋃ (k : (↑{k : ι | k + i ≤ j} : Type u_3)), {ω : Ω | τ ω = (↑(↑k : ι) : WithTop ι)}) ω
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Add ι
inst_1 : LinearOrder ι
inst_2 : CanonicallyOrderedAdd ι
inst_3 : Countable ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i j : ι
ω : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)} ω ↔
    Membership.mem (γ := Set Ω) (⋃ (k : (↑{k : ι | k + i ≤ j} : Type u_3)), {ω : Ω | τ ω = (↑(↑k : ι) : WithTop ι)}) ω
have h : τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι) ↔ ∃ (i_1 : (↑{k : ι | k + i ≤ j} : Type u_3)), τ ω = (↑(↑i_1 : ι) : WithTop ι)
Tactic: simp only [Set.mem_setOf_eq, Set.mem_iUnion]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Add ι
inst_1 : LinearOrder ι
inst_2 : CanonicallyOrderedAdd ι
inst_3 : Countable ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i j : ι
ω : Ω
a : ι
⊢ (↑a : WithTop ι) + (↑i : WithTop ι) ≤ (↑j : WithTop ι) ↔
    ∃ (i_1 : (↑{k : ι | k + i ≤ j} : Type u_3)), (↑a : WithTop ι) = (↑(↑i_1 : ι) : WithTop ι)
have h : (↑a : WithTop ι) + (↑i : WithTop ι) ≤ (↑j : WithTop ι) ↔ a + i ≤ j
Tactic: simp
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Add ι
inst_1 : LinearOrder ι
inst_2 : CanonicallyOrderedAdd ι
inst_3 : Countable ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i j : ι
ω : Ω
a : ι
⊢ (↑a : WithTop ι) + (↑i : WithTop ι) ≤ (↑j : WithTop ι) ↔ a + i ≤ j
have h : a + i ≤ j ↔ a + 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 : Add ι
inst_1 : LinearOrder ι
inst_2 : CanonicallyOrderedAdd ι
inst_3 : Countable ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i j : ι
ω : Ω
⊢ τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι) ↔
    ∃ (i_1 : (↑{k : ι | k + i ≤ j} : Type u_3)), τ ω = (↑(↑i_1 : ι) : WithTop ι)
have h : ∀ (x : WithTop ι),
  x + (↑i : WithTop ι) ≤ (↑j : WithTop ι) ↔ ∃ (i_1 : (↑{k : ι | k + i ≤ j} : Type u_3)), x = (↑(↑i_1 : ι) : WithTop ι)
Tactic: cases τ ω with
    | top => simp
    | coe a => simp; norm_cast
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Add ι
inst_1 : LinearOrder ι
inst_2 : CanonicallyOrderedAdd ι
inst_3 : Countable ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i j : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (fun (ω : Ω) ↦ τ ω + (↑i : WithTop ι)) ω ≤ (↑j : WithTop ι)}
have h : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω + (↑i : WithTop ι) ≤ (↑j : WithTop ι)}
  (⋃ (k : (↑{k : ι | k + i ≤ j} : Type u_3)), {ω : Ω | τ ω = (↑(↑k : ι) : WithTop ι)})
Tactic: have h : {ω | τ ω + i ≤ j} = ⋃ k : {k | k + i ≤ j}, {ω | τ ω = k} := by
    ext ω
    simp only [Set.mem_setOf_eq, Set.mem_iUnion]
    cases τ ω with
    | top => simp
    | coe a => simp; norm_cast
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Add ι
inst_1 : LinearOrder ι
inst_2 : CanonicallyOrderedAdd ι
inst_3 : Countable ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (τ + π) ω ≤ (↑j : WithTop ι)}
    (⋃ (k : (↑(Set.Iic j) : Type u_3)),
      {ω : Ω | π ω = (↑(↑k : ι) : WithTop ι)} ∩ {ω : Ω | τ ω + (↑(↑k : ι) : WithTop ι) ≤ (↑j : WithTop ι)})
have h : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | (τ + π) ω ≤ (↑j : WithTop ι)} ω ↔
    Membership.mem (γ := Set Ω)
      (⋃ (k : (↑(Set.Iic j) : Type u_3)),
        {ω : Ω | π ω = (↑(↑k : ι) : WithTop ι)} ∩ {ω : Ω | τ ω + (↑(↑k : ι) : WithTop ι) ≤ (↑j : WithTop ι)})
      ω
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Add ι
inst_1 : LinearOrder ι
inst_2 : CanonicallyOrderedAdd ι
inst_3 : Countable ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | (τ + π) ω ≤ (↑j : WithTop ι)} ω ↔
    Membership.mem (γ := Set Ω)
      (⋃ (k : (↑(Set.Iic j) : Type u_3)),
        {ω : Ω | π ω = (↑(↑k : ι) : WithTop ι)} ∩ {ω : Ω | τ ω + (↑(↑k : ι) : WithTop ι) ≤ (↑j : WithTop ι)})
      ω
have h : τ ω + π ω ≤ (↑j : WithTop ι) ↔
  ∃ (i : (↑(Set.Iic j) : Type u_3)), π ω = (↑(↑i : ι) : WithTop ι) ∧ τ ω + (↑(↑i : ι) : WithTop ι) ≤ (↑j : WithTop ι)
Tactic: simp only [Pi.add_apply, Set.mem_setOf_eq, Set.mem_iUnion, Set.mem_inter_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Add ι
inst_1 : LinearOrder ι
inst_2 : CanonicallyOrderedAdd ι
inst_3 : Countable ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
a b : ι
⊢ (↑a : WithTop ι) + (↑b : WithTop ι) ≤ (↑j : WithTop ι) ↔
    ∃ (i : (↑(Set.Iic j) : Type u_3)),
      (↑b : WithTop ι) = (↑(↑i : ι) : WithTop ι) ∧ (↑a : WithTop ι) + (↑(↑i : ι) : WithTop ι) ≤ (↑j : WithTop ι)
have h : a + b ≤ j ↔ ∃ (i : (↑(Set.Iic j) : Type u_3)), b = (↑i : ι) ∧ a + (↑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 : Add ι
inst_1 : LinearOrder ι
inst_2 : CanonicallyOrderedAdd ι
inst_3 : Countable ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
a : ι
⊢ (↑a : WithTop ι) + π ω ≤ (↑j : WithTop ι) ↔
    ∃ (i : (↑(Set.Iic j) : Type u_3)),
      π ω = (↑(↑i : ι) : WithTop ι) ∧ (↑a : WithTop ι) + (↑(↑i : ι) : WithTop ι) ≤ (↑j : WithTop ι)
have h : ∀ (x : WithTop ι),
  (↑a : WithTop ι) + x ≤ (↑j : WithTop ι) ↔
    ∃ (i : (↑(Set.Iic j) : Type u_3)),
      x = (↑(↑i : ι) : WithTop ι) ∧ (↑a : WithTop ι) + (↑(↑i : ι) : WithTop ι) ≤ (↑j : WithTop ι)
Tactic: cases π ω with
      | top => simp
      | coe b => norm_cast; simpa using le_of_add_le_right
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Add ι
inst_1 : LinearOrder ι
inst_2 : CanonicallyOrderedAdd ι
inst_3 : Countable ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
⊢ τ ω + π ω ≤ (↑j : WithTop ι) ↔
    ∃ (i : (↑(Set.Iic j) : Type u_3)), π ω = (↑(↑i : ι) : WithTop ι) ∧ τ ω + (↑(↑i : ι) : WithTop ι) ≤ (↑j : WithTop ι)
have h : ∀ (x : WithTop ι),
  x + π ω ≤ (↑j : WithTop ι) ↔
    ∃ (i : (↑(Set.Iic j) : Type u_3)), π ω = (↑(↑i : ι) : WithTop ι) ∧ x + (↑(↑i : ι) : WithTop ι) ≤ (↑j : WithTop ι)
Tactic: cases τ ω with
    | top => simp
    | coe a =>
      cases π ω with
      | top => simp
      | coe b => norm_cast; simpa using le_of_add_le_right
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Add ι
inst_1 : LinearOrder ι
inst_2 : CanonicallyOrderedAdd ι
inst_3 : Countable ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (τ + π) ω ≤ (↑j : WithTop ι)}
have h : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (τ + π) ω ≤ (↑j : WithTop ι)}
  (⋃ (k : (↑(Set.Iic j) : Type u_3)),
    {ω : Ω | π ω = (↑(↑k : ι) : WithTop ι)} ∩ {ω : Ω | τ ω + (↑(↑k : ι) : WithTop ι) ≤ (↑j : WithTop ι)})
Tactic: have h : {ω | (τ + π) ω ≤ j} = ⋃ k : Set.Iic j, {ω | π ω = k} ∩ {ω | τ ω + k ≤ j} := by
    ext ω
    simp only [Pi.add_apply, Set.mem_setOf_eq, Set.mem_iUnion, Set.mem_inter_iff]
    cases τ ω with
    | top => simp
    | coe a =>
      cases π ω with
      | top => simp
      | coe b => norm_cast; simpa using le_of_add_le_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 : MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
⊢ MeasurableSet sᶜ ∧ ∀ (i : ι), MeasurableSet (sᶜ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
have refine : ∀ (i : ι), MeasurableSet (sᶜ ∩ {ω : Ω | τ ω ≤ (↑i : WithTop ι)})
Tactic: refine ⟨hs.1.compl, fun i ↦ ?_⟩