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 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i i' : ι
hi'_lub : IsLUB (Set.Iio i) i'
hi'_eq_i : i' = i
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have inl : ∀ (hi'_lub : IsLUB (Set.Iio i') i') (hi'_eq_i : i' = i), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i' : WithTop ι)}
Tactic: rw [← hi'_eq_i] at hi'_lub ⊢
Cleared hypotheses: hi'_lub, hi'_eq_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 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i i' : ι
hi'_lub : IsLUB (Set.Iio i) i'
h_Iio_eq_Iic : Set.Iio i = Set.Iic i'
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have h_lt_eq_preimage : {ω : Ω | τ ω < (↑i : WithTop ι)} = τ ⁻¹' Set.Iio (↑i : WithTop ι)
Tactic: have h_lt_eq_preimage : {ω : Ω | τ ω < i} = τ ⁻¹' Set.Iio i := rfl
-- 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 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i i' : ι
hi'_lub : IsLUB (Set.Iio i) i'
h_Iio_eq_Iic : Set.Iio i = Set.Iic i'
h_lt_eq_preimage : {ω : Ω | τ ω < (↑i : WithTop ι)} = τ ⁻¹' Set.Iio (↑i : WithTop ι)
⊢ Set.Iio (↑i : WithTop ι) = Set.Iic (↑i' : WithTop ι)
have rw : WithTop.some '' Set.Iio i = Set.Iic (↑i' : WithTop ι)
Tactic: rw [← image_coe_Iio, ← image_coe_Iic, h_Iio_eq_Iic]
-- 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 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i i' : ι
hi'_lub : IsLUB (Set.Iio i) i'
h_Iio_eq_Iic : Set.Iio i = Set.Iic i'
h_lt_eq_preimage : {ω : Ω | τ ω < (↑i : WithTop ι)} = τ ⁻¹' Set.Iio (↑i : WithTop ι)
rw : WithTop.some '' Set.Iio i = Set.Iic (↑i' : WithTop ι)
⊢ Set.Iio (↑i : WithTop ι) = Set.Iic (↑i' : WithTop ι)
have rw₁ : WithTop.some '' Set.Iio i = WithTop.some '' Set.Iic i'
Tactic: rw [← image_coe_Iio, ← image_coe_Iic, h_Iio_eq_Iic]
-- 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 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i i' : ι
hi'_lub : IsLUB (Set.Iio i) i'
h_Iio_eq_Iic : Set.Iio i = Set.Iic i'
h_lt_eq_preimage : {ω : Ω | τ ω < (↑i : WithTop ι)} = τ ⁻¹' Set.Iio (↑i : WithTop ι)
rw : WithTop.some '' Set.Iio i = Set.Iic (↑i' : WithTop ι)
rw₁ : WithTop.some '' Set.Iio i = WithTop.some '' Set.Iic i'
⊢ Set.Iio (↑i : WithTop ι) = Set.Iic (↑i' : WithTop ι)
have rw₂ : WithTop.some '' Set.Iic i' = WithTop.some '' Set.Iic i'
Tactic: rw [← image_coe_Iio, ← image_coe_Iic, h_Iio_eq_Iic]
-- 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 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i i' : ι
hi'_lub : IsLUB (Set.Iio i) i'
h_Iio_eq_Iic : Set.Iio i = Set.Iic i'
h_lt_eq_preimage : {ω : Ω | τ ω < (↑i : WithTop ι)} = τ ⁻¹' Set.Iio (↑i : WithTop ι)
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have h_Iio_eq_Iic' : Set.Iio (↑i : WithTop ι) = Set.Iic (↑i' : WithTop ι)
Tactic: have h_Iio_eq_Iic' : Set.Iio (i : WithTop ι) = Set.Iic (i' : WithTop ι) := by
      rw [← image_coe_Iio, ← image_coe_Iic, h_Iio_eq_Iic]
-- 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 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i i' : ι
hi'_lub : IsLUB (Set.Iio i) i'
h_Iio_eq_Iic : Set.Iio i = Set.Iic i'
h_lt_eq_preimage : {ω : Ω | τ ω < (↑i : WithTop ι)} = τ ⁻¹' Set.Iio (↑i : WithTop ι)
h_Iio_eq_Iic' : Set.Iio (↑i : WithTop ι) = Set.Iic (↑i' : WithTop ι)
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have inr : MeasurableSet (τ ⁻¹' Set.Iic (↑i' : WithTop ι))
Tactic: rw [h_lt_eq_preimage, h_Iio_eq_Iic']
-- 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 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω} {ω : Ω | τ ω < (↑i : WithTop ι)}ᶜ
have h : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω} ω ↔
    Membership.mem (γ := Set Ω) {ω : Ω | τ ω < (↑i : 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 ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω}
have this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω} {ω : Ω | τ ω < (↑i : WithTop ι)}ᶜ
Tactic: have : {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ := by
    ext1 ω; simp only [Set.mem_setOf_eq, Set.mem_compl_iff, not_lt]
-- 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 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω} {ω : Ω | τ ω < (↑i : WithTop ι)}ᶜ
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω}
have rw : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : 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 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≥ (↑i : WithTop ι)})
have h : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} ω ↔
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≥ (↑i : 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 ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
have this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
  ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≥ (↑i : WithTop ι)})
