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 : 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 ω))

Tactic:
tendsto_atTop_iSup fun n m hnm ↦ ?_

Premises used: tendsto_atTop_iSup
-- 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 : 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 ω) ⊤
h :
  ∀ (n m : ℕ) (hnm : n ≤ m),
    LE.le.{u_1} (α := WithTop ι) (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω) (⨅ (j : ℕ), ⨅ (_ : j ≥ m), τ j ω)
⊢ Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ ⨅ (j : ℕ), ⨅ (_ : j ≥ x), τ j ω) atTop
    (𝓝 (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), τ i ω))

Tactic:
refine tendsto_atTop_iSup fun n m hnm ↦ ?_

Premises used: tendsto_atTop_iSup
-- 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 : 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
h : ∀ (i : ℕ) (i_1 : m ≤ i) (b : WithTop ι), (∀ (i : ℕ) (i_2 : n ≤ i), b ≤ τ i ω) → b ≤ τ i ω
⊢ LE.le.{u_1} (α := WithTop ι) (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω) (⨅ (j : ℕ), ⨅ (_ : j ≥ m), τ j ω)

Tactic:
simp [iInf_le_iff]

Premises used: iInf_le_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 : 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
⊢ ∀ (i : ℕ) (i_1 : m ≤ i) (b : WithTop ι), (∀ (i : ℕ) (i_2 : n ≤ i), b ≤ τ i ω) → b ≤ τ i ω

Tactic:
grind
-- 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 : 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

Tactic:
⟨_, hτ.isLocalizingSequence_biInf, fun n ↦ ?_⟩

Premises used: ProbabilityTheory.IsPreLocalizingSequence.isLocalizingSequence_biInf, And.intro, Exists.intro, ProbabilityTheory.Locally
-- 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 : 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))
refine :
  ∀ (n : ℕ),
    p
      (stoppedProcess
        (fun (i : ι) ↦ Set.indicator {ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)} (X i))
        fun (ω : Ω) ↦ ⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)
⊢ Locally p 𝓕 X P

Tactic:
refine ⟨_, hτ.isLocalizingSequence_biInf, fun 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 : 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 : ℕ
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)
⊢ p
    (stoppedProcess
      (fun (i : ι) ↦ Set.indicator {ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)} (X i))
      fun (ω : Ω) ↦ ⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)

Tactic:
rw [stoppedProcess_indicator_comm', ← stoppedProcess_stoppedProcess_of_le_right
    (τ := fun ω ↦ τ n ω) (fun _ ↦ (iInf_le _ n).trans <| iInf_le _ le_rfl),
    ← stoppedProcess_indicator_comm']

Premises used: MeasureTheory.stoppedProcess_indicator_comm', MeasureTheory.stoppedProcess_stoppedProcess_of_le_right, LE.le.trans, iInf_le
-- 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 : 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 ι) ⊥ ((fun (ω : Ω) ↦ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω : WithTop ι)) ω)}
          (stoppedProcess (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < τ n ω} (X i)) (τ n) i))
      fun (ω : Ω) ↦ ⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)

Tactic:
hp _ (hpτ n) (fun ω ↦ ⨅ j ≥ n, τ j ω) <| hτ.isLocalizingSequence_biInf.isStoppingTime n

Premises used: iInf, ProbabilityTheory.IsPreLocalizingSequence.isStoppingTime, setOf, ProbabilityTheory.IsPreLocalizingSequence.isLocalizingSequence_biInf, ProbabilityTheory.IsLocalizingSequence.toIsPreLocalizingSequence
-- 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 : 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 : ℕ
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)
⊢ 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:
convert!
    hp _ (hpτ n) (fun ω ↦ ⨅ j ≥ n, τ j ω) <| hτ.isLocalizingSequence_biInf.isStoppingTime n using 2

Premises used: iInf, ProbabilityTheory.IsPreLocalizingSequence.isStoppingTime, ProbabilityTheory.IsPreLocalizingSequence.isLocalizingSequence_biInf, ProbabilityTheory.IsLocalizingSequence.toIsPreLocalizingSequence
-- 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 : 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 : ℕ
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) ω
⊢ 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:
ext i ω
-- 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 : 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 : ι
ω : Ω
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) ω
⊢ 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:
rw [stoppedProcess_indicator_comm', Set.indicator_indicator]

Premises used: MeasureTheory.stoppedProcess_indicator_comm', Set.indicator_indicator
-- 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 : 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 : ι
ω : Ω
h :
  ∀ (ω : Ω),
    LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω) ↔
      ({ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)} ∩ {ω : Ω | ⊥ < τ n ω}) ω
