awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Stopping
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 ι)})
i : ι
hti : t < i
refine_2 :
  ∀ (m_1 : ℕ) (hm : s m_1 < i), ⨅ (m_2 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_2) ≤ (↑f : ι → MeasurableSpace Ω) i
⊢ ⨅ (m_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1) ≤ (↑f : ι → MeasurableSpace Ω) i

Tactic:
obtain ⟨m, hm⟩ := h_exists_lt i hti
-- Module: Mathlib.Probability.Process.Stopping
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 ι)})
i : ι
hti : t < i
m : ℕ
hm : s m < i
⊢ ⨅ (m : ℕ), (↑f : ι → MeasurableSpace Ω) (s m) ≤ (↑f : ι → MeasurableSpace Ω) i

Tactic:
(iInf_le _ m).trans (f.mono hm.le)

Premises used: LT.lt.le, MeasureTheory.Filtration.mono, LE.le.trans, iInf_le
-- Module: Mathlib.Probability.Process.Stopping
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 ι)})
i : ι
hti : t < i
m : ℕ
hm : s m < i
⊢ ⨅ (m : ℕ), (↑f : ι → MeasurableSpace Ω) (s m) ≤ (↑f : ι → MeasurableSpace Ω) i

Tactic:
exact (iInf_le _ m).trans (f.mono hm.le)

Premises used: LE.le.trans, iInf_le
-- Module: Mathlib.Probability.Process.Stopping
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 ι)})
⊢ (↑f : ι → MeasurableSpace Ω) t = ⨅ (m_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1)

Tactic:
have h𝓕_eq_iInf : f t = ⨅ m, f (s m) := by
    nth_rw 1 [← hf.eq, Filtration.rightCont_eq_of_neBot_nhdsGT]
    refine le_antisymm ?_ ?_
    · simp only [gt_iff_lt, le_iInf_iff]
      exact fun i ↦ iInf₂_le (s i) (hs_gt i)
    · simp only [gt_iff_lt, le_iInf_iff]
      intro i hti
      obtain ⟨m, hm⟩ := h_exists_lt i hti
      exact (iInf_le _ m).trans (f.mono hm.le)
-- Module: Mathlib.Probability.Process.Stopping
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)
neg : MeasurableSet.{u_1} (α := Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})

Tactic:
rw [h𝓕_eq_iInf]
-- Module: Mathlib.Probability.Process.Stopping
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)
neg : ∀ (a : ℕ), MeasurableSet.{u_1} (α := Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})

Tactic:
simp only [MeasurableSpace.measurableSet_sInf, Set.mem_range, forall_exists_index,
    forall_apply_eq_imp_iff]

Premises used: Set.mem_range, forall_exists_index, MeasurableSpace.measurableSet_sInf, forall_apply_eq_imp_iff
-- Module: Mathlib.Probability.Process.Stopping
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 :
  ∀ (x : Ω),
    Membership.mem (γ := Set Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)}) x ↔
      Membership.mem (γ := Set Ω) (⋂ (m : ℕ), ⋂ (_ : s m ≤ s k), {ω : Ω | τ ω < (↑(s m) : WithTop ι)}) x
⊢ Eq.{u_1 + 1} (α := Set Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
    (⋂ (m : ℕ), ⋂ (_ : s m ≤ s k), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})

Tactic:
ext x
-- Module: Mathlib.Probability.Process.Stopping
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 : Ω
h : (∀ (i : ℕ), τ x < (↑(s i) : WithTop ι)) ↔ ∀ (i : ℕ) (i_1 : s i ≤ s k), τ x < (↑(s i) : WithTop ι)
⊢ Membership.mem (γ := Set Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)}) x ↔
    Membership.mem (γ := Set Ω) (⋂ (m : ℕ), ⋂ (_ : s m ≤ s k), {ω : Ω | τ ω < (↑(s m) : WithTop ι)}) x

Tactic:
simp only [Set.mem_iInter, Set.mem_setOf_eq]

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

Tactic:
⟨fun h m _ ↦ h m, fun h m ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Probability.Process.Stopping
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 : Ω
h : ∀ (h : ∀ (i : ℕ) (i_1 : s i ≤ s k), τ x < (↑(s i) : WithTop ι)) (m : ℕ), τ x < (↑(s m) : WithTop ι)
⊢ (∀ (i : ℕ), τ x < (↑(s i) : WithTop ι)) ↔ ∀ (i : ℕ) (i_1 : s i ≤ s k), τ x < (↑(s i) : WithTop ι)

Tactic:
refine ⟨fun h m _ ↦ h m, fun h m ↦ ?_⟩
-- Module: Mathlib.Probability.Process.Stopping
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 ι)
h₂ : ∀ (hkm : s k ≤ s m), τ x < (↑(s m) : WithTop ι)
⊢ τ x < (↑(s m) : WithTop ι)

Tactic:
rcases le_total (s m) (s k) with hmk | hkm

Premises used: le_total
-- Module: Mathlib.Probability.Process.Stopping
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 : ℕ
hmk : s m ≤ s k
⊢ τ x < (↑(s m) : WithTop ι)

Tactic:
h m hmk
-- Module: Mathlib.Probability.Process.Stopping
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 : ℕ
hmk : s m ≤ s k
⊢ τ x < (↑(s m) : WithTop ι)

Tactic:
exact h m hmk
-- Module: Mathlib.Probability.Process.Stopping
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 : ℕ
hkm : s k ≤ s m
⊢ τ x < (↑(s m) : WithTop ι)

Tactic:
(h k le_rfl).trans_le (mod_cast hkm)

Premises used: le_rfl, WithTop.coe_le_coe._simp_1, cast, LT.lt.trans_le, Eq.symm
-- Module: Mathlib.Probability.Process.Stopping
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 : ℕ
hkm : s k ≤ s m
⊢ τ x < (↑(s m) : WithTop ι)

Tactic:
exact (h k le_rfl).trans_le (mod_cast hkm)

Premises used: le_rfl, LT.lt.trans_le
-- Module: Mathlib.Probability.Process.Stopping
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 : ℕ
⊢ 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)
-- Module: Mathlib.Probability.Process.Stopping
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 ι)})
neg : MeasurableSet.{u_1} (α := Ω) (⋂ (m : ℕ), ⋂ (_ : s m ≤ s k), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})

Tactic:
rw [h_eq_k]
-- Module: Mathlib.Probability.Process.Stopping
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 ≤ s k), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})

Tactic:
MeasurableSet.iInter fun m ↦ MeasurableSet.iInter fun hm ↦ f.mono hm _ (hτ1 (s m))

Premises used: setOf, WithTop.some, LT.lt, MeasureTheory.Filtration.mono, MeasurableSet.iInter
-- Module: Mathlib.Probability.Process.Stopping
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 ≤ s k), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})

Tactic:
exact MeasurableSet.iInter fun m ↦ MeasurableSet.iInter fun hm ↦ f.mono hm _ (hτ1 (s m))

Premises used: setOf, WithTop.some, LT.lt, MeasureTheory.Filtration.mono, MeasurableSet.iInter
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
inst_4 : DenselyOrdered ι
inst_5 : NoMaxOrder ι
τ : Ω → WithTop ι
inst_6 : f.IsRightContinuous
hτ : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
⊢ IsStoppingTime f τ

Tactic:
isStoppingTime_of_measurableSet_lt_of_isRightContinuous' hτ
    <| fun _ hi ↦ absurd hi (NeBot.ne inferInstance)

Premises used: Filter.NeBot.ne, MeasureTheory.isStoppingTime_of_measurableSet_lt_of_isRightContinuous', inferInstance, absurd