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 : 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 :
  ∀ (i : ι) (ω : Ω),
    Eq.{u_3 + 1} (α := 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) ω)) i ω)
      (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)) i ω)
⊢ 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)))

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 : 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 : ℕ
i : ι
ω : Ω
h :
  Eq.{u_3 + 1} (α := E)
    ((fun (i : ι) ↦
        Set.indicator {ω : Ω | ⊥ < min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω) (τ n (nk n) ω)}
          (stoppedProcess X
            (fun (ω : Ω) ↦ min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω) (τ n (nk n) ω)) i))
      i ω)
    ((fun (i : ι) ↦
        (Set.indicator {ω : Ω | ⊥ < τ n (nk n) ω}
            ((fun (i : ι) ↦
                Set.indicator {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω}
                  (stoppedProcess X (τ n (nk n) ⊓ hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n) i))
              i) :
          (x : Ω) → E))
      i ω)
⊢ Eq.{u_3 + 1} (α := 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) ω)) i ω)
    (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)) i ω)

Tactic:
rw [stoppedProcess_indicator_comm', stoppedProcess_indicator_comm',
    stoppedProcess_stoppedProcess, stoppedProcess_indicator_comm']

Premises used: MeasureTheory.stoppedProcess_stoppedProcess, 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 : 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 : ℕ
i : ι
ω : Ω
h :
  Set.indicator {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω ∧ ⊥ < τ n (nk n) ω}
      (stoppedProcess X
        (fun (ω : Ω) ↦ min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω) (τ n (nk n) ω)) i)
      ω =
    Set.indicator
      ({ω : Ω | ⊥ < τ n (nk n) ω} ∩ {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω})
      (stoppedProcess X (τ n (nk n) ⊓ hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n) i) ω
⊢ Eq.{u_3 + 1} (α := E)
    ((fun (i : ι) ↦
        Set.indicator {ω : Ω | ⊥ < min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω) (τ n (nk n) ω)}
          (stoppedProcess X
            (fun (ω : Ω) ↦ min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω) (τ n (nk n) ω)) i))
      i ω)
    ((fun (i : ι) ↦
        (Set.indicator {ω : Ω | ⊥ < τ n (nk n) ω}
            ((fun (i : ι) ↦
                Set.indicator {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω}
                  (stoppedProcess X (τ n (nk n) ⊓ hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n) i))
              i) :
          (x : Ω) → E))
      i ω)

Tactic:
simp only [lt_inf_iff, Set.indicator_indicator]

Premises used: lt_inf_iff, 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 : 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 : ℕ
i : ι
ω : Ω
h :
  Eq.{u_2 + 1} (α := Set Ω)
    {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω ∧ ⊥ < τ n (nk n) ω}
    ({ω : Ω | ⊥ < τ n (nk n) ω} ∩ {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω})
h₁ :
  stoppedProcess X (fun (ω : Ω) ↦ min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω) (τ n (nk n) ω)) i =
    stoppedProcess X (τ n (nk n) ⊓ hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n) i
⊢ Set.indicator {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω ∧ ⊥ < τ n (nk n) ω}
      (stoppedProcess X
        (fun (ω : Ω) ↦ min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω) (τ n (nk n) ω)) i)
      ω =
    Set.indicator
      ({ω : Ω | ⊥ < τ n (nk n) ω} ∩ {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω})
      (stoppedProcess X (τ n (nk n) ⊓ hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n) i) ω

Tactic:
congr 1
-- 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 : ℕ
i : ι
ω : Ω
h :
  ∀ (x : Ω),
    Membership.mem (γ := Set Ω)
        {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω ∧ ⊥ < τ n (nk n) ω} x ↔
      Membership.mem (γ := Set Ω)
        ({ω : Ω | ⊥ < τ n (nk n) ω} ∩ {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω}) x
⊢ Eq.{u_2 + 1} (α := Set Ω)
    {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω ∧ ⊥ < τ n (nk n) ω}
    ({ω : Ω | ⊥ < τ n (nk n) ω} ∩ {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω})

