awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Stopping
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
⊢ ∃ (a : ℕ), ∀ b ≥ a, k ≤ seq b

Tactic:
h_tendsto (Set.Ici k) h_nhds

Premises used: Set.Ici, Set.Mem, setOf
-- Module: Mathlib.Probability.Process.Stopping
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
h : ∀ (a : ℕ) (ha : ∀ b ≥ a, k ≤ seq b), ∃ (i : ℕ), k ≤ seq i
⊢ ∃ (i : ℕ), k ≤ seq i

Tactic:
obtain ⟨a, ha⟩ : ∃ a : ℕ, ∀ b : ℕ, b ≥ a → k ≤ seq b := h_tendsto (Set.Ici k) h_nhds

Premises used: Set.Ici
-- Module: Mathlib.Probability.Process.Stopping
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
a : ℕ
ha : ∀ b ≥ a, k ≤ seq b
⊢ ∃ (i : ℕ), k ≤ seq i

Tactic:
⟨a, ha a le_rfl⟩

Premises used: le_rfl, Exists.intro
-- Module: Mathlib.Probability.Process.Stopping
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
a : ℕ
ha : ∀ b ≥ a, k ≤ seq b
⊢ ∃ (i : ℕ), k ≤ seq i

Tactic:
exact ⟨a, ha a le_rfl⟩
-- Module: Mathlib.Probability.Process.Stopping
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 ι)
h₁ : ∀ (k : ι) (hk_lt_i : (↑k : WithTop ι) < (↑i : WithTop ι)), ∃ (i : ℕ), (↑k : WithTop ι) ≤ (↑(seq i) : WithTop ι)
⊢ ∃ (i : ℕ), k ≤ (↑(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⟩

Premises used: WithTop.top, WithTop.coe
-- Module: Mathlib.Probability.Process.Stopping
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 ι)
h : ∀ (j : ℕ) (hk_seq_j : k ≤ (↑(seq j) : WithTop ι)), k < (↑i : WithTop ι)
⊢ k < (↑i : WithTop ι)

Tactic:
obtain ⟨j, hk_seq_j⟩ := h_exists_k_le_seq
-- Module: Mathlib.Probability.Process.Stopping
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 ι
j : ℕ
hk_seq_j : k ≤ (↑(seq j) : WithTop ι)
⊢ k < (↑i : WithTop ι)

Tactic:
hk_seq_j.trans_lt (mod_cast h_bound j)

Premises used: cast, WithTop.coe_lt_coe._simp_1, Eq.symm, LE.le.trans_lt
-- Module: Mathlib.Probability.Process.Stopping
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 ι
j : ℕ
hk_seq_j : k ≤ (↑(seq j) : WithTop ι)
⊢ k < (↑i : WithTop ι)

Tactic:
exact hk_seq_j.trans_lt (mod_cast h_bound j)

Premises used: LE.le.trans_lt
-- Module: Mathlib.Probability.Process.Stopping
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 ι)}

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)
-- Module: Mathlib.Probability.Process.Stopping
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 : ∀ (ω : Ω), Membership.mem (γ := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)} ω ↔ ω ∈ τ ⁻¹' Set.Iio (↑i : WithTop ι)
⊢ {ω : Ω | τ ω < (↑i : WithTop ι)} = τ ⁻¹' Set.Iio (↑i : WithTop ι)

Tactic:
ext1 ω
-- Module: Mathlib.Probability.Process.Stopping
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 ι) ↔ τ ω < (↑i : WithTop ι)

Tactic:
rfl
-- Module: Mathlib.Probability.Process.Stopping
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 ι)

Tactic:
have h_lt_eq_preimage : {ω | τ ω < i} = τ ⁻¹' Set.Iio i := by
    ext1 ω; push _ ∈ _; rfl
