awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
p : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
hp : IsStable 𝓕 p
X : ι → Ω → E
hX : (fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) X
τ : Ω → WithTop ι
hτ : IsStoppingTime 𝓕 τ
n : ℕ
⊢ p fun (i : ι) ↦
    Set.indicator {ω : Ω | ⊥ < τ ω}
      (Set.indicator {ω : Ω | ⊥ < Locally.localSeq (p := p) hX n ω}
        (stoppedProcess (stoppedProcess X (Locally.localSeq (p := p) hX n)) τ i))

Tactic:
hp _ (hX.stoppedProcess_localSeq n) τ hτ

Premises used: Set.indicator, MeasureTheory.stoppedProcess, WithTop.some, ProbabilityTheory.Locally.stoppedProcess_localSeq, WithTop.untopD, WithTop.recTopCoe, ite
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
p : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
hp : IsStable 𝓕 p
X : ι → Ω → E
hX : (fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) X
τ : Ω → WithTop ι
hτ : IsStoppingTime 𝓕 τ
n : ℕ
⊢ p fun (i : ι) ↦
    Set.indicator {ω : Ω | ⊥ < τ ω}
      (Set.indicator {ω : Ω | ⊥ < Locally.localSeq (p := p) hX n ω}
        (stoppedProcess (stoppedProcess X (Locally.localSeq (p := p) hX n)) τ i))

Tactic:
exact hp _ (hX.stoppedProcess_localSeq n) τ hτ

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 : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p q : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
⊢ Locally (fun (Y : ι → Ω → E) ↦ p Y ∧ q Y) 𝓕 X P ↔ Locally p 𝓕 X P ∧ Locally q 𝓕 X P

Tactic:
⟨Locally.of_and, fun ⟨hpX, hqX⟩ ↦
    ⟨_, hpX.isLocalizingSequence_localSeq.min hqX.isLocalizingSequence_localSeq, fun n ↦ ?_⟩⟩