Tactic:
ext
-- 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 : ℕ
i : ι
ω x : Ω
⊢ Membership.mem (γ := Set Ω)
      {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω ∧ ⊥ < τ n (nk n) ω} x ↔
    Membership.mem (γ := Set Ω)
      ({ω : Ω | ⊥ < τ n (nk n) ω} ∩ {ω : Ω | ⊥ < hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω}) x

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 : 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 : ℕ
i : ι
ω : Ω
h :
  stoppedProcess X (fun (ω : Ω) ↦ min (τ n (nk n) ω) (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω)) i =
    stoppedProcess X (τ n (nk n) ⊓ hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n) i
⊢ stoppedProcess X (fun (ω : Ω) ↦ min (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω) (τ n (nk n) ω)) i =
    stoppedProcess X (τ n (nk n) ⊓ hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n) i

Tactic:
simp_rw [inf_comm]

Premises used: inf_comm
-- 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 : ℕ
i : ι
ω : Ω
⊢ stoppedProcess X (fun (ω : Ω) ↦ min (τ n (nk n) ω) (hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n ω)) i =
    stoppedProcess X (τ n (nk n) ⊓ hL.localSeq (p := fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) n) i

Tactic:
rfl
-- 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 q : (ι → Ω → E) → Prop
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
inst_5 : DenselyOrdered ι
inst_6 : NoMaxOrder ι
inst_7 : Zero E
inst_8 : 𝓕.IsRightContinuous
hq : IsStable (mΩ := mΩ) 𝓕 q
hpq : ∀ (Y : ι → Ω → E), p Y → Locally q 𝓕 Y P
hpX : Locally p 𝓕 X P
⊢ Locally q 𝓕 X P

Tactic:
hq.locally_locally_iff.1 <| hpX.mono hpq

Premises used: Iff.mp, ProbabilityTheory.Locally.mono, ProbabilityTheory.IsStable.locally_locally_iff
-- 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 q : (ι → Ω → E) → Prop
inst_3 : SecondCountableTopology ι
inst_4 : IsFiniteMeasure P
inst_5 : DenselyOrdered ι
inst_6 : NoMaxOrder ι
inst_7 : Zero E
r : (ι → Ω → E) → Prop
inst_8 : 𝓕.IsRightContinuous
hrpq : ∀ (Y : ι → Ω → E), r Y → p Y → Locally q 𝓕 Y P
hr : IsStable (mΩ := mΩ) 𝓕 r
hp : IsStable (mΩ := mΩ) 𝓕 p
hq : IsStable (mΩ := mΩ) 𝓕 q
hrX : Locally r 𝓕 X P
hpX : Locally p 𝓕 X P
⊢ Locally q 𝓕 X P

Tactic:
hq.locally_induction (p := fun Y ↦ r Y ∧ p Y) (and_imp.2 <| hrpq ·) <|
    (hr.locally_and_iff hp).2 ⟨hrX, hpX⟩

Premises used: Iff.mpr, and_imp, ProbabilityTheory.IsStable.locally_induction, And.intro, ProbabilityTheory.IsStable.locally_and_iff
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet s

Tactic:
measurableSet_generateFrom hs

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
a : α
⊢ MeasurableSet (memPartitionSet t n a)

Tactic:
measurableSet_partitionFiltration_of_mem ht n (memPartitionSet_mem t n a)

Premises used: ProbabilityTheory.measurableSet_partitionFiltration_of_mem, memPartitionSet_mem
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
m_1 : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace (↑(memPartition t n) : Type u_1)
⊢ Measurable (β := (↑(memPartition t n) : Type u_1)) fun (a : α) ↦
    Subtype.mk (p := fun (x : Set α) ↦ x ∈ memPartition t n) (memPartitionSet t n a) ⋯

Tactic:
@measurable_to_countable' (memPartition t n) α m _
    (partitionFiltration ht n) _ (fun s ↦ ?_)

Premises used: measurable_to_countable'
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
m_1 : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace (↑(memPartition t n) : Type u_1)
refine :
  ∀ (s : (↑(memPartition t n) : Type u_1)),
    MeasurableSet (α := α)
      (Set.preimage (β := (↑(memPartition t n) : Type u_1))
        (fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ memPartition t n) (memPartitionSet t n a) ⋯) {s})
