awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
u : WithTop ι
hu : (↑t : WithTop ι) < u
⊢ ∀ᶠ (x : ℕ) in atTop, (↑(s x) : WithTop ι) < u
have hs_tendsto' : 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
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
have h_exists_lt' : ∀ (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
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
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 ι)})
have h : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)} ω ↔
    Membership.mem (γ := Set Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)}) ω
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
h_exists_lt' : ∀ (u : WithTop ι) (hu : (↑t : WithTop ι) < u), ∃ (i : ℕ), (↑(s i) : WithTop ι) < u
ω : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)} ω ↔
    Membership.mem (γ := Set Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)}) ω
have h : τ ω ≤ (↑t : WithTop ι) ↔ ∀ (i : ℕ), τ ω < (↑(s i) : WithTop ι)
Tactic: simp only [Set.mem_setOf_eq, Set.mem_iInter]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
h_exists_lt' : ∀ (u : WithTop ι) (hu : (↑t : WithTop ι) < u), ∃ (i : ℕ), (↑(s i) : WithTop ι) < u
ω : Ω
⊢ τ ω ≤ (↑t : WithTop ι) ↔ ∀ (i : ℕ), τ ω < (↑(s i) : WithTop ι)
have h : ∀ (h_lt : ∀ (i : ℕ), τ ω < (↑(s i) : WithTop ι)), τ ω ≤ (↑t : WithTop ι)
Tactic: refine ⟨fun h_le m ↦ h_le.trans_lt (mod_cast (hs_gt m)), fun h_lt ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
h_exists_lt' : ∀ (u : WithTop ι) (hu : (↑t : WithTop ι) < u), ∃ (i : ℕ), (↑(s i) : WithTop ι) < u
ω : Ω
h_lt : ∀ (i : ℕ), τ ω < (↑(s i) : WithTop ι)
⊢ τ ω ≤ (↑t : WithTop ι)
have h : ∀ (u : WithTop ι) (hu : (↑t : WithTop ι) < u), τ ω < u
Tactic: refine le_of_forall_gt fun u hu ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
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
⊢ τ ω < u
have h : ∀ (i : ℕ) (hi : (↑(s i) : WithTop ι) < u), τ ω < u
Tactic: obtain ⟨i, hi⟩ : ∃ i, s i < u := h_exists_lt' u hu
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
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
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
have h_eq_iInter : 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
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
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 ι)})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑t : WithTop ι)}
have neg : MeasurableSet.{u_1} (α := Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
Tactic: rw [h_eq_iInter]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
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)
have nth_rw : Eq.{u_1 + 1} (α := MeasurableSpace Ω) (⨅ (j : ι), ⨅ (_ : j > t), (↑f : ι → MeasurableSpace Ω) j)
  (⨅ (m_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1))
Tactic: nth_rw 1 [← hf.eq, Filtration.rightCont_eq_of_neBot_nhdsGT]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
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))
have refine_1 : LE.le.{u_1} (α := MeasurableSpace Ω) (⨅ (j : ι), ⨅ (_ : j > t), (↑f : ι → MeasurableSpace Ω) j)
  (⨅ (m_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
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))
⊢ Eq.{u_1 + 1} (α := MeasurableSpace Ω) (⨅ (j : ι), ⨅ (_ : j > t), (↑f : ι → MeasurableSpace Ω) j)
    (⨅ (m_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1))
have refine_2 : LE.le.{u_1} (α := MeasurableSpace Ω) (⨅ (m_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1))
  (⨅ (j : ι), ⨅ (_ : j > t), (↑f : ι → MeasurableSpace Ω) j)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
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 ι)})
⊢ LE.le.{u_1} (α := MeasurableSpace Ω) (⨅ (j : ι), ⨅ (_ : j > t), (↑f : ι → MeasurableSpace Ω) j)
    (⨅ (m_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1))
have refine_1 : ∀ (i : ℕ), ⨅ (j : ι), ⨅ (_ : t < j), (↑f : ι → MeasurableSpace Ω) j ≤ (↑f : ι → MeasurableSpace Ω) (s i)
Tactic: simp only [gt_iff_lt, le_iInf_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
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 ι)})
⊢ LE.le.{u_1} (α := MeasurableSpace Ω) (⨅ (m_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1))
    (⨅ (j : ι), ⨅ (_ : j > t), (↑f : ι → MeasurableSpace Ω) j)
have refine_2 : ∀ (i : ι) (i_1 : t < i), ⨅ (m_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1) ≤ (↑f : ι → MeasurableSpace Ω) i
Tactic: simp only [gt_iff_lt, le_iInf_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
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_1 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_1) ≤ (↑f : ι → MeasurableSpace Ω) i
have refine_2 : ∀ (m_1 : ℕ) (hm : s m_1 < i), ⨅ (m_2 : ℕ), (↑f : ι → MeasurableSpace Ω) (s m_2) ≤ (↑f : ι → MeasurableSpace Ω) i
Tactic: obtain ⟨m, hm⟩ := h_exists_lt i hti
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
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 ι)})
⊢ MeasurableSet.{u_1} (α := Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
have h𝓕_eq_iInf : (↑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)
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
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)
⊢ MeasurableSet.{u_1} (α := Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
have neg : MeasurableSet.{u_1} (α := Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
Tactic: rw [h𝓕_eq_iInf]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
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)
⊢ MeasurableSet.{u_1} (α := Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
have neg : ∀ (a : ℕ), MeasurableSet.{u_1} (α := Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)})
Tactic: simp only [MeasurableSpace.measurableSet_sInf, Set.mem_range, forall_exists_index,
    forall_apply_eq_imp_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
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 ι)})
have h : ∀ (x : Ω),
  Membership.mem (γ := Set Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)}) x ↔
    Membership.mem (γ := Set Ω) (⋂ (m : ℕ), ⋂ (_ : s m ≤ s k), {ω : Ω | τ ω < (↑(s m) : WithTop ι)}) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω < (↑i : WithTop ι)}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = (↑i : WithTop ι)}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι) (hu : t < u), ∃ (i : ℕ), s i < u
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 : Ω
⊢ Membership.mem (γ := Set Ω) (⋂ (m : ℕ), {ω : Ω | τ ω < (↑(s m) : WithTop ι)}) x ↔
    Membership.mem (γ := Set Ω) (⋂ (m : ℕ), ⋂ (_ : s m ≤ s k), {ω : Ω | τ ω < (↑(s m) : WithTop ι)}) x
have h : (∀ (i : ℕ), τ x < (↑(s i) : WithTop ι)) ↔ ∀ (i : ℕ) (i_1 : s i ≤ s k), τ x < (↑(s i) : WithTop ι)
Tactic: simp only [Set.mem_iInter, Set.mem_setOf_eq]