awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (hypothesis)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : DenselyOrdered ι
inst_4 : FirstCountableTopology ι
inst_5 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
inst_6 : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
ω : Ω
hω : Eq.{u_1 + 1} (α := WithTop ι) (liminf (fun (x : ℕ) ↦ τ x ω) atTop) ⊤
⊢ Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ ⨅ (j : ℕ), ⨅ (_ : j ≥ x), τ j ω) atTop (𝓝 ⊤)
have hω₁ : Eq.{u_1 + 1} (α := WithTop ι) (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), τ i ω) ⊤
Tactic: rw [liminf_eq_iSup_iInf_of_nat] at hω
Cleared hypotheses: hω
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : DenselyOrdered ι
inst_4 : FirstCountableTopology ι
inst_5 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
inst_6 : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
ω : Ω
hω : Eq.{u_1 + 1} (α := WithTop ι) (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), τ i ω) ⊤
⊢ Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ ⨅ (j : ℕ), ⨅ (_ : j ≥ x), τ j ω) atTop (𝓝 ⊤)
have h : Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ ⨅ (j : ℕ), ⨅ (_ : j ≥ x), τ j ω) atTop
  (𝓝 (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), τ i ω))
Tactic: rw [← hω]
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : DenselyOrdered ι
inst_4 : FirstCountableTopology ι
inst_5 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
inst_6 : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
ω : Ω
hω : Eq.{u_1 + 1} (α := WithTop ι) (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), τ i ω) ⊤
⊢ Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ ⨅ (j : ℕ), ⨅ (_ : j ≥ x), τ j ω) atTop
    (𝓝 (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), τ i ω))
have h : ∀ (n m : ℕ) (hnm : n ≤ m),
  LE.le.{u_1} (α := WithTop ι) (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω) (⨅ (j : ℕ), ⨅ (_ : j ≥ m), τ j ω)
Tactic: refine tendsto_atTop_iSup fun n m hnm ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : DenselyOrdered ι
inst_4 : FirstCountableTopology ι
inst_5 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
inst_6 : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
ω : Ω
hω : Eq.{u_1 + 1} (α := WithTop ι) (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), τ i ω) ⊤
n m : ℕ
hnm : n ≤ m
⊢ LE.le.{u_1} (α := WithTop ι) (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω) (⨅ (j : ℕ), ⨅ (_ : j ≥ m), τ j ω)
have h : ∀ (i : ℕ) (i_1 : m ≤ i) (b : WithTop ι), (∀ (i : ℕ) (i_2 : n ≤ i), b ≤ τ i ω) → b ≤ τ i ω
Tactic: simp [iInf_le_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst_3 : Zero E
inst_4 : DenselyOrdered ι
inst_5 : FirstCountableTopology ι
inst_6 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
hp : IsStable (mΩ := mΩ) 𝓕 p
inst_7 : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
hpτ : ∀ (n : ℕ), p (stoppedProcess (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < τ n ω} (X i)) (τ n))
⊢ Locally p 𝓕 X P
have refine : ∀ (n : ℕ),
  p
    (stoppedProcess
      (fun (i : ι) ↦ Set.indicator {ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)} (X i))
      fun (ω : Ω) ↦ ⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)
Tactic: refine ⟨_, hτ.isLocalizingSequence_biInf, fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst_3 : Zero E
inst_4 : DenselyOrdered ι
inst_5 : FirstCountableTopology ι
inst_6 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
hp : IsStable (mΩ := mΩ) 𝓕 p
inst_7 : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
hpτ : ∀ (n : ℕ), p (stoppedProcess (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < τ n ω} (X i)) (τ n))
n : ℕ
⊢ p
    (stoppedProcess
      (fun (i : ι) ↦ Set.indicator {ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)} (X i))
      fun (ω : Ω) ↦ ⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)
have rw : p
  (stoppedProcess
    (fun (i : ι) ↦
      Set.indicator {ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)}
        (stoppedProcess X (fun (ω : Ω) ↦ τ n ω) i))
    fun (x : Ω) ↦ ⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j x)
Tactic: rw [stoppedProcess_indicator_comm', ← stoppedProcess_stoppedProcess_of_le_right
    (τ := fun ω ↦ τ n ω) (fun _ ↦ (iInf_le _ n).trans <| iInf_le _ le_rfl),
    ← stoppedProcess_indicator_comm']
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst_3 : Zero E
inst_4 : DenselyOrdered ι
inst_5 : FirstCountableTopology ι
inst_6 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
hp : IsStable (mΩ := mΩ) 𝓕 p
inst_7 : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
hpτ : ∀ (n : ℕ), p (stoppedProcess (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < τ n ω} (X i)) (τ n))
n : ℕ
⊢ p
    (stoppedProcess
      (fun (i : ι) ↦
        Set.indicator {ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)}
          (stoppedProcess X (fun (ω : Ω) ↦ τ n ω) i))
      fun (x : Ω) ↦ ⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j x)
