awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.LocalProperty
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 ι)
h : ∀ (N : ℕ) (hN : ∀ b ≥ N, (↑(T n) : WithTop ι) < σ n b ω), False
⊢ False

Tactic:
obtain ⟨N, hN⟩ := hTop (T n)
-- Module: Mathlib.Probability.Process.LocalProperty
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 ω
⊢ (↑(T n) : WithTop ι) < σ n N ω

Tactic:
specialize hN N le_rfl

Premises used: le_rfl
-- Module: Mathlib.Probability.Process.LocalProperty
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 ω
⊢ σ n N ω < min (τ n ω) (↑(T n) : WithTop ι)

Tactic:
specialize hmem N
-- Module: Mathlib.Probability.Process.LocalProperty
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 ω
N : ℕ
hN : (↑(T n) : WithTop ι) < σ n N ω
hmem : σ n N ω < min (τ n ω) (↑(T n) : WithTop ι)
⊢ False

Tactic:
grind
-- Module: Mathlib.Probability.Process.LocalProperty
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 ι)}
suffices : (1 / 2) ^ n ≤ (P : (a : Set Ω) → ℝ≥0∞) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)})
⊢ False

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
-- Module: Mathlib.Probability.Process.LocalProperty
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 ι)}
hs :
  ∀ᵐ (ω : Ω) ∂P,
    Antitone (β := Prop) fun (x : ℕ) ↦
      Membership.mem (γ := Set Ω) {ω : Ω | σ n x ω < min (τ n ω) (↑(T n) : WithTop ι)} ω
hsm : ∀ (i : ℕ), NullMeasurableSet {ω : Ω | σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)} P
hfin :
  ∃ (i : ℕ),
    Ne (α := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (1 / 2) ^ n ≤ (P : (a : Set Ω) → ℝ≥0∞) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)})

Tactic:
rw [measure_iInter_of_ae_antitone, le_iInf_iff]

Premises used: MeasureTheory.measure_iInter_of_ae_antitone, le_iInf_iff
-- Module: Mathlib.Probability.Process.LocalProperty
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 ι)}
⊢ ∀ (i : ℕ), (1 / 2) ^ n ≤ (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)}

Tactic:
fun k ↦ (hn k).le

Premises used: LT.lt.le
-- Module: Mathlib.Probability.Process.LocalProperty
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 ι)}
⊢ ∀ (i : ℕ), (1 / 2) ^ n ≤ (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)}

Tactic:
exact fun k ↦ (hn k).le

Premises used: LT.lt.le
-- Module: Mathlib.Probability.Process.LocalProperty
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 ι)}
h :
  ∀ (ω : Ω) (hω : Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ σ n x ω),
    Antitone (β := Prop) fun (x : ℕ) ↦ σ n x ω < min (τ n ω) (↑(T n) : WithTop ι)
⊢ ∀ᵐ (ω : Ω) ∂P,
    Antitone (β := Prop) fun (x : ℕ) ↦
      Membership.mem (γ := Set Ω) {ω : Ω | σ n x ω < min (τ n ω) (↑(T n) : WithTop ι)} ω

Tactic:
filter_upwards [(hσ n).mono] with ω hω

Premises used: ProbabilityTheory.IsLocalizingSequence.mono
-- Module: Mathlib.Probability.Process.LocalProperty
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 ι)}
ω : Ω
hω : Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ σ n x ω
i j : ℕ
hij : i ≤ j
⊢ LE.le.{u_1} (α := WithTop ι) ((fun (x : ℕ) ↦ σ n x ω) i) ((fun (x : ℕ) ↦ σ n x ω) j)

Tactic:
specialize hω hij
-- Module: Mathlib.Probability.Process.LocalProperty
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 ι)}
ω : Ω
i j : ℕ
hij : i ≤ j
hω : LE.le.{u_1} (α := WithTop ι) ((fun (x : ℕ) ↦ σ n x ω) i) ((fun (x : ℕ) ↦ σ n x ω) j)
h :
  ∀
    (hn :
      ∀ (k : ℕ),
        HPow.hPow (α := ℝ≥0∞) 2⁻¹ n <
          (P : (a : Set Ω) → ℝ≥0∞) fun (ω : Ω) ↦ σ n k ω < τ n ω ∧ σ n k ω < (↑(T n) : WithTop ι)),
    σ n j ω < τ n ω → σ n j ω < (↑(T n) : WithTop ι) → σ n i ω < τ n ω ∧ σ n i ω < (↑(T n) : WithTop ι)
