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
u : WithTop ι
hu : (↑t : WithTop ι) < u
⊢ Tendsto (fun (n : ℕ) ↦ (↑(s n) : WithTop ι)) atTop (𝓝 (↑t : WithTop ι))

Tactic:
have hs_tendsto' : Tendsto (fun n ↦ (s n : WithTop ι)) atTop (𝓝 (t : WithTop ι)) :=
      WithTop.continuous_coe.continuousAt.tendsto.comp hs_tendsto
-- 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
u : WithTop ι
hu : (↑t : WithTop ι) < u
hs_tendsto' : Tendsto (fun (n : ℕ) ↦ (↑(s n) : WithTop ι)) atTop (𝓝 (↑t : WithTop ι))
⊢ ∀ᶠ (x : ℕ) in atTop, (↑(s x) : WithTop ι) < u

Tactic:
hs_tendsto'.eventually_lt_const hu

Premises used: Filter.Tendsto.eventually_lt_const
-- 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
u : WithTop ι
hu : (↑t : WithTop ι) < u
hs_tendsto' : Tendsto (fun (n : ℕ) ↦ (↑(s n) : WithTop ι)) atTop (𝓝 (↑t : WithTop ι))
⊢ ∀ᶠ (x : ℕ) in atTop, (↑(s x) : WithTop ι) < u

Tactic:
exact hs_tendsto'.eventually_lt_const hu

Premises used: Filter.Tendsto.eventually_lt_const
-- 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
⊢ ∀ (u : WithTop ι) (hu : (↑t : WithTop ι) < u), ∃ (i : ℕ), (↑(s i) : WithTop ι) < u

Tactic:
have h_exists_lt' (u : WithTop ι) (hu : t < u) : ∃ i, s i < u := by
    refine Eventually.exists (f := atTop) ?_
    have hs_tendsto' : Tendsto (fun n ↦ (s n : WithTop ι)) atTop (𝓝 (t : WithTop ι)) :=
      WithTop.continuous_coe.continuousAt.tendsto.comp hs_tendsto
    exact hs_tendsto'.eventually_lt_const hu
-- 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 :
  ∀ (ω : Ω),
    Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)} ω ↔
      Membership.mem (γ := Set Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)}) ω
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)} (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})

Tactic:
ext ω
-- 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 : τ ω ≤ (↑t : WithTop ι) ↔ ∀ (i : ℕ), τ ω < (↑(s i) : WithTop ι)
⊢ Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)} ω ↔
    Membership.mem (γ := Set Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)}) ω

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

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
ω : Ω
⊢ τ ω ≤ (↑t : WithTop ι) ↔ ∀ (i : ℕ), τ ω < (↑(s i) : WithTop ι)

Tactic:
⟨fun h_le m ↦ h_le.trans_lt (mod_cast (hs_gt m)), fun h_lt ↦ ?_⟩

Premises used: cast, WithTop.coe_lt_coe._simp_1, Iff.intro, Eq.symm, LE.le.trans_lt
-- 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 : ∀ (h_lt : ∀ (i : ℕ), τ ω < (↑(s i) : WithTop ι)), τ ω ≤ (↑t : WithTop ι)
⊢ τ ω ≤ (↑t : WithTop ι) ↔ ∀ (i : ℕ), τ ω < (↑(s i) : WithTop ι)

Tactic:
refine ⟨fun h_le m ↦ h_le.trans_lt (mod_cast (hs_gt m)), fun h_lt ↦ ?_⟩
-- 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_lt : ∀ (i : ℕ), τ ω < (↑(s i) : WithTop ι)
⊢ τ ω ≤ (↑t : WithTop ι)

Tactic:
le_of_forall_gt fun u hu ↦ ?_

Premises used: le_of_forall_gt
-- 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_lt : ∀ (i : ℕ), τ ω < (↑(s i) : WithTop ι)
h : ∀ (u : WithTop ι) (hu : (↑t : WithTop ι) < u), τ ω < u
⊢ τ ω ≤ (↑t : WithTop ι)

Tactic:
refine le_of_forall_gt fun u hu ↦ ?_

Premises used: le_of_forall_gt
-- 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_lt : ∀ (i : ℕ), τ ω < (↑(s i) : WithTop ι)
u : WithTop ι
hu : (↑t : WithTop ι) < u
⊢ ∃ (i : ℕ), (↑(s i) : WithTop ι) < u

Tactic:
h_exists_lt' u hu
-- 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_lt : ∀ (i : ℕ), τ ω < (↑(s i) : WithTop ι)
u : WithTop ι
hu : (↑t : WithTop ι) < u
h : ∀ (i : ℕ) (hi : (↑(s i) : WithTop ι) < u), τ ω < u
⊢ τ ω < u