have h : Eq (α := ι → Ω → E)
  (fun (i : ι) ↦
    Set.indicator {ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)}
      (stoppedProcess X (fun (ω : Ω) ↦ τ n ω) i))
  fun (i : ι) ↦
  Set.indicator {ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)}
    (stoppedProcess (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < τ n ω} (X i)) (τ n) i)
Tactic: convert!
    hp _ (hpτ n) (fun ω ↦ ⨅ j ≥ n, τ j ω) <| hτ.isLocalizingSequence_biInf.isStoppingTime n using 2
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst_3 : Zero E
inst_4 : DenselyOrdered ι
inst_5 : FirstCountableTopology ι
inst_6 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
hp : IsStable (mΩ := mΩ) 𝓕 p
inst_7 : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
hpτ : ∀ (n : ℕ), p (stoppedProcess (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < τ n ω} (X i)) (τ n))
n : ℕ
⊢ Eq (α := ι → Ω → E)
    (fun (i : ι) ↦
      Set.indicator {ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)}
        (stoppedProcess X (fun (ω : Ω) ↦ τ n ω) i))
    fun (i : ι) ↦
    Set.indicator {ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)}
      (stoppedProcess (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < τ n ω} (X i)) (τ n) i)
have h : ∀ (i : ι) (ω : Ω),
  Set.indicator {ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)}
      (stoppedProcess X (fun (ω : Ω) ↦ τ n ω) i) ω =
    Set.indicator {ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)}
      (stoppedProcess (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < τ n ω} (X i)) (τ n) i) ω
Tactic: ext i ω
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst_3 : Zero E
inst_4 : DenselyOrdered ι
inst_5 : FirstCountableTopology ι
inst_6 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
hp : IsStable (mΩ := mΩ) 𝓕 p
inst_7 : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
hpτ : ∀ (n : ℕ), p (stoppedProcess (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < τ n ω} (X i)) (τ n))
n : ℕ
i : ι
ω : Ω
⊢ Set.indicator {ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)}
      (stoppedProcess X (fun (ω : Ω) ↦ τ n ω) i) ω =
    Set.indicator {ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)}
      (stoppedProcess (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < τ n ω} (X i)) (τ n) i) ω
have h : Set.indicator {ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)}
    (stoppedProcess X (fun (ω : Ω) ↦ τ n ω) i) ω =
  Set.indicator ({ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)} ∩ {ω : Ω | ⊥ < τ n ω})
    (stoppedProcess X (τ n) i) ω
Tactic: rw [stoppedProcess_indicator_comm', Set.indicator_indicator]
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst_3 : Zero E
inst_4 : DenselyOrdered ι
inst_5 : FirstCountableTopology ι
inst_6 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
hp : IsStable (mΩ := mΩ) 𝓕 p
inst_7 : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
hpτ : ∀ (n : ℕ), p (stoppedProcess (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < τ n ω} (X i)) (τ n))
n : ℕ
i : ι
ω : Ω
⊢ Set.indicator {ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)}
      (stoppedProcess X (fun (ω : Ω) ↦ τ n ω) i) ω =
    Set.indicator ({ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)} ∩ {ω : Ω | ⊥ < τ n ω})
      (stoppedProcess X (τ n) i) ω
have h : ∀ (ω : Ω),
  LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω) ↔
    ({ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)} ∩ {ω : Ω | ⊥ < τ n ω}) ω
Tactic: congr with ω
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
⊢ ∃ (T : ℕ → ι),
    Tendsto T atTop atTop ∧
      ∀ (n : ℕ), ∃ (k : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
have obtain : ∀ (T : ℕ → ι) (hT : Tendsto T atTop atTop),
  ∃ (T : ℕ → ι),
    Tendsto T atTop atTop ∧
      ∀ (n : ℕ), ∃ (k : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
Tactic: obtain ⟨T, -, hT⟩ := Filter.exists_seq_monotone_tendsto_atTop_atTop ι
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
⊢ ∃ (T : ℕ → ι),
    Tendsto T atTop atTop ∧
      ∀ (n : ℕ), ∃ (k : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
have refine : ∀ (n : ℕ), ∃ (k : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
Tactic: refine ⟨T, hT, fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
⊢ ∃ (k : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
have by_contra! : ∀ (hn : ∀ (k : ℕ), (1 / 2) ^ n < (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}), False
Tactic: by_contra! hn
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}
this : (1 / 2) ^ n ≤ (P : (a : Set Ω) → ℝ≥0∞) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)})
⊢ False
have refine : Eq (α := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}) : ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: refine (by simp : ¬ (1 / 2 : ℝ≥0∞) ^ n ≤ 0) <| this.trans <| nonpos_iff_eq_zero.2 ?_
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}
this : (1 / 2) ^ n ≤ (P : (a : Set Ω) → ℝ≥0∞) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)})
⊢ Eq (α := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have rw : ∀ᵐ (a : Ω) ∂P, a ∉ ⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}
Tactic: rw [measure_eq_zero_iff_ae_notMem]
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}
this : (1 / 2) ^ n ≤ (P : (a : Set Ω) → ℝ≥0∞) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)})
⊢ ∀ᵐ (a : Ω) ∂P, a ∉ ⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}
have h : ∀ (ω : Ω) (hTop : Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ σ n x ω) atTop (𝓝 ⊤))
  (hmem : Membership.mem (γ := Set Ω) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}) ω), False