⊢ LE.le (α := Prop) ((fun (x : ℕ) ↦ σ n x ω < min (τ n ω) (↑(T n) : WithTop ι)) j)
    ((fun (x : ℕ) ↦ σ n x ω < min (τ n ω) (↑(T n) : WithTop ι)) i)

Tactic:
simp [setOf] at *

Premises used: setOf
-- Module: Mathlib.Probability.Process.LocalProperty
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 : ℕ
ω : Ω
i j : ℕ
hij : i ≤ j
hω : σ n i ω ≤ σ n j ω
hn :
  ∀ (k : ℕ),
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ n <
      (P : (a : Set Ω) → ℝ≥0∞) fun (ω : Ω) ↦ σ n k ω < τ n ω ∧ σ n k ω < (↑(T n) : WithTop ι)
⊢ σ n j ω < τ n ω → σ n j ω < (↑(T n) : WithTop ι) → σ n i ω < τ n ω ∧ σ n i ω < (↑(T n) : WithTop ι)

Tactic:
grind
-- Module: Mathlib.Probability.Process.LocalProperty
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 ι)}
⊢ ∀ (i : ℕ), NullMeasurableSet {ω : Ω | σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)} P

Tactic:
fun i ↦ .nullMeasurableSet ?_

Premises used: MeasurableSet.nullMeasurableSet
-- Module: Mathlib.Probability.Process.LocalProperty
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 ι)}
hsm : ∀ (i : ℕ), MeasurableSet.{u_2} (α := Ω) {ω : Ω | σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)}
⊢ ∀ (i : ℕ), NullMeasurableSet {ω : Ω | σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)} P

Tactic:
refine fun i ↦ .nullMeasurableSet ?_
-- Module: Mathlib.Probability.Process.LocalProperty
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 ι)}
i : ℕ
hsm : MeasurableSet.{u_2} (α := Ω) ({a : Ω | σ n i a < τ n a} ∩ {a : Ω | σ n i a < (↑(T n) : WithTop ι)})
⊢ MeasurableSet.{u_2} (α := Ω) {ω : Ω | σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)}

Tactic:
simp_rw [lt_inf_iff, Set.setOf_and]

Premises used: Set.setOf_and, lt_inf_iff
-- Module: Mathlib.Probability.Process.LocalProperty
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 ι)}
i : ℕ
⊢ MeasurableSet.{u_2} (α := Ω) ({a : Ω | σ n i a < τ n a} ∩ {a : Ω | σ n i a < (↑(T n) : WithTop ι)})

Tactic:
MeasurableSet.inter
      (measurableSet_lt ((hσ n).isStoppingTime i).measurable' (hτ.isStoppingTime n).measurable')
        <| measurableSet_lt ((hσ n).isStoppingTime i).measurable' measurable_const

Premises used: ProbabilityTheory.IsPreLocalizingSequence.isStoppingTime, MeasureTheory.IsStoppingTime.measurable', measurableSet_lt, measurable_const, ProbabilityTheory.IsLocalizingSequence.toIsPreLocalizingSequence, MeasurableSet.inter
-- Module: Mathlib.Probability.Process.LocalProperty
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 ι)}
i : ℕ
⊢ MeasurableSet.{u_2} (α := Ω) ({a : Ω | σ n i a < τ n a} ∩ {a : Ω | σ n i a < (↑(T n) : WithTop ι)})

Tactic:
exact MeasurableSet.inter
      (measurableSet_lt ((hσ n).isStoppingTime i).measurable' (hτ.isStoppingTime n).measurable')
        <| measurableSet_lt ((hσ n).isStoppingTime i).measurable' measurable_const