Premises used: ProbabilityTheory.Locally.localSeq, ProbabilityTheory.Locally.isLocalizingSequence_localSeq, _private.0.ProbabilityTheory.IsStable.locally_and_iff.match_1, ProbabilityTheory.IsLocalizingSequence.min, And, And.intro, Iff.intro, Exists.intro, ProbabilityTheory.Locally, ProbabilityTheory.Locally.of_and, Min.min
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p q : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
refine :
  Locally p 𝓕 X P ∧ Locally q 𝓕 X P →
    ∀ (hpX : Locally p 𝓕 X P) (hqX : Locally q 𝓕 X P) (n : ℕ),
      (fun (Y : ι → Ω → E) ↦ p Y ∧ q Y)
        (stoppedProcess
          (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < (hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n ω} (X i))
          ((hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n))
⊢ Locally (fun (Y : ι → Ω → E) ↦ p Y ∧ q Y) 𝓕 X P ↔ Locally p 𝓕 X P ∧ Locally q 𝓕 X P

Tactic:
refine ⟨Locally.of_and, fun ⟨hpX, hqX⟩ ↦
    ⟨_, hpX.isLocalizingSequence_localSeq.min hqX.isLocalizingSequence_localSeq, fun n ↦ ?_⟩⟩
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p q : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
h : Locally p 𝓕 X P ∧ Locally q 𝓕 X P
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
n : ℕ
this :
  ∀ (p q : (ι → Ω → E) → Prop) (hp : IsStable 𝓕 p) (hq : IsStable 𝓕 q) (hpX : Locally p 𝓕 X P) (hqX : Locally q 𝓕 X P),
    p
      (stoppedProcess
        (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < (hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n ω} (X i))
        ((hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n))
⊢ (fun (Y : ι → Ω → E) ↦ p Y ∧ q Y)
    (stoppedProcess
      (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < (hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n ω} (X i))
      ((hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n))

Tactic:
⟨this p q hp hq hpX hqX, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p q : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
h : Locally p 𝓕 X P ∧ Locally q 𝓕 X P
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
n : ℕ
this :
  ∀ (p q : (ι → Ω → E) → Prop) (hp : IsStable 𝓕 p) (hq : IsStable 𝓕 q) (hpX : Locally p 𝓕 X P) (hqX : Locally q 𝓕 X P),
    p
      (stoppedProcess
        (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < (hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n ω} (X i))
        ((hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n))
refine :
  q
    (stoppedProcess
      (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < (hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n ω} (X i))
      ((hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n))
⊢ (fun (Y : ι → Ω → E) ↦ p Y ∧ q Y)
    (stoppedProcess
      (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < (hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n ω} (X i))
      ((hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n))

Tactic:
refine ⟨this p q hp hq hpX hqX, ?_⟩
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p q : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
h : Locally p 𝓕 X P ∧ Locally q 𝓕 X P
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
n : ℕ
this :
  ∀ (p q : (ι → Ω → E) → Prop) (hp : IsStable 𝓕 p) (hq : IsStable 𝓕 q) (hpX : Locally p 𝓕 X P) (hqX : Locally q 𝓕 X P),
    p
      (stoppedProcess
        (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < (hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n ω} (X i))
        ((hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n))
simp_rw :
  q
    (stoppedProcess
      (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < (hqX.localSeq (p := q) ⊓ hpX.localSeq (p := p)) n ω} (X i))
      ((hqX.localSeq (p := q) ⊓ hpX.localSeq (p := p)) n))
⊢ q
    (stoppedProcess
      (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < (hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n ω} (X i))
      ((hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n))

Tactic:
simp_rw [inf_comm hpX.localSeq]

Premises used: ProbabilityTheory.Locally.localSeq, inf_comm
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p q : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
h : Locally p 𝓕 X P ∧ Locally q 𝓕 X P
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
n : ℕ
this :
  ∀ (p q : (ι → Ω → E) → Prop) (hp : IsStable 𝓕 p) (hq : IsStable 𝓕 q) (hpX : Locally p 𝓕 X P) (hqX : Locally q 𝓕 X P),
    p
      (stoppedProcess
        (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < (hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n ω} (X i))
        ((hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n))
⊢ q
    (stoppedProcess
      (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < (hqX.localSeq (p := q) ⊓ hpX.localSeq (p := p)) n ω} (X i))
      ((hqX.localSeq (p := q) ⊓ hpX.localSeq (p := p)) n))

Tactic:
this q p hq hp hqX hpX

Premises used: setOf
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p q : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
h : Locally p 𝓕 X P ∧ Locally q 𝓕 X P
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
n : ℕ
this :
  ∀ (p q : (ι → Ω → E) → Prop) (hp : IsStable 𝓕 p) (hq : IsStable 𝓕 q) (hpX : Locally p 𝓕 X P) (hqX : Locally q 𝓕 X P),
    p
      (stoppedProcess
        (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < (hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n ω} (X i))
        ((hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n))
⊢ q
    (stoppedProcess
      (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < (hqX.localSeq (p := q) ⊓ hpX.localSeq (p := p)) n ω} (X i))
      ((hqX.localSeq (p := q) ⊓ hpX.localSeq (p := p)) n))

Tactic:
exact this q p hq hp hqX hpX
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p q : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
h : Locally p 𝓕 X P ∧ Locally q 𝓕 X P
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
n : ℕ
suffices :
  ∀ (p q : (ι → Ω → E) → Prop) (hp : IsStable 𝓕 p) (hq : IsStable 𝓕 q) (hpX : Locally p 𝓕 X P) (hqX : Locally q 𝓕 X P),
    p
      (stoppedProcess
        (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < (hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n ω} (X i))
        ((hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n))
⊢ p
      (stoppedProcess
        (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < (hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n ω} (X i))
        ((hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n)) ∧
    q
      (stoppedProcess
        (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < (hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n ω} (X i))
        ((hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n))

Tactic:
suffices ∀ (p q : (ι → Ω → E) → Prop) (hp : IsStable 𝓕 p) (hq : IsStable 𝓕 q)
      (hpX : Locally p 𝓕 X P) (hqX : Locally q 𝓕 X P),
      p (stoppedProcess (fun i ↦ {ω | ⊥ < (hpX.localSeq ⊓ hqX.localSeq) n ω}.indicator (X i))
      ((hpX.localSeq ⊓ hqX.localSeq) n)) by
    refine ⟨this p q hp hq hpX hqX, ?_⟩
    simp_rw [inf_comm hpX.localSeq]
    exact this q p hq hp hqX hpX
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p_1 q_1 : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
hp_1 : IsStable 𝓕 p_1
hq_1 : IsStable 𝓕 q_1
h : Locally p_1 𝓕 X P ∧ Locally q_1 𝓕 X P
hpX_1 : Locally p_1 𝓕 X P
hqX_1 : Locally q_1 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
⊢ p
    (stoppedProcess
      (fun (i : ι) ↦
        Set.indicator {ω : Ω | ⊥ < hqX.localSeq (p := q) n ω}
          (stoppedProcess (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < hpX.localSeq (p := p) n ω} (X i))
            (hpX.localSeq (p := p) n) i))
      (hqX.localSeq (p := q) n))

Tactic:
hp _ (hpX.stoppedProcess_localSeq n) _ <|
      hqX.isLocalizingSequence_localSeq.isStoppingTime n

Premises used: ProbabilityTheory.Locally.isLocalizingSequence_localSeq, ProbabilityTheory.IsPreLocalizingSequence.isStoppingTime, ProbabilityTheory.Locally.stoppedProcess_localSeq, ProbabilityTheory.IsLocalizingSequence.toIsPreLocalizingSequence
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p_1 q_1 : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
hp_1 : IsStable 𝓕 p_1
hq_1 : IsStable 𝓕 q_1
h_1 : Locally p_1 𝓕 X P ∧ Locally q_1 𝓕 X P
hpX_1 : Locally p_1 𝓕 X P
hqX_1 : Locally q_1 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
h :
  Eq (α := ι → Ω → E)
    (stoppedProcess
      (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < (hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n ω} (X i))
      ((hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n))
    (stoppedProcess
      (fun (i : ι) ↦
        Set.indicator {ω : Ω | ⊥ < hqX.localSeq (p := q) n ω}
          (stoppedProcess (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < hpX.localSeq (p := p) n ω} (X i))
            (hpX.localSeq (p := p) n) i))
      (hqX.localSeq (p := q) n))
⊢ p
    (stoppedProcess
      (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < (hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n ω} (X i))
      ((hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n))

Tactic:
convert!
    hp _ (hpX.stoppedProcess_localSeq n) _ <|
      hqX.isLocalizingSequence_localSeq.isStoppingTime n using 1

Premises used: ProbabilityTheory.Locally.isLocalizingSequence_localSeq, ProbabilityTheory.IsPreLocalizingSequence.isStoppingTime, ProbabilityTheory.Locally.stoppedProcess_localSeq, ProbabilityTheory.IsLocalizingSequence.toIsPreLocalizingSequence
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p_1 q_1 : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
hp_1 : IsStable 𝓕 p_1
hq_1 : IsStable 𝓕 q_1
h_1 : Locally p_1 𝓕 X P ∧ Locally q_1 𝓕 X P
hpX_1 : Locally p_1 𝓕 X P
hqX_1 : Locally q_1 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
h :
  ∀ (i : ι) (ω : Ω),
    Eq.{u_3 + 1} (α := E)
      (stoppedProcess
        (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < (hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n ω} (X i))
        ((hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n) i ω)
      (stoppedProcess
        (fun (i : ι) ↦
          Set.indicator {ω : Ω | ⊥ < hqX.localSeq (p := q) n ω}
            (stoppedProcess (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < hpX.localSeq (p := p) n ω} (X i))
              (hpX.localSeq (p := p) n) i))
        (hqX.localSeq (p := q) n) i ω)
⊢ Eq (α := ι → Ω → E)
    (stoppedProcess
      (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < (hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n ω} (X i))
      ((hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n))
    (stoppedProcess
      (fun (i : ι) ↦
        Set.indicator {ω : Ω | ⊥ < hqX.localSeq (p := q) n ω}
          (stoppedProcess (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < hpX.localSeq (p := p) n ω} (X i))
            (hpX.localSeq (p := p) n) i))
      (hqX.localSeq (p := q) n))

Tactic:
ext i ω
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p_1 q_1 : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
hp_1 : IsStable 𝓕 p_1
hq_1 : IsStable 𝓕 q_1
h_1 : Locally p_1 𝓕 X P ∧ Locally q_1 𝓕 X P
hpX_1 : Locally p_1 𝓕 X P
hqX_1 : Locally q_1 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
i : ι
ω : Ω
h :
  Set.indicator {ω : Ω | ⊥ < hpX.localSeq (p := p) n ω ∧ ⊥ < hqX.localSeq (p := q) n ω}
      (stoppedProcess X (hqX.localSeq (p := q) n ⊓ hpX.localSeq (p := p) n) i) ω =
    Set.indicator {ω : Ω | ⊥ < hqX.localSeq (p := q) n ω}
      (Set.indicator {ω : Ω | ⊥ < hpX.localSeq (p := p) n ω}
        (stoppedProcess (stoppedProcess X (hpX.localSeq (p := p) n)) (hqX.localSeq (p := q) n) i))
      ω
⊢ Eq.{u_3 + 1} (α := E)
    (stoppedProcess
      (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < (hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n ω} (X i))
      ((hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n) i ω)
    (stoppedProcess
      (fun (i : ι) ↦
        Set.indicator {ω : Ω | ⊥ < hqX.localSeq (p := q) n ω}
          (stoppedProcess (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < hpX.localSeq (p := p) n ω} (X i))
            (hpX.localSeq (p := p) n) i))
      (hqX.localSeq (p := q) n) i ω)

Tactic:
simp_rw [stoppedProcess_indicator_comm, Pi.inf_apply, lt_inf_iff, inf_comm (hpX.localSeq n)]

Premises used: ProbabilityTheory.Locally.localSeq, lt_inf_iff, inf_comm, Pi.inf_apply, MeasureTheory.stoppedProcess_indicator_comm
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p_1 q_1 : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
hp_1 : IsStable 𝓕 p_1
hq_1 : IsStable 𝓕 q_1
h_1 : Locally p_1 𝓕 X P ∧ Locally q_1 𝓕 X P
hpX_1 : Locally p_1 𝓕 X P
hqX_1 : Locally q_1 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
i : ι
ω : Ω
h :
  stoppedProcess
      (fun (i : ι) ↦
        Set.indicator ({a : Ω | ⊥ < hqX.localSeq (p := q) n a} ∩ {a : Ω | ⊥ < hpX.localSeq (p := p) n a})
          (stoppedProcess X (hpX.localSeq (p := p) n) i))
      (hqX.localSeq (p := q) n) i ω =
    Set.indicator {ω : Ω | ⊥ < hqX.localSeq (p := q) n ω}
      (Set.indicator {ω : Ω | ⊥ < hpX.localSeq (p := p) n ω}
        (stoppedProcess (stoppedProcess X (hpX.localSeq (p := p) n)) (hqX.localSeq (p := q) n) i))
      ω
⊢ Set.indicator {ω : Ω | ⊥ < hpX.localSeq (p := p) n ω ∧ ⊥ < hqX.localSeq (p := q) n ω}
      (stoppedProcess X (hqX.localSeq (p := q) n ⊓ hpX.localSeq (p := p) n) i) ω =
    Set.indicator {ω : Ω | ⊥ < hqX.localSeq (p := q) n ω}
      (Set.indicator {ω : Ω | ⊥ < hpX.localSeq (p := p) n ω}
        (stoppedProcess (stoppedProcess X (hpX.localSeq (p := p) n)) (hqX.localSeq (p := q) n) i))
      ω

Tactic:
rw [← stoppedProcess_stoppedProcess, ← stoppedProcess_indicator_comm, Set.setOf_and,
    Set.inter_comm]

Premises used: MeasureTheory.stoppedProcess_stoppedProcess, Set.setOf_and, Set.inter_comm, MeasureTheory.stoppedProcess_indicator_comm
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p_1 q_1 : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
hp_1 : IsStable 𝓕 p_1
hq_1 : IsStable 𝓕 q_1
h_1 : Locally p_1 𝓕 X P ∧ Locally q_1 𝓕 X P
hpX_1 : Locally p_1 𝓕 X P
hqX_1 : Locally q_1 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
i : ι
ω : Ω
h :
  stoppedProcess
      (fun (i : ι) ↦
        Set.indicator {a : Ω | ⊥ < hqX.localSeq (p := q) n a}
          (Set.indicator {a : Ω | ⊥ < hpX.localSeq (p := p) n a} (stoppedProcess X (hpX.localSeq (p := p) n) i)))
      (hqX.localSeq (p := q) n) i ω =
    Set.indicator {ω : Ω | ⊥ < hqX.localSeq (p := q) n ω}
      (Set.indicator {ω : Ω | ⊥ < hpX.localSeq (p := p) n ω}
        (stoppedProcess (stoppedProcess X (hpX.localSeq (p := p) n)) (hqX.localSeq (p := q) n) i))
      ω
⊢ stoppedProcess
      (fun (i : ι) ↦
        Set.indicator ({a : Ω | ⊥ < hqX.localSeq (p := q) n a} ∩ {a : Ω | ⊥ < hpX.localSeq (p := p) n a})
          (stoppedProcess X (hpX.localSeq (p := p) n) i))
      (hqX.localSeq (p := q) n) i ω =
    Set.indicator {ω : Ω | ⊥ < hqX.localSeq (p := q) n ω}
      (Set.indicator {ω : Ω | ⊥ < hpX.localSeq (p := p) n ω}
        (stoppedProcess (stoppedProcess X (hpX.localSeq (p := p) n)) (hqX.localSeq (p := q) n) i))
      ω

Tactic:
simp_rw [← Set.indicator_indicator]

Premises used: Set.indicator_indicator
-- Module: Mathlib.Probability.Process.LocalProperty
Goal:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p_1 q_1 : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
hp_1 : IsStable 𝓕 p_1
hq_1 : IsStable 𝓕 q_1
h : Locally p_1 𝓕 X P ∧ Locally q_1 𝓕 X P
hpX_1 : Locally p_1 𝓕 X P
hqX_1 : Locally q_1 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
i : ι
ω : Ω
⊢ stoppedProcess
      (fun (i : ι) ↦
        Set.indicator {a : Ω | ⊥ < hqX.localSeq (p := q) n a}
          (Set.indicator {a : Ω | ⊥ < hpX.localSeq (p := p) n a} (stoppedProcess X (hpX.localSeq (p := p) n) i)))
      (hqX.localSeq (p := q) n) i ω =
    Set.indicator {ω : Ω | ⊥ < hqX.localSeq (p := q) n ω}
      (Set.indicator {ω : Ω | ⊥ < hpX.localSeq (p := p) n ω}
        (stoppedProcess (stoppedProcess X (hpX.localSeq (p := p) n)) (hqX.localSeq (p := q) n) i))
      ω

Tactic:
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 : DenselyOrdered ι
inst_4 : FirstCountableTopology ι
inst_5 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
inst_6 : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
h :
  ∀ (ω : Ω) (hω : Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ τ x ω) atTop (𝓝 ⊤)),
    Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ ⨅ (j : ℕ), ⨅ (_ : j ≥ x), τ j ω) atTop (𝓝 ⊤)
⊢ ∀ᵐ (ω : Ω) ∂P, Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ ⨅ (j : ℕ), ⨅ (_ : j ≥ x), τ j ω) atTop (𝓝 ⊤)

Tactic:
filter_upwards [hτ.tendsto_top] with ω hω

Premises used: 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 : DenselyOrdered ι
inst_4 : FirstCountableTopology ι
inst_5 : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
inst_6 : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
ω : Ω
hω : Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ τ x ω) atTop (𝓝 ⊤)
⊢ Eq.{u_1 + 1} (α := WithTop ι) (liminf (fun (x : ℕ) ↦ τ x ω) atTop) ⊤

Tactic:
replace hω := hω.liminf_eq
-- 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 ι) (liminf (fun (x : ℕ) ↦ τ x ω) atTop) ⊤
⊢ Eq.{u_1 + 1} (α := WithTop ι) (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), τ i ω) ⊤

Tactic:
rw [liminf_eq_iSup_iInf_of_nat] at hω

Premises used: Filter.liminf_eq_iSup_iInf_of_nat
-- 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 :
  Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ ⨅ (j : ℕ), ⨅ (_ : j ≥ x), τ j ω) atTop
    (𝓝 (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), τ i ω))
⊢ Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ ⨅ (j : ℕ), ⨅ (_ : j ≥ x), τ j ω) atTop (𝓝 ⊤)

Tactic:
rw [← hω]