⊢ Measurable (β := (↑(memPartition t n) : Type u_1)) fun (a : α) ↦
    Subtype.mk (p := fun (x : Set α) ↦ x ∈ memPartition t n) (memPartitionSet t n a) ⋯

Tactic:
refine @measurable_to_countable' (memPartition t n) α m _
    (partitionFiltration ht n) _ (fun s ↦ ?_)

Premises used: measurable_to_countable'
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
m_1 : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace (↑(memPartition t n) : Type u_1)
s : (↑(memPartition t n) : Type u_1)
rcases :
  ∀ (s : Set α) (hs : s ∈ memPartition t n),
    MeasurableSet (α := α)
      (Set.preimage (β := (↑(memPartition t n) : Type u_1))
        (fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ memPartition t n) (memPartitionSet t n a) ⋯)
        {Subtype.mk (p := fun (x : Set α) ↦ x ∈ memPartition t n) s hs})
⊢ MeasurableSet (α := α)
    (Set.preimage (β := (↑(memPartition t n) : Type u_1))
      (fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ memPartition t n) (memPartitionSet t n a) ⋯) {s})

Tactic:
rcases s with ⟨s, hs⟩
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
m_1 : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace (↑(memPartition t n) : Type u_1)
s : Set α
hs : s ∈ memPartition t n
this : MeasurableSet.{u_1} (α := α) {x : α | memPartitionSet t n x = s}
⊢ MeasurableSet.{u_1} (α := α) {x : α | memPartitionSet t n x = s}

Tactic:
this
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
m_1 : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace (↑(memPartition t n) : Type u_1)
s : Set α
hs : s ∈ memPartition t n
this : MeasurableSet.{u_1} (α := α) {x : α | memPartitionSet t n x = s}
h :
  Eq (α := Set α)
    (Set.preimage (β := (↑(memPartition t n) : Type u_1))
      (fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ memPartition t n) (memPartitionSet t n a) ⋯)
      {Subtype.mk (p := fun (x : Set α) ↦ x ∈ memPartition t n) s hs})
    {x : α | memPartitionSet t n x = s}
⊢ MeasurableSet (α := α)
    (Set.preimage (β := (↑(memPartition t n) : Type u_1))
      (fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ memPartition t n) (memPartitionSet t n a) ⋯)
      {Subtype.mk (p := fun (x : Set α) ↦ x ∈ memPartition t n) s hs})

Tactic:
convert! this
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
m_1 : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace (↑(memPartition t n) : Type u_1)
s : Set α
hs : s ∈ memPartition t n
this : MeasurableSet.{u_1} (α := α) {x : α | memPartitionSet t n x = s}
h :
  ∀ (x : α),
    Membership.mem (γ := Set α)
        (Set.preimage (β := (↑(memPartition t n) : Type u_1))
          (fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ memPartition t n) (memPartitionSet t n a) ⋯)
          {Subtype.mk (p := fun (x : Set α) ↦ x ∈ memPartition t n) s hs})
        x ↔
      Membership.mem (γ := Set α) {x : α | memPartitionSet t n x = s} x
⊢ Eq (α := Set α)
    (Set.preimage (β := (↑(memPartition t n) : Type u_1))
      (fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ memPartition t n) (memPartitionSet t n a) ⋯)
      {Subtype.mk (p := fun (x : Set α) ↦ x ∈ memPartition t n) s hs})
    {x : α | memPartitionSet t n x = s}

Tactic:
ext x
-- Module: Mathlib.Probability.Process.PartitionFiltration
Goal:
α : Type u_1
m_1 : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace (↑(memPartition t n) : Type u_1)
s : Set α
hs : s ∈ memPartition t n
this : MeasurableSet.{u_1} (α := α) {x : α | memPartitionSet t n x = s}
x : α
⊢ Membership.mem (γ := Set α)
      (Set.preimage (β := (↑(memPartition t n) : Type u_1))
        (fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ memPartition t n) (memPartitionSet t n a) ⋯)
        {Subtype.mk (p := fun (x : Set α) ↦ x ∈ memPartition t n) s hs})
      x ↔
    Membership.mem (γ := Set α) {x : α | memPartitionSet t n x = s} x

Tactic:
simp