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
nk : (n : ℕ) → ℕ
hnk : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
n : ℕ
ω : Ω
hω : Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ σ n x ω
⊢ LE.le.{u_1} (α := WithTop ι) ((fun (x : ℕ) ↦ σ n x ω) (nk n)) ((fun (x : ℕ) ↦ σ n x ω) (mkStrictMonoAux nk n))

Tactic:
specialize hω (le_mkStrictMonoAux nk n)

Premises used: _private.0.ProbabilityTheory.le_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
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ω : LE.le.{u_1} (α := WithTop ι) ((fun (x : ℕ) ↦ σ n x ω) (nk n)) ((fun (x : ℕ) ↦ σ n x ω) (mkStrictMonoAux nk n))
h :
  σ n (mkStrictMonoAux nk n) ω < τ n ω →
    σ n (mkStrictMonoAux nk n) ω < (↑(T n) : WithTop ι) → σ n (nk n) ω < τ n ω ∧ σ n (nk n) ω < (↑(T n) : WithTop ι)
⊢ {ω : Ω | σ n (mkStrictMonoAux nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ω ≤
    {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ω

Tactic:
simp [setOf]

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
nk : (n : ℕ) → ℕ
hnk : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
n : ℕ
ω : Ω
hω : LE.le.{u_1} (α := WithTop ι) ((fun (x : ℕ) ↦ σ n x ω) (nk n)) ((fun (x : ℕ) ↦ σ n x ω) (mkStrictMonoAux nk n))
⊢ σ n (mkStrictMonoAux nk n) ω < τ n ω →
    σ n (mkStrictMonoAux nk n) ω < (↑(T n) : WithTop ι) → σ n (nk n) ω < τ n ω ∧ σ n (nk n) ω < (↑(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
inst_5 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
obtain :
  ∀ (nk : ℕ → ℕ) (T : ℕ → ι) (hnk : StrictMono nk) (hT : Tendsto T atTop atTop)
    (hP : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n),
    ∃ (nk : ℕ → ℕ), StrictMono nk ∧ IsPreLocalizingSequence 𝓕 (fun (i : ℕ) (ω : Ω) ↦ min (τ i ω) (σ i (nk i) ω)) P
⊢ ∃ (nk : ℕ → ℕ), StrictMono nk ∧ IsPreLocalizingSequence 𝓕 (fun (i : ℕ) (ω : Ω) ↦ min (τ i ω) (σ i (nk i) ω)) P

Tactic:
obtain ⟨nk, T, hnk, hT, hP⟩ := 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
inst_5 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
nk : ℕ → ℕ
T : ℕ → ι
hnk : StrictMono nk
hT : Tendsto T atTop atTop
hP : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
⊢ ∃ (nk : ℕ → ℕ), StrictMono nk ∧ IsPreLocalizingSequence 𝓕 (fun (i : ℕ) (ω : Ω) ↦ min (τ i ω) (σ i (nk i) ω)) P

Tactic:
⟨nk, hnk, fun n ↦ (hτ.isStoppingTime n).min ((hσ _).isStoppingTime _), ?_⟩

Premises used: ProbabilityTheory.IsPreLocalizingSequence.isStoppingTime, MeasureTheory.IsStoppingTime.min, And.intro, Exists.intro, ProbabilityTheory.IsLocalizingSequence.toIsPreLocalizingSequence, ProbabilityTheory.IsPreLocalizingSequence.mk
-- 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
inst_5 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
nk : ℕ → ℕ
T : ℕ → ι
hnk : StrictMono nk
hT : Tendsto T atTop atTop
hP : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
refine : ∀ᵐ (ω : Ω) ∂P, Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ min (τ x ω) (σ x (nk x) ω)) atTop (𝓝 ⊤)
⊢ ∃ (nk : ℕ → ℕ), StrictMono nk ∧ IsPreLocalizingSequence 𝓕 (fun (i : ℕ) (ω : Ω) ↦ min (τ i ω) (σ i (nk i) ω)) P

Tactic:
refine ⟨nk, hnk, fun n ↦ (hτ.isStoppingTime n).min ((hσ _).isStoppingTime _), ?_⟩
-- 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
inst_5 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
nk : ℕ → ℕ
T : ℕ → ι
hnk : StrictMono nk
hT : Tendsto T atTop atTop
hP : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
⊢ 1 / 2 < 1

Tactic:
simp
-- 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
inst_5 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
nk : ℕ → ℕ
T : ℕ → ι
hnk : StrictMono nk
hT : Tendsto T atTop atTop
hP : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
⊢ LT.lt (α := ℝ≥0∞) (∑' (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)}) ∞

Tactic:
have : ∑' n, P {ω | σ n (nk n) ω < min (τ n ω) (T n)} < ∞ :=
    lt_of_le_of_lt (ENNReal.summable.tsum_mono ENNReal.summable hP)
      (tsum_geometric_lt_top.2 <| by simp)
-- 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
inst_5 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
nk : ℕ → ℕ
T : ℕ → ι
hnk : StrictMono nk
hT : Tendsto T atTop atTop
hP : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
this :
  LT.lt (α := ℝ≥0∞) (∑' (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)}) ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, ¬σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)
hωτ : Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ τ x ω) atTop (𝓝 ⊤)
⊢ ∀ᶠ (b : ℕ) in atTop, min (τ b ω) ((WithTop.some ∘ T) b) ≤ σ b (nk b) ω

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
inst_5 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
nk : ℕ → ℕ
T : ℕ → ι
hnk : StrictMono nk
hT : Tendsto T atTop atTop
hP : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
this :
  LT.lt (α := ℝ≥0∞) (∑' (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)}) ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, ¬σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)
hωτ : Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ τ x ω) atTop (𝓝 ⊤)
⊢ ∀ᶠ (b : ℕ) in atTop, σ b (nk b) ω ≤ min ⊤ ⊤

Tactic:
simp
-- 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
inst_5 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
nk : ℕ → ℕ
T : ℕ → ι
hnk : StrictMono nk
hT : Tendsto T atTop atTop
hP : ∀ (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
this :
  LT.lt (α := ℝ≥0∞) (∑' (n : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)}) ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, ¬σ n (nk n) ω < min (τ n ω) (↑(T n) : WithTop ι)
hωτ : Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ τ x ω) atTop (𝓝 ⊤)
⊢ Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ min (τ x ω) (σ x (nk x) ω)) atTop (𝓝 ⊤)

Tactic:
exact hωτ.min <| tendsto_of_tendsto_of_tendsto_of_le_of_le'
    (hωτ.min <| WithTop.tendsto_coe_atTop.comp hT) tendsto_const_nhds (by grind) (by simp)

Premises used: tendsto_const_nhds, tendsto_of_tendsto_of_tendsto_of_le_of_le', WithTop.tendsto_coe_atTop, Filter.Tendsto.min, Filter.Tendsto.comp
-- Module: Mathlib.Probability.Process.LocalProperty
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 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
inst_5 : DenselyOrdered ι
inst_6 : NoMaxOrder ι
inst_7 : Zero E
inst_8 : 𝓕.IsRightContinuous
hp : IsStable (mΩ := mΩ) 𝓕 p
⊢ Locally (fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) 𝓕 X P ↔ Locally p 𝓕 X P

Tactic:
⟨fun hL ↦ ?_, fun hL ↦ ⟨hL.localSeq, hL.isLocalizingSequence_localSeq,
    fun n ↦ .of_prop <| hL.stoppedProcess_localSeq n⟩⟩

Premises used: ProbabilityTheory.Locally.localSeq, ProbabilityTheory.Locally.isLocalizingSequence_localSeq, ProbabilityTheory.Locally.of_prop, ProbabilityTheory.Locally.stoppedProcess_localSeq, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.Probability.Process.LocalProperty
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 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
inst_5 : DenselyOrdered ι
inst_6 : NoMaxOrder ι
inst_7 : Zero E
inst_8 : 𝓕.IsRightContinuous
hp : IsStable (mΩ := mΩ) 𝓕 p
refine : ∀ (hL : Locally (fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) 𝓕 X P), Locally p 𝓕 X P
⊢ Locally (fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) 𝓕 X P ↔ Locally p 𝓕 X P

Tactic:
refine ⟨fun hL ↦ ?_, fun hL ↦ ⟨hL.localSeq, hL.isLocalizingSequence_localSeq,
    fun n ↦ .of_prop <| hL.stoppedProcess_localSeq n⟩⟩
-- Module: Mathlib.Probability.Process.LocalProperty
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 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
inst_5 : DenselyOrdered ι
inst_6 : NoMaxOrder ι
inst_7 : Zero E
inst_8 : 𝓕.IsRightContinuous
hp : IsStable (mΩ := mΩ) 𝓕 p
hL : Locally (fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) 𝓕 X P
choose :
  ∀ (τ : (n : ℕ) → ℕ → Ω → WithTop ι) (hτ₁ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (τ n) P)
    (hτ₂ :
      ∀ (n n_1 : ℕ),
        p
          (stoppedProcess
            (fun (i : ι) ↦
              Set.indicator {ω : Ω | ⊥ < τ n n_1 ω}
                (stoppedProcess
                  (fun (i : ι) ↦
                    Set.indicator {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω} (X i))
                  (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n) i))
            (τ n n_1))),
    Locally p 𝓕 X P
⊢ Locally p 𝓕 X P

Tactic:
choose τ hτ₁ hτ₂ using hL.stoppedProcess_localSeq

Premises used: ProbabilityTheory.Locally.stoppedProcess_localSeq
-- Module: Mathlib.Probability.Process.LocalProperty
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 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
inst_5 : DenselyOrdered ι
inst_6 : NoMaxOrder ι
inst_7 : Zero E
inst_8 : 𝓕.IsRightContinuous
hp : IsStable (mΩ := mΩ) 𝓕 p
hL : Locally (fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) 𝓕 X P
τ : (n : ℕ) → ℕ → Ω → WithTop ι
hτ₁ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (τ n) P
hτ₂ :
  ∀ (n n_1 : ℕ),
    p
      (stoppedProcess
        (fun (i : ι) ↦
          Set.indicator {ω : Ω | ⊥ < τ n n_1 ω}
            (stoppedProcess
              (fun (i : ι) ↦
                Set.indicator {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω} (X i))
              (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n) i))
        (τ n n_1))
obtain :
  ∀ (nk : ℕ → ℕ) (hnk : StrictMono nk)
    (hpre :
      IsPreLocalizingSequence 𝓕
        (fun (i : ℕ) (ω : Ω) ↦ min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) i ω) (τ i (nk i) ω)) P),
    Locally p 𝓕 X P
⊢ Locally p 𝓕 X P

Tactic:
obtain ⟨nk, hnk, hpre⟩ :=
    hL.isLocalizingSequence_localSeq.isPrelocalizingSequence_inf_extraction hτ₁

Premises used: ProbabilityTheory.Locally.isLocalizingSequence_localSeq, ProbabilityTheory.IsLocalizingSequence.isPrelocalizingSequence_inf_extraction
-- Module: Mathlib.Probability.Process.LocalProperty
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 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
inst_5 : DenselyOrdered ι
inst_6 : NoMaxOrder ι
inst_7 : Zero E
inst_8 : 𝓕.IsRightContinuous
hp : IsStable (mΩ := mΩ) 𝓕 p
hL : Locally (fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) 𝓕 X P
τ : (n : ℕ) → ℕ → Ω → WithTop ι
hτ₁ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (τ n) P
hτ₂ :
  ∀ (n n_1 : ℕ),
    p
      (stoppedProcess
        (fun (i : ι) ↦
          Set.indicator {ω : Ω | ⊥ < τ n n_1 ω}
            (stoppedProcess
              (fun (i : ι) ↦
                Set.indicator {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω} (X i))
              (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n) i))
        (τ n n_1))
nk : ℕ → ℕ
hnk : StrictMono nk
hpre :
  IsPreLocalizingSequence 𝓕
    (fun (i : ℕ) (ω : Ω) ↦ min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) i ω) (τ i (nk i) ω)) P
⊢ Locally p 𝓕 X P

Tactic:
locally_of_isPreLocalizingSequence hp hpre <| fun n ↦ ?_

Premises used: ProbabilityTheory.IsStable.locally_of_isPreLocalizingSequence
-- Module: Mathlib.Probability.Process.LocalProperty
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 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
inst_5 : DenselyOrdered ι
inst_6 : NoMaxOrder ι
inst_7 : Zero E
inst_8 : 𝓕.IsRightContinuous
hp : IsStable (mΩ := mΩ) 𝓕 p
hL : Locally (fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) 𝓕 X P
τ : (n : ℕ) → ℕ → Ω → WithTop ι
hτ₁ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (τ n) P
hτ₂ :
  ∀ (n n_1 : ℕ),
    p
      (stoppedProcess
        (fun (i : ι) ↦
          Set.indicator {ω : Ω | ⊥ < τ n n_1 ω}
            (stoppedProcess
              (fun (i : ι) ↦
                Set.indicator {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω} (X i))
              (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n) i))
        (τ n n_1))
nk : ℕ → ℕ
hnk : StrictMono nk
hpre :
  IsPreLocalizingSequence 𝓕
    (fun (i : ℕ) (ω : Ω) ↦ min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) i ω) (τ i (nk i) ω)) P
refine :
  ∀ (n : ℕ),
    p
      (stoppedProcess
        (fun (i : ι) ↦
          Set.indicator {ω : Ω | ⊥ < min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω) (τ n (nk n) ω)}
            (X i))
        fun (ω : Ω) ↦ min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω) (τ n (nk n) ω))
⊢ Locally p 𝓕 X P

Tactic:
refine locally_of_isPreLocalizingSequence hp hpre <| fun n ↦ ?_

Premises used: ProbabilityTheory.IsStable.locally_of_isPreLocalizingSequence
-- Module: Mathlib.Probability.Process.LocalProperty
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 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
inst_5 : DenselyOrdered ι
inst_6 : NoMaxOrder ι
inst_7 : Zero E
inst_8 : 𝓕.IsRightContinuous
hp : IsStable (mΩ := mΩ) 𝓕 p
hL : Locally (fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) 𝓕 X P
τ : (n : ℕ) → ℕ → Ω → WithTop ι
hτ₁ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (τ n) P
hτ₂ :
  ∀ (n n_1 : ℕ),
    p
      (stoppedProcess
        (fun (i : ι) ↦
          Set.indicator {ω : Ω | ⊥ < τ n n_1 ω}
            (stoppedProcess
              (fun (i : ι) ↦
                Set.indicator {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω} (X i))
              (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n) i))
        (τ n n_1))
nk : ℕ → ℕ
hnk : StrictMono nk
hpre :
  IsPreLocalizingSequence 𝓕
    (fun (i : ℕ) (ω : Ω) ↦ min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) i ω) (τ i (nk i) ω)) P
n : ℕ
⊢ p
    (stoppedProcess
      (fun (i : ι) ↦
        Set.indicator {ω : Ω | ⊥ < τ n (nk n) ω}
          (stoppedProcess
            (fun (i : ι) ↦
              Set.indicator {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω} (X i))
            (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n) i))
      (τ n (nk n)))

Tactic:
hτ₂ n (nk n)
-- Module: Mathlib.Probability.Process.LocalProperty
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 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
inst_5 : DenselyOrdered ι
inst_6 : NoMaxOrder ι
inst_7 : Zero E
inst_8 : 𝓕.IsRightContinuous
hp : IsStable (mΩ := mΩ) 𝓕 p
hL : Locally (fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) 𝓕 X P
τ : (n : ℕ) → ℕ → Ω → WithTop ι
hτ₁ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (τ n) P
hτ₂ :
  ∀ (n n_1 : ℕ),
    p
      (stoppedProcess
        (fun (i : ι) ↦
          Set.indicator {ω : Ω | ⊥ < τ n n_1 ω}
            (stoppedProcess
              (fun (i : ι) ↦
                Set.indicator {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω} (X i))
              (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n) i))
        (τ n n_1))
nk : ℕ → ℕ
hnk : StrictMono nk
hpre :
  IsPreLocalizingSequence 𝓕
    (fun (i : ℕ) (ω : Ω) ↦ min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) i ω) (τ i (nk i) ω)) P
n : ℕ
h :
  Eq (α := ι → Ω → E)
    (stoppedProcess
      (fun (i : ι) ↦
        Set.indicator {ω : Ω | ⊥ < min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω) (τ n (nk n) ω)}
          (X i))
      fun (ω : Ω) ↦ min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω) (τ n (nk n) ω))
    (stoppedProcess
      (fun (i : ι) ↦
        Set.indicator {ω : Ω | ⊥ < τ n (nk n) ω}
          (stoppedProcess
            (fun (i : ι) ↦
              Set.indicator {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω} (X i))
            (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n) i))
      (τ n (nk n)))
⊢ p
    (stoppedProcess
      (fun (i : ι) ↦
        Set.indicator {ω : Ω | ⊥ < min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω) (τ n (nk n) ω)}
          (X i))
      fun (ω : Ω) ↦ min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω) (τ n (nk n) ω))

Tactic:
convert! hτ₂ n (nk n) using 1 with