Tactic:
obtain ⟨i, hi⟩ : ∃ i, s i < u := h_exists_lt' u hu
-- 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_lt : ∀ (i : ℕ), τ ω < (↑(s i) : WithTop ι)
u : WithTop ι
hu : (↑t : WithTop ι) < u
i : ℕ
hi : (↑(s i) : WithTop ι) < u
⊢ τ ω < u

Tactic:
(h_lt i).trans hi

Premises used: LT.lt.trans
-- 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_lt : ∀ (i : ℕ), τ ω < (↑(s i) : WithTop ι)
u : WithTop ι
hu : (↑t : WithTop ι) < u
i : ℕ
hi : (↑(s i) : WithTop ι) < u
⊢ τ ω < u

Tactic:
exact (h_lt i).trans hi

Premises used: LT.lt.trans
-- 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
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)} (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})

Tactic:
have h_eq_iInter : {ω | τ ω ≤ t} = ⋂ m, {ω | τ ω < s m} := by
    ext ω
    simp only [Set.mem_setOf_eq, Set.mem_iInter]
    refine ⟨fun h_le m ↦ h_le.trans_lt (mod_cast (hs_gt m)), fun h_lt ↦ ?_⟩
    refine le_of_forall_gt fun u hu ↦ ?_
    obtain ⟨i, hi⟩ : ∃ i, s i < u := h_exists_lt' u hu
    exact (h_lt i).trans hi
-- 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 ι)})
neg : MeasurableSet.{u_1} (α := Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}

Tactic:
rw [h_eq_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 ι)})
nth_rw :
  Eq.{u_1 + 1} (α := MeasurableSpace Ω) (⨅ (j : ι), ⨅ (_ : j > t), (↑f : ι → MeasurableSpace Ω) j)
    (⨅ (m_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1))
⊢ (↑f : ι → MeasurableSpace Ω) t = ⨅ (m_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1)

Tactic:
nth_rw 1 [← hf.eq, Filtration.rightCont_eq_of_neBot_nhdsGT]

Premises used: MeasureTheory.Filtration.IsRightContinuous.eq, MeasureTheory.Filtration.rightCont_eq_of_neBot_nhdsGT
-- 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 ι)})
⊢ Eq.{u_1 + 1} (α := MeasurableSpace Ω) (⨅ (j : ι), ⨅ (_ : j > t), (↑f : ι → MeasurableSpace Ω) j)
    (⨅ (m_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1))

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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 ι)})
refine_1 :
  LE.le.{u_1} (α := MeasurableSpace Ω) (⨅ (j : ι), ⨅ (_ : j > t), (↑f : ι → MeasurableSpace Ω) j)
    (⨅ (m_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1))
refine_2 :
  LE.le.{u_1} (α := MeasurableSpace Ω) (⨅ (m_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1))
    (⨅ (j : ι), ⨅ (_ : j > t), (↑f : ι → MeasurableSpace Ω) j)
⊢ Eq.{u_1 + 1} (α := MeasurableSpace Ω) (⨅ (j : ι), ⨅ (_ : j > t), (↑f : ι → MeasurableSpace Ω) j)
    (⨅ (m_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1))

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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 ι)})
refine_1 : ∀ (i : ℕ), ⨅ (j : ι), ⨅ (_ : t < j), (↑f : ι → MeasurableSpace Ω) j ≤ (↑f : ι → MeasurableSpace Ω) (s i)
⊢ LE.le.{u_1} (α := MeasurableSpace Ω) (⨅ (j : ι), ⨅ (_ : j > t), (↑f : ι → MeasurableSpace Ω) j)
    (⨅ (m_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1))

Tactic:
simp only [gt_iff_lt, le_iInf_iff]

Premises used: le_iInf_iff, gt_iff_lt
-- 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 : ℕ), ⨅ (j : ι), ⨅ (_ : t < j), (↑f : ι → MeasurableSpace Ω) j ≤ (↑f : ι → MeasurableSpace Ω) (s i)

Tactic:
fun i ↦ iInf₂_le (s i) (hs_gt i)

Premises used: 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 ι)})
⊢ ∀ (i : ℕ), ⨅ (j : ι), ⨅ (_ : t < j), (↑f : ι → MeasurableSpace Ω) j ≤ (↑f : ι → MeasurableSpace Ω) (s i)

Tactic:
exact fun i ↦ iInf₂_le (s i) (hs_gt i)

Premises used: 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 ι)})
refine_2 : ∀ (i : ι) (i_1 : t < i), ⨅ (m_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1) ≤ (↑f : ι → MeasurableSpace Ω) i
⊢ LE.le.{u_1} (α := MeasurableSpace Ω) (⨅ (m_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1))
    (⨅ (j : ι), ⨅ (_ : j > t), (↑f : ι → MeasurableSpace Ω) j)

Tactic:
simp only [gt_iff_lt, le_iInf_iff]

Premises used: le_iInf_iff, gt_iff_lt