Tactic: have : {ω | τ ω = i} = {ω | τ ω ≤ i} ∩ {ω | τ ω ≥ i} := by
    ext1 ω; simp only [Set.mem_setOf_eq, Set.mem_inter_iff, le_antisymm_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 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≥ (↑i : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
have rw : MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≥ (↑i : WithTop ι)})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
inst_1 : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
i : ι
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
    (⋃ (k : ι), ⋃ (_ : k ≤ i), {ω : Ω | τ ω = (↑k : WithTop ι)})
have h : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ω ↔
    Membership.mem (γ := Set Ω) (⋃ (k : ι), ⋃ (_ : k ≤ i), {ω : Ω | τ ω = (↑k : WithTop ι)}) ω
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
inst_1 : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
i : ι
ω : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)} ω ↔
    Membership.mem (γ := Set Ω) (⋃ (k : ι), ⋃ (_ : k ≤ i), {ω : Ω | τ ω = (↑k : WithTop ι)}) ω
have h : τ ω ≤ (↑i : WithTop ι) ↔ ∃ i_1 ≤ i, τ ω = (↑i_1 : WithTop ι)
Tactic: simp only [Set.mem_setOf_eq, Set.mem_iUnion, exists_prop]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
inst_1 : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
i : ι
ω : Ω
a : ι
⊢ (↑a : WithTop ι) ≤ (↑i : WithTop ι) ↔ ∃ i_1 ≤ i, (↑a : WithTop ι) = (↑i_1 : WithTop ι)
have h : a ≤ i ↔ ∃ i_1 ≤ i, a = i_1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
inst_1 : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
i : ι
ω : Ω
⊢ τ ω ≤ (↑i : WithTop ι) ↔ ∃ i_1 ≤ i, τ ω = (↑i_1 : WithTop ι)
have h : ∀ (x : WithTop ι), x ≤ (↑i : WithTop ι) ↔ ∃ i_1 ≤ i, x = (↑i_1 : WithTop ι)
Tactic: cases τ ω with
    | top => simp
    | coe a => norm_cast; simp
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
inst_1 : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
have h_eq_iUnion : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)} (⋃ (k : ι), ⋃ (_ : k ≤ i), {ω : Ω | τ ω = (↑k : WithTop ι)})
Tactic: have h_eq_iUnion : {ω | τ ω ≤ i} = ⋃ k ≤ i, {ω | τ ω = k} := by
    ext ω
    simp only [Set.mem_setOf_eq, Set.mem_iUnion, exists_prop]
    cases τ ω with
    | top => simp
    | coe a => norm_cast; simp
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
inst_1 : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
i : ι
h_eq_iUnion :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
    (⋃ (k : ι), ⋃ (_ : k ≤ i), {ω : Ω | τ ω = (↑k : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
have rw : MeasurableSet.{u_1} (α := Ω) (⋃ (k : ι), ⋃ (_ : k ≤ i), {ω : Ω | τ ω = (↑k : WithTop ι)})
Tactic: rw [h_eq_iUnion]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Preorder ι
inst_1 : Countable ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
i : ι
h_eq_iUnion :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑i : WithTop ι)}
    (⋃ (k : ι), ⋃ (_ : k ≤ i), {ω : Ω | τ ω = (↑k : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) (⋃ (k : ι), ⋃ (_ : k ≤ i), {ω : Ω | τ ω = (↑k : WithTop ι)})
have refine : ∀ (k : ι) (hk : Membership.mem (γ := Set ι) (fun (k : ι) ↦ (Preorder.toLE : LE ι).1 k i) k),
  MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑k : WithTop ι)}
Tactic: refine MeasurableSet.biUnion (Set.to_countable _) fun k hk => ?_
-- 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 : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
have pos : ∀ (ht : 𝓝[>] t = ⊥), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
Tactic: by_cases ht : 𝓝[>] t = ⊥
-- 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 : ι
pos : ∀ (ht : 𝓝[>] t = ⊥), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
have neg : ∀ (ht : ¬𝓝[>] t = ⊥), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
Tactic: by_cases ht : 𝓝[>] t = ⊥
-- 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 = ⊥
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
    ({ω : Ω | τ ω < (↑t : WithTop ι)} ∪ {ω : Ω | τ ω = (↑t : WithTop ι)})
have h : ∀ (x : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)} x ↔
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω < (↑t : WithTop ι)} ∪ {ω : Ω | τ ω = (↑t : WithTop ι)}) x
Tactic: ext
-- 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 = ⊥
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
have h_eq : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
  ({ω : Ω | τ ω < (↑t : WithTop ι)} ∪ {ω : Ω | τ ω = (↑t : WithTop ι)})