-- Module: Mathlib.Probability.Process.Stopping
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 ι)
neg : MeasurableSet (τ ⁻¹' ⋃ (j : ℕ), {k : WithTop ι | k ≤ (↑(seq j) : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}

Tactic:
rw [h_lt_eq_preimage, h_Iio_eq_Union]
-- Module: Mathlib.Probability.Process.Stopping
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 ι)
neg : MeasurableSet.{u_1} (α := Ω) (⋃ (i : ℕ), {a : Ω | τ a ≤ (↑(seq i) : WithTop ι)})
⊢ MeasurableSet (τ ⁻¹' ⋃ (j : ℕ), {k : WithTop ι | k ≤ (↑(seq j) : WithTop ι)})

Tactic:
simp only [Set.preimage_iUnion, Set.preimage_setOf_eq]

Premises used: Set.preimage_setOf_eq, Set.preimage_iUnion
-- Module: Mathlib.Probability.Process.Stopping
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 : ℕ), {a : Ω | τ a ≤ (↑(seq i) : WithTop ι)})

Tactic:
MeasurableSet.iUnion fun n => f.mono (h_bound n).le _ (hτ.measurableSet_le (seq n))

Premises used: setOf, MeasureTheory.IsStoppingTime.measurableSet_le, LT.lt.le, LE.le, WithTop.some, MeasureTheory.Filtration.mono, MeasurableSet.iUnion
-- Module: Mathlib.Probability.Process.Stopping
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 : ℕ), {a : Ω | τ a ≤ (↑(seq i) : WithTop ι)})

Tactic:
exact MeasurableSet.iUnion fun n => f.mono (h_bound n).le _ (hτ.measurableSet_le (seq n))

Premises used: setOf, MeasureTheory.IsStoppingTime.measurableSet_le, LT.lt.le, LE.le, WithTop.some, MeasureTheory.Filtration.mono, MeasurableSet.iUnion
-- Module: Mathlib.Probability.Process.Stopping
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' : ι), IsLUB (Set.Iio i) i'

Tactic:
exists_lub_Iio i

Premises used: exists_lub_Iio
-- Module: Mathlib.Probability.Process.Stopping
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 : ι
obtain : ∀ (i' : ι) (hi'_lub : IsLUB (Set.Iio i) i'), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}

Tactic:
obtain ⟨i', hi'_lub⟩ : ∃ i', IsLUB (Set.Iio i) i' := exists_lub_Iio i

Premises used: exists_lub_Iio
-- Module: Mathlib.Probability.Process.Stopping
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 ι)}
inr : ∀ (h_Iio_eq_Iic : Set.Iio i = Set.Iic i'), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
⊢ 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

Premises used: lub_Iio_eq_self_or_Iio_eq_Iic
-- Module: Mathlib.Probability.Process.Stopping
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
inl :
  ∀ (hi'_lub : IsLUB (Set.Iio i') i') (hi'_eq_i : i' = i),
    MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i' : WithTop ι)}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}

Tactic:
rw [← hi'_eq_i] at hi'_lub ⊢
-- Module: Mathlib.Probability.Process.Stopping
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 ι)}

Tactic:
hτ.measurableSet_lt_of_isLUB i' hi'_lub

Premises used: MeasureTheory.IsStoppingTime.measurableSet_lt_of_isLUB
-- Module: Mathlib.Probability.Process.Stopping
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 ι)}

Tactic:
exact hτ.measurableSet_lt_of_isLUB i' hi'_lub

Premises used: MeasureTheory.IsStoppingTime.measurableSet_lt_of_isLUB
-- Module: Mathlib.Probability.Process.Stopping
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'
⊢ {ω : Ω | τ ω < (↑i : WithTop ι)} = τ ⁻¹' Set.Iio (↑i : WithTop ι)

Tactic:
have h_lt_eq_preimage : {ω : Ω | τ ω < i} = τ ⁻¹' Set.Iio i := rfl
-- Module: Mathlib.Probability.Process.Stopping
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'
rw₂ rw₃ : WithTop.some '' Set.Iic i' = WithTop.some '' Set.Iic i'
⊢ Set.Iio (↑i : WithTop ι) = Set.Iic (↑i' : WithTop ι)

Tactic:
rw [← image_coe_Iio, ← image_coe_Iic, h_Iio_eq_Iic]

Premises used: WithTop.image_coe_Iic, WithTop.image_coe_Iio
-- Module: Mathlib.Probability.Process.Stopping
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 ι)

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]
-- Module: Mathlib.Probability.Process.Stopping
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 ι)
inr : MeasurableSet (τ ⁻¹' Set.Iic (↑i' : WithTop ι))
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}

