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 : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
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 : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
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 [lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
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
m : MeasurableSpace Ω
ι : Type u_4
inst : LinearOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
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
m : MeasurableSpace Ω
ι : Type u_4
inst : LinearOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
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
m : MeasurableSpace Ω
ι : Type u_4
inst : LinearOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
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 ι
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 ι
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_le]
-- 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 : ι
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 : ι
h_lub : IsLUB (Set.Iio i) i
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have pos : ∀ (hi_min : IsMin i), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
Tactic: by_cases hi_min : IsMin 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 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
pos : ∀ (hi_min : IsMin i), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have neg : ∀ (hi_min : ¬IsMin i), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
Tactic: by_cases hi_min : IsMin 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 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ∅
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have rw : MeasurableSet.{u_1} (α := Ω) ∅
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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have pos : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ∅
Tactic: suffices {ω | τ ω < i} = ∅ by rw [this]; exact @MeasurableSet.empty _ (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 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ∅
have pos : ∀ (ω : Ω), Membership.mem (γ := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ω ↔ Membership.mem (γ := Set Ω) ∅ ω
Tactic: ext1 ω
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
ω : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ω ↔ Membership.mem (γ := Set Ω) ∅ ω
have pos : ¬τ ω < (↑i : WithTop ι)
Tactic: simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false]
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
ω : Ω
t : ι
⊢ ¬(↑t : WithTop ι) < (↑i : WithTop ι)
have pos : ¬t < i
Tactic: norm_cast
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
ω : Ω
⊢ ¬τ ω < (↑i : WithTop ι)
have pos : ∀ (x : WithTop ι), ¬x < (↑i : WithTop ι)
Tactic: cases τ ω with
    | top => simp
    | coe t => norm_cast; exact isMin_iff_forall_not_lt.mp hi_min t
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have neg : ∀ (seq : ℕ → ι) (h_tendsto : Tendsto seq atTop (𝓝 i)) (h_bound : ∀ (j : ℕ), seq j < i),
  MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
Tactic: obtain ⟨seq, -, -, h_tendsto, h_bound⟩ :
      ∃ seq : ℕ → ι, Monotone seq ∧ (∀ j, seq j ≤ i) ∧ Tendsto seq atTop (𝓝 i) ∧ ∀ j, seq j < i :=
    h_lub.exists_seq_monotone_tendsto (not_isMin_iff.mp hi_min)
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
⊢ Set.Iio (↑i : WithTop ι) = ⋃ (j : ℕ), {k : WithTop ι | k ≤ (↑(seq j) : WithTop ι)}
have h : ∀ (k : WithTop ι),
  k ∈ Set.Iio (↑i : WithTop ι) ↔
    Membership.mem (γ := Set (WithTop ι)) (⋃ (j : ℕ), {k : WithTop ι | k ≤ (↑(seq j) : WithTop ι)}) k
Tactic: ext1 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 ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
k : WithTop ι
⊢ k ∈ Set.Iio (↑i : WithTop ι) ↔
    Membership.mem (γ := Set (WithTop ι)) (⋃ (j : ℕ), {k : WithTop ι | k ≤ (↑(seq j) : WithTop ι)}) k
have h : k < (↑i : WithTop ι) ↔ ∃ (i : ℕ), k ≤ (↑(seq i) : WithTop ι)
Tactic: push _ ∈ _
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
k : WithTop ι
⊢ k < (↑i : WithTop ι) ↔ ∃ (i : ℕ), k ≤ (↑(seq i) : WithTop ι)
have h : ∀ (hk_lt_i : k < (↑i : WithTop ι)), ∃ (i : ℕ), k ≤ (↑(seq i) : WithTop ι)
Tactic: refine ⟨fun hk_lt_i => ?_, fun h_exists_k_le_seq => ?_⟩
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
k : WithTop ι
h : ∀ (hk_lt_i : k < (↑i : WithTop ι)), ∃ (i : ℕ), k ≤ (↑(seq i) : WithTop ι)
⊢ k < (↑i : WithTop ι) ↔ ∃ (i : ℕ), k ≤ (↑(seq i) : WithTop ι)
have h₁ : ∀ (h_exists_k_le_seq : ∃ (i : ℕ), k ≤ (↑(seq i) : WithTop ι)), k < (↑i : WithTop ι)
Tactic: refine ⟨fun hk_lt_i => ?_, fun h_exists_k_le_seq => ?_⟩
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
k : WithTop ι
hk_lt_i : k < (↑i : WithTop ι)
⊢ ∃ (i : ℕ), k ≤ (↑(seq i) : WithTop ι)
have h : ∀ (h_tendsto : ∀ s ∈ 𝓝 i, ∃ (a : ℕ), ∀ b ≥ a, seq b ∈ s) (h_bound : ∀ (j : ℕ), seq j < i) (k : WithTop ι)
  (hk_lt_i : k < (↑i : WithTop ι)), ∃ (i : ℕ), k ≤ (↑(seq i) : WithTop ι)
Tactic: rw [tendsto_atTop'] at h_tendsto
Cleared hypotheses: h_tendsto, h_bound, k, hk_lt_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 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : ∀ s ∈ 𝓝 i, ∃ (a : ℕ), ∀ b ≥ a, seq b ∈ s
h_bound : ∀ (j : ℕ), seq j < i
k : ι
hk_lt_i : (↑k : WithTop ι) < (↑i : WithTop ι)
⊢ ∃ (i : ℕ), (↑k : WithTop ι) ≤ (↑(seq i) : WithTop ι)
have h : ∀ (hk_lt_i : k < i), ∃ (i : ℕ), k ≤ seq i
Tactic: norm_cast at hk_lt_i ⊢
Cleared hypotheses: hk_lt_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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : ∀ s ∈ 𝓝 i, ∃ (a : ℕ), ∀ b ≥ a, seq b ∈ s
h_bound : ∀ (j : ℕ), seq j < i
k : ι
hk_lt_i : k < i
⊢ ∃ (i : ℕ), k ≤ seq i
have h_nhds : Set.Ici k ∈ 𝓝 i
Tactic: have h_nhds : Set.Ici k ∈ 𝓝 i :=
          mem_nhds_iff.mpr ⟨Set.Ioi k, Set.Ioi_subset_Ici le_rfl, isOpen_Ioi, hk_lt_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 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : ∀ s ∈ 𝓝 i, ∃ (a : ℕ), ∀ b ≥ a, seq b ∈ s
h_bound : ∀ (j : ℕ), seq j < i
k : ι
hk_lt_i : k < i
h_nhds : Set.Ici k ∈ 𝓝 i
⊢ ∃ (i : ℕ), k ≤ seq i
have h : ∀ (a : ℕ) (ha : ∀ b ≥ a, k ≤ seq b), ∃ (i : ℕ), k ≤ seq i
Tactic: obtain ⟨a, ha⟩ : ∃ a : ℕ, ∀ b : ℕ, b ≥ a → k ≤ seq b := h_tendsto (Set.Ici k) h_nhds
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : ∀ s ∈ 𝓝 i, ∃ (a : ℕ), ∀ b ≥ a, seq b ∈ s
h_bound : ∀ (j : ℕ), seq j < i
k : WithTop ι
hk_lt_i : k < (↑i : WithTop ι)
⊢ ∃ (i : ℕ), k ≤ (↑(seq i) : WithTop ι)
have h : ∀ (hk_lt_i : ⊤ < (↑i : WithTop ι)), ∃ (i : ℕ), ⊤ ≤ (↑(seq i) : WithTop ι)
Tactic: cases k with
      | top => simp at hk_lt_i
      | coe k =>
        norm_cast at hk_lt_i ⊢
        have h_nhds : Set.Ici k ∈ 𝓝 i :=
          mem_nhds_iff.mpr ⟨Set.Ioi k, Set.Ioi_subset_Ici le_rfl, isOpen_Ioi, hk_lt_i⟩
        obtain ⟨a, ha⟩ : ∃ a : ℕ, ∀ b : ℕ, b ≥ a → k ≤ seq b := h_tendsto (Set.Ici k) h_nhds
        exact ⟨a, ha a le_rfl⟩
Cleared hypotheses: k, hk_lt_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 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : ∀ s ∈ 𝓝 i, ∃ (a : ℕ), ∀ b ≥ a, seq b ∈ s
h_bound : ∀ (j : ℕ), seq j < i
k : WithTop ι
hk_lt_i : k < (↑i : WithTop ι)
h : ∀ (hk_lt_i : ⊤ < (↑i : WithTop ι)), ∃ (i : ℕ), ⊤ ≤ (↑(seq i) : WithTop ι)
⊢ ∃ (i : ℕ), k ≤ (↑(seq i) : WithTop ι)
have h₁ : ∀ (k : ι) (hk_lt_i : (↑k : WithTop ι) < (↑i : WithTop ι)), ∃ (i : ℕ), (↑k : WithTop ι) ≤ (↑(seq i) : WithTop ι)
Tactic: cases k with
      | top => simp at hk_lt_i
      | coe k =>
        norm_cast at hk_lt_i ⊢
        have h_nhds : Set.Ici k ∈ 𝓝 i :=
          mem_nhds_iff.mpr ⟨Set.Ioi k, Set.Ioi_subset_Ici le_rfl, isOpen_Ioi, hk_lt_i⟩
        obtain ⟨a, ha⟩ : ∃ a : ℕ, ∀ b : ℕ, b ≥ a → k ≤ seq b := h_tendsto (Set.Ici k) h_nhds
        exact ⟨a, ha a le_rfl⟩
Cleared hypotheses: k, hk_lt_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 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
k : WithTop ι
h_exists_k_le_seq : ∃ (i : ℕ), k ≤ (↑(seq i) : WithTop ι)
⊢ k < (↑i : WithTop ι)
have h : ∀ (j : ℕ) (hk_seq_j : k ≤ (↑(seq j) : WithTop ι)), k < (↑i : WithTop ι)
Tactic: obtain ⟨j, hk_seq_j⟩ := h_exists_k_le_seq
Cleared hypotheses: h_exists_k_le_seq
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have h_Iio_eq_Union : Set.Iio (↑i : WithTop ι) = ⋃ (j : ℕ), {k : WithTop ι | k ≤ (↑(seq j) : WithTop ι)}
Tactic: have h_Iio_eq_Union : Set.Iio (i : WithTop ι) = ⋃ j, {k : WithTop ι | k ≤ seq j} := by
    ext1 k
    push _ ∈ _
    refine ⟨fun hk_lt_i => ?_, fun h_exists_k_le_seq => ?_⟩
    · rw [tendsto_atTop'] at h_tendsto
      cases k with
      | top => simp at hk_lt_i
      | coe k =>
        norm_cast at hk_lt_i ⊢
        have h_nhds : Set.Ici k ∈ 𝓝 i :=
          mem_nhds_iff.mpr ⟨Set.Ioi k, Set.Ioi_subset_Ici le_rfl, isOpen_Ioi, hk_lt_i⟩
        obtain ⟨a, ha⟩ : ∃ a : ℕ, ∀ b : ℕ, b ≥ a → k ≤ seq b := h_tendsto (Set.Ici k) h_nhds
        exact ⟨a, ha a le_rfl⟩
    · obtain ⟨j, hk_seq_j⟩ := h_exists_k_le_seq
      exact hk_seq_j.trans_lt (mod_cast h_bound 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 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
h_Iio_eq_Union : Set.Iio (↑i : WithTop ι) = ⋃ (j : ℕ), {k : WithTop ι | k ≤ (↑(seq j) : WithTop ι)}
⊢ {ω : Ω | τ ω < (↑i : WithTop ι)} = τ ⁻¹' Set.Iio (↑i : WithTop ι)
have h : ∀ (ω : Ω), Membership.mem (γ := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ω ↔ ω ∈ τ ⁻¹' Set.Iio (↑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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
h_Iio_eq_Union : Set.Iio (↑i : WithTop ι) = ⋃ (j : ℕ), {k : WithTop ι | k ≤ (↑(seq j) : WithTop ι)}
⊢ 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 := by
    ext1 ω; push _ ∈ _; 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
h_Iio_eq_Union : Set.Iio (↑i : WithTop ι) = ⋃ (j : ℕ), {k : WithTop ι | k ≤ (↑(seq j) : WithTop ι)}
h_lt_eq_preimage : {ω : Ω | τ ω < (↑i : WithTop ι)} = τ ⁻¹' Set.Iio (↑i : WithTop ι)
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have neg : MeasurableSet (τ ⁻¹' ⋃ (j : ℕ), {k : WithTop ι | k ≤ (↑(seq j) : WithTop ι)})
Tactic: rw [h_lt_eq_preimage, h_Iio_eq_Union]
-- 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 : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
h_Iio_eq_Union : Set.Iio (↑i : WithTop ι) = ⋃ (j : ℕ), {k : WithTop ι | k ≤ (↑(seq j) : WithTop ι)}
h_lt_eq_preimage : {ω : Ω | τ ω < (↑i : WithTop ι)} = τ ⁻¹' Set.Iio (↑i : WithTop ι)
⊢ MeasurableSet (τ ⁻¹' ⋃ (j : ℕ), {k : WithTop ι | k ≤ (↑(seq j) : WithTop ι)})
have neg : MeasurableSet.{u_1} (α := Ω) (⋃ (i : ℕ), {a : Ω | τ a ≤ (↑(seq i) : WithTop ι)})
Tactic: simp only [Set.preimage_iUnion, Set.preimage_setOf_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 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have obtain : ∀ (i' : ι) (hi'_lub : IsLUB (Set.Iio i) i'), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
Tactic: obtain ⟨i', hi'_lub⟩ : ∃ i', IsLUB (Set.Iio i) i' := exists_lub_Iio 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 : OrderTopology ι
inst_3 : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i i' : ι
hi'_lub : IsLUB (Set.Iio i) i'
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have inl : ∀ (hi'_eq_i : i' = i), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
Tactic: rcases lub_Iio_eq_self_or_Iio_eq_Iic i hi'_lub with hi'_eq_i | 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'
inl : ∀ (hi'_eq_i : i' = i), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
have inr : ∀ (h_Iio_eq_Iic : Set.Iio i = Set.Iic i'), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
Tactic: rcases lub_Iio_eq_self_or_Iio_eq_Iic i hi'_lub with hi'_eq_i | h_Iio_eq_Iic