Premises used: ProbabilityTheory.IsPreLocalizingSequence.isStoppingTime, MeasureTheory.IsStoppingTime.measurable', measurableSet_lt, measurable_const, ProbabilityTheory.IsLocalizingSequence.toIsPreLocalizingSequence, MeasurableSet.inter
-- Module: Mathlib.Probability.Process.LocalProperty
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 ι)}
⊢ ∃ (i : ℕ),
    Ne (α := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
⟨0, measure_ne_top P _⟩

Premises used: MeasureTheory.measure_ne_top, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Probability.Process.LocalProperty
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 ι)}
⊢ ∃ (i : ℕ),
    Ne (α := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ⟨0, measure_ne_top P _⟩
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
x : ℕ → ℕ
n : ℕ
⊢ mkStrictMonoAux x n < mkStrictMonoAux x (n + 1)

Tactic:
grind [mkStrictMonoAux]

Premises used: _private.0.ProbabilityTheory.mkStrictMonoAux
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
x : ℕ → ℕ
⊢ x 0 ≤ mkStrictMonoAux x 0

Tactic:
simp [mkStrictMonoAux]

Premises used: _private.0.ProbabilityTheory.mkStrictMonoAux
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
x : ℕ → ℕ
n : ℕ
⊢ x (n + 1) ≤ mkStrictMonoAux x (n + 1)

Tactic:
grind [mkStrictMonoAux]

Premises used: _private.0.ProbabilityTheory.mkStrictMonoAux
-- Module: Mathlib.Probability.Process.LocalProperty
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
obtain :
  ∀ (T : ℕ → ι) (hT : Tendsto T atTop atTop)
    (h :
      ∀ (n : ℕ),
        ∃ (k : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n),
    ∃ (nk : ℕ → ℕ) (T : ℕ → ι),
      StrictMono nk ∧
        Tendsto T atTop atTop ∧
          ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
⊢ ∃ (nk : ℕ → ℕ) (T : ℕ → ι),
    StrictMono nk ∧
      Tendsto T atTop atTop ∧
        ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n

Tactic:
obtain ⟨T, hT, h⟩ := isPreLocalizingSequence_of_isLocalizingSequence_aux' hτ hσ

Premises used: _private.0.ProbabilityTheory.isPreLocalizingSequence_of_isLocalizingSequence_aux'
-- Module: Mathlib.Probability.Process.LocalProperty
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
h : ∀ (n : ℕ), ∃ (k : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
choose :
  ∀ (nk : (n : ℕ) → ℕ)
    (hnk : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n),
    ∃ (nk : ℕ → ℕ) (T : ℕ → ι),
      StrictMono nk ∧
        Tendsto T atTop atTop ∧
          ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
⊢ ∃ (nk : ℕ → ℕ) (T : ℕ → ι),
    StrictMono nk ∧
      Tendsto T atTop atTop ∧
        ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n

Tactic:
choose nk hnk using h
-- Module: Mathlib.Probability.Process.LocalProperty
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
nk : (n : ℕ) → ℕ
hnk : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
⊢ ∃ (nk : ℕ → ℕ) (T : ℕ → ι),
    StrictMono nk ∧
      Tendsto T atTop atTop ∧
        ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n

Tactic:
⟨mkStrictMonoAux nk, T, mkStrictMonoAux_strictMono nk, hT,
    fun n ↦ le_trans (EventuallyLE.measure_le ?_) (hnk n)⟩

Premises used: _private.0.ProbabilityTheory.mkStrictMonoAux_strictMono, And.intro, Exists.intro, Filter.EventuallyLE.measure_le, _private.0.ProbabilityTheory.mkStrictMonoAux, le_trans
-- Module: Mathlib.Probability.Process.LocalProperty
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
nk : (n : ℕ) → ℕ
hnk : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
refine :
  ∀ (n : ℕ),
    {ω : Ω | σ n (mkStrictMonoAux nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ᶠ[ae P]
      {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)}
⊢ ∃ (nk : ℕ → ℕ) (T : ℕ → ι),
    StrictMono nk ∧
      Tendsto T atTop atTop ∧
        ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n

Tactic:
refine ⟨mkStrictMonoAux nk, T, mkStrictMonoAux_strictMono nk, hT,
    fun n ↦ le_trans (EventuallyLE.measure_le ?_) (hnk n)⟩
-- Module: Mathlib.Probability.Process.LocalProperty
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
nk : (n : ℕ) → ℕ
hnk : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
n : ℕ
h :
  ∀ (ω : Ω) (hω : Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ σ n x ω),
    {ω : Ω | σ n (mkStrictMonoAux nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ω ≤
      {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ω
⊢ {ω : Ω | σ n (mkStrictMonoAux nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ᶠ[ae P]
    {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)}

Tactic:
filter_upwards [(hσ n).mono] with ω hω

Premises used: ProbabilityTheory.IsLocalizingSequence.mono