Tactic:
rw [h_lt_eq_preimage, h_Iio_eq_Iic']
-- Module: Mathlib.Probability.Process.Stopping
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 (τ ⁻¹' Set.Iic (↑i' : WithTop ι))

Tactic:
f.mono (le_of_isLUB_Iio i hi'_lub) _ (hτ.measurableSet_le i')

Premises used: le_of_isLUB_Iio, MeasureTheory.IsStoppingTime.measurableSet_le, MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Process.Stopping
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 (τ ⁻¹' Set.Iic (↑i' : WithTop ι))

Tactic:
exact f.mono (le_of_isLUB_Iio i hi'_lub) _ (hτ.measurableSet_le i')

Premises used: le_of_isLUB_Iio, MeasureTheory.IsStoppingTime.measurableSet_le, MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Process.Stopping
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 :
  ∀ (ω : Ω),
    Membership.mem (γ := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω} ω ↔
      Membership.mem (γ := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}ᶜ ω
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω} {ω : Ω | τ ω < (↑i : WithTop ι)}ᶜ

Tactic:
ext1 ω
-- Module: Mathlib.Probability.Process.Stopping
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 : ι
ω : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω} ω ↔
    Membership.mem (γ := Set Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}ᶜ ω

Tactic:
simp only [Set.mem_setOf_eq, Set.mem_compl_iff, not_lt]

Premises used: Set.mem_setOf_eq, not_lt, Set.mem_compl_iff
-- Module: Mathlib.Probability.Process.Stopping
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 ι)}ᶜ

Tactic:
have : {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ := by
    ext1 ω; simp only [Set.mem_setOf_eq, Set.mem_compl_iff, not_lt]
-- Module: Mathlib.Probability.Process.Stopping
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 ι)}ᶜ
rw : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}ᶜ
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | (↑i : WithTop ι) ≤ τ ω}

Tactic:
rw [this]
-- Module: Mathlib.Probability.Process.Stopping
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 ι)}ᶜ

Tactic:
(hτ.measurableSet_lt i).compl

Premises used: MeasureTheory.IsStoppingTime.measurableSet_lt, MeasurableSet.compl
-- Module: Mathlib.Probability.Process.Stopping
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 ι)}ᶜ

Tactic:
exact (hτ.measurableSet_lt i).compl

Premises used: MeasureTheory.IsStoppingTime.measurableSet_lt, MeasurableSet.compl
-- Module: Mathlib.Probability.Process.Stopping
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 :
  ∀ (ω : Ω),
    Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} ω ↔
      Membership.mem (γ := Set Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≥ (↑i : WithTop ι)}) ω
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
    ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≥ (↑i : WithTop ι)})

Tactic:
ext1 ω
-- Module: Mathlib.Probability.Process.Stopping
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 : ι
ω : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} ω ↔
    Membership.mem (γ := Set Ω) ({ω : Ω | τ ω ≤ (↑i : WithTop ι)} ∩ {ω : Ω | τ ω ≥ (↑i : WithTop ι)}) ω

Tactic:
simp only [Set.mem_setOf_eq, Set.mem_inter_iff, le_antisymm_iff]

Premises used: Set.mem_inter_iff, Set.mem_setOf_eq, le_antisymm_iff
-- Module: Mathlib.Probability.Process.Stopping
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 ι)})

Tactic:
have : {ω | τ ω = i} = {ω | τ ω ≤ i} ∩ {ω | τ ω ≥ i} := by
    ext1 ω; simp only [Set.mem_setOf_eq, Set.mem_inter_iff, le_antisymm_iff]