Tactic: filter_upwards [(hσ n).tendsto_top] with ω hTop hmem
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (hypothesis)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}
this : (1 / 2) ^ n ≤ (P : (a : Set Ω) → ℝ≥0∞) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)})
ω : Ω
hTop : Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ σ n x ω) atTop (𝓝 ⊤)
hmem : Membership.mem (γ := Set Ω) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}) ω
⊢ False
have hTop₁ : ∀ (i : ι), ∃ (a : ℕ), ∀ b ≥ a, (↑i : WithTop ι) < σ n b ω
Tactic: simp_rw [WithTop.tendsto_nhds_top_iff, eventually_atTop] at hTop
Cleared hypotheses: hTop
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (hypothesis)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}
this : (1 / 2) ^ n ≤ (P : (a : Set Ω) → ℝ≥0∞) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)})
ω : Ω
hmem : Membership.mem (γ := Set Ω) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}) ω
hTop : ∀ (i : ι), ∃ (a : ℕ), ∀ b ≥ a, (↑i : WithTop ι) < σ n b ω
⊢ False
have hmem₁ : ∀ (i : ℕ), σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)
Tactic: simp only [Set.mem_iInter, Set.mem_setOf_eq] at hmem
Cleared hypotheses: hmem
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}
this : (1 / 2) ^ n ≤ (P : (a : Set Ω) → ℝ≥0∞) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)})
ω : Ω
hTop : ∀ (i : ι), ∃ (a : ℕ), ∀ b ≥ a, (↑i : WithTop ι) < σ n b ω
hmem : ∀ (i : ℕ), σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)
⊢ False
have h : ∀ (N : ℕ) (hN : ∀ b ≥ N, (↑(T n) : WithTop ι) < σ n b ω), False
Tactic: obtain ⟨N, hN⟩ := hTop (T n)
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (hypothesis)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}
this : (1 / 2) ^ n ≤ (P : (a : Set Ω) → ℝ≥0∞) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)})
ω : Ω
hTop : ∀ (i : ι), ∃ (a : ℕ), ∀ b ≥ a, (↑i : WithTop ι) < σ n b ω
hmem : ∀ (i : ℕ), σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)
N : ℕ
hN : ∀ b ≥ N, (↑(T n) : WithTop ι) < σ n b ω
⊢ False
have hN₁ : (↑(T n) : WithTop ι) < σ n N ω
Tactic: specialize hN N le_rfl
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (hypothesis)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}
this : (1 / 2) ^ n ≤ (P : (a : Set Ω) → ℝ≥0∞) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)})
ω : Ω
hTop : ∀ (i : ι), ∃ (a : ℕ), ∀ b ≥ a, (↑i : WithTop ι) < σ n b ω
hmem : ∀ (i : ℕ), σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)
N : ℕ
hN : (↑(T n) : WithTop ι) < σ n N ω
⊢ False
have hmem₁ : σ n N ω < min (τ n ω) (↑(T n) : WithTop ι)
Tactic: specialize hmem N
Cleared hypotheses: hmem
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}
⊢ False
have suffices : (1 / 2) ^ n ≤ (P : (a : Set Ω) → ℝ≥0∞) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)})
Tactic: suffices (1 / 2) ^ n ≤ P (⋂ k : ℕ, {ω | σ n k ω < min (τ n ω) (T n)}) by
    refine (by simp : ¬ (1 / 2 : ℝ≥0∞) ^ n ≤ 0) <| this.trans <| nonpos_iff_eq_zero.2 ?_
    rw [measure_eq_zero_iff_ae_notMem]
    filter_upwards [(hσ n).tendsto_top] with ω hTop hmem
    simp_rw [WithTop.tendsto_nhds_top_iff, eventually_atTop] at hTop
    simp only [Set.mem_iInter, Set.mem_setOf_eq] at hmem
    obtain ⟨N, hN⟩ := hTop (T n)
    specialize hN N le_rfl
    specialize hmem N
    grind
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}
⊢ (1 / 2) ^ n ≤ (P : (a : Set Ω) → ℝ≥0∞) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)})
have rw : ∀ (i : ℕ), (1 / 2) ^ n ≤ (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)}
Tactic: rw [measure_iInter_of_ae_antitone, le_iInf_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
𝓕 : Filtration ι mΩ
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}
rw : ∀ (i : ℕ), (1 / 2) ^ n ≤ (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)}
⊢ (1 / 2) ^ n ≤ (P : (a : Set Ω) → ℝ≥0∞) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)})
have hs : ∀ᵐ (ω : Ω) ∂P,
  Antitone (β := Prop) fun (x : ℕ) ↦ Membership.mem (γ := Set Ω) {ω : Ω | σ n x ω < min (τ n ω) (↑(T n) : WithTop ι)} ω
Tactic: rw [measure_iInter_of_ae_antitone, le_iInf_iff]