Tactic: have h_eq : {ω | τ ω ≤ t} = {ω | τ ω < t} ∪ {ω | τ ω = t} := by ext; grind
-- 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 = ⊥
h_eq :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
    ({ω : Ω | τ ω < (↑t : WithTop ι)} ∪ {ω : Ω | τ ω = (↑t : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
have pos : MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω < (↑t : WithTop ι)} ∪ {ω : Ω | τ ω = (↑t : WithTop ι)})
Tactic: rw [h_eq]
-- 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 = ⊥
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
have this : (𝓝[>] t).NeBot
Tactic: have : (𝓝[>] t).NeBot := ⟨ht⟩
-- 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 : ℕ → ι), (∀ (n : ℕ), t < s n) ∧ Tendsto s atTop (𝓝 t)
have h_freq : ∃ᶠ (x : ι) in 𝓝[>] t, t < x
Tactic: have h_freq : ∃ᶠ x in 𝓝[>] t, t < x :=
      Eventually.frequently <| eventually_nhdsWithin_of_forall fun _ hx ↦ hx
-- 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
h_freq : ∃ᶠ (x : ι) in 𝓝[>] t, t < x
⊢ ∃ (s : ℕ → ι), (∀ (n : ℕ), t < s n) ∧ Tendsto s atTop (𝓝 t)
have this₁ : ∃ (ns : ℕ → ι), Tendsto ns atTop (𝓝[>] t) ∧ ∀ (n : ℕ), t < ns n
Tactic: have := exists_seq_forall_of_frequently h_freq
-- 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_1 : (𝓝[>] t).NeBot
h_freq : ∃ᶠ (x : ι) in 𝓝[>] t, t < x
this : ∃ (ns : ℕ → ι), Tendsto ns atTop (𝓝[>] t) ∧ ∀ (n : ℕ), t < ns n
⊢ ∃ (s : ℕ → ι), (∀ (n : ℕ), t < s n) ∧ Tendsto s atTop (𝓝 t)
have this₁ : ∃ (ns : ℕ → ι), (Tendsto ns atTop (𝓝 t) ∧ ∀ᶠ (n : ℕ) in atTop, ns n ∈ Set.Ioi t) ∧ ∀ (n : ℕ), t < ns n
Tactic: simp_rw [tendsto_nhdsWithin_iff] 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 : 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_1 : (𝓝[>] t).NeBot
h_freq : ∃ᶠ (x : ι) in 𝓝[>] t, t < x
this : ∃ (ns : ℕ → ι), (Tendsto ns atTop (𝓝 t) ∧ ∀ᶠ (n : ℕ) in atTop, ns n ∈ Set.Ioi t) ∧ ∀ (n : ℕ), t < ns n
⊢ ∃ (s : ℕ → ι), (∀ (n : ℕ), t < s n) ∧ Tendsto s atTop (𝓝 t)
have obtain : ∀ (s : ℕ → ι) (hs_gt : ∀ (n : ℕ), t < s n) (hs_tendsto : Tendsto s atTop (𝓝 t)),
  (∀ᶠ (n : ℕ) in atTop, s n ∈ Set.Ioi t) → ∃ (s : ℕ → ι), (∀ (n : ℕ), t < s n) ∧ Tendsto s atTop (𝓝 t)
Tactic: obtain ⟨s, ⟨hs_tendsto, _⟩, hs_gt⟩ := this
Cleared hypotheses: this
-- 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
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
have neg : ∀ (s : ℕ → ι) (hs_gt : ∀ (n : ℕ), t < s n) (hs_tendsto : Tendsto s atTop (𝓝 t)),
  MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
Tactic: obtain ⟨s, hs_gt, hs_tendsto⟩ : ∃ s : ℕ → ι, (∀ n, t < s n) ∧ Tendsto s atTop (𝓝 t) := by
    have h_freq : ∃ᶠ x in 𝓝[>] t, t < x :=
      Eventually.frequently <| eventually_nhdsWithin_of_forall fun _ hx ↦ hx
    have := exists_seq_forall_of_frequently h_freq
    simp_rw [tendsto_nhdsWithin_iff] at this
    obtain ⟨s, ⟨hs_tendsto, _⟩, hs_gt⟩ := this
    exact ⟨s, hs_gt, hs_tendsto⟩
-- 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)
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
have h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
Tactic: have h_exists_lt (u : ι) (hu : t < u) : ∃ i, s i < u :=
    Eventually.exists (f := atTop) (hs_tendsto.eventually_lt_const hu)
-- 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
u : WithTop ι
hu : (↑t : WithTop ι) < u
⊢ ∃ (i : ℕ), (↑(s i) : WithTop ι) < u
have refine : ∀ᶠ (x : ℕ) in atTop, (↑(s x) : WithTop ι) < u
Tactic: refine Eventually.exists (f := atTop) ?_