⊢ 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:
congr with ω
-- 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 : 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 : ι
ω_1 ω : Ω
⊢ LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω) ↔
    ({ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)} ∩ {ω : Ω | ⊥ < τ n ω}) ω

Tactic:
⟨fun h ↦ ⟨h, lt_of_lt_of_le h <| (iInf_le _ n).trans (iInf_le _ le_rfl)⟩, fun h ↦ h.1⟩

Premises used: iInf, le_rfl, And.left, And.intro, Iff.intro, LE.le.trans, iInf_le, lt_of_lt_of_le
-- 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 : 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 : ι
ω_1 ω : Ω
⊢ LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω) ↔
    ({ω : Ω | LT.lt.{u_1} (α := WithTop ι) ⊥ (⨅ (j : ℕ), ⨅ (_ : j ≥ n), τ j ω)} ∩ {ω : Ω | ⊥ < τ n ω}) ω

Tactic:
exact ⟨fun h ↦ ⟨h, lt_of_lt_of_le h <| (iInf_le _ n).trans (iInf_le _ le_rfl)⟩, fun h ↦ h.1⟩
-- 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),
    ∃ (T : ℕ → ι),
      Tendsto T atTop atTop ∧
        ∀ (n : ℕ),
          ∃ (k : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
⊢ ∃ (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 ι

Premises used: Filter.exists_seq_monotone_tendsto_atTop_atTop
-- 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
⊢ ∃ (T : ℕ → ι),
    Tendsto T atTop atTop ∧
      ∀ (n : ℕ), ∃ (k : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n

Tactic:
⟨T, hT, fun n ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- 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
refine :
  ∀ (n : ℕ), ∃ (k : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n
⊢ ∃ (T : ℕ → ι),
    Tendsto T atTop atTop ∧
      ∀ (n : ℕ), ∃ (k : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n

Tactic:
refine ⟨T, hT, fun 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 : ℕ
by_contra! :
  ∀ (hn : ∀ (k : ℕ), (1 / 2) ^ n < (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}), False
⊢ ∃ (k : ℕ), (P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)} ≤ (1 / 2) ^ n

Tactic:
by_contra! hn
-- 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 ι)})
⊢ ¬(1 / 2) ^ n ≤ 0

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
τ : ℕ → Ω → 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 ι)})
refine :
  Eq (α := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}) : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ False

Tactic:
refine (by simp : ¬ (1 / 2 : ℝ≥0∞) ^ n ≤ 0) <| this.trans <| nonpos_iff_eq_zero.2 ?_

Premises used: Iff.mpr, LE.le.trans, nonpos_iff_eq_zero
-- 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 ι)})
rw : ∀ᵐ (a : Ω) ∂P, a ∉ ⋂ (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∞)

Tactic:
rw [measure_eq_zero_iff_ae_notMem]

Premises used: MeasureTheory.measure_eq_zero_iff_ae_notMem
-- 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 ι)})
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
⊢ ∀ᵐ (a : Ω) ∂P, a ∉ ⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}

Tactic:
filter_upwards [(hσ n).tendsto_top] with ω hTop hmem

Premises used: ProbabilityTheory.IsLocalizingSequence.toIsPreLocalizingSequence, ProbabilityTheory.IsPreLocalizingSequence.tendsto_top
-- 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 : Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ σ n x ω) atTop (𝓝 ⊤)
hmem : Membership.mem (γ := Set Ω) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}) ω
⊢ ∀ (i : ι), ∃ (a : ℕ), ∀ b ≥ a, (↑i : WithTop ι) < σ n b ω

Tactic:
simp_rw [WithTop.tendsto_nhds_top_iff, eventually_atTop] at hTop

Premises used: WithTop.tendsto_nhds_top_iff, Filter.eventually_atTop
-- 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 ι)})
ω : Ω
hmem : Membership.mem (γ := Set Ω) (⋂ (k : ℕ), {ω : Ω | σ n k ω < min (τ n ω) (↑(T n) : WithTop ι)}) ω
hTop : ∀ (i : ι), ∃ (a : ℕ), ∀ b ≥ a, (↑i : WithTop ι) < σ n b ω
⊢ ∀ (i : ℕ), σ n i ω < min (τ n ω) (↑(T n) : WithTop ι)

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

Premises used: Set.mem_setOf_eq, Set.mem_iInter