awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
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 : ℕ
⊢ 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)))
have 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 ω)
Tactic: ext i ω
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
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 : ι
ω : Ω
⊢ 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 ω)
have 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 ω)
Tactic: rw [stoppedProcess_indicator_comm', stoppedProcess_indicator_comm',
    stoppedProcess_stoppedProcess, stoppedProcess_indicator_comm']
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
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 : ι
ω : Ω
⊢ 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 ω)
have 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) ω
Tactic: simp only [lt_inf_iff, Set.indicator_indicator]
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
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 : ι
ω : Ω
⊢ 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) ω
have 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 ω})
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
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 ω})
⊢ 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) ω
have 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
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
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 : ι
ω : Ω
⊢ 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 ω})
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
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 (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
have 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
Tactic: simp_rw [inf_comm]
-- Lean 4 proof step from Mathlib.Probability.Process.PartitionFiltration (goal)
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) ⋯
have 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) sorry) {s})
Tactic: refine @measurable_to_countable' (memPartition t n) α m _
    (partitionFiltration ht n) _ (fun s ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Process.PartitionFiltration (goal)
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)
⊢ 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})
have 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) sorry)
      {Subtype.mk (p := fun (x : Set α) ↦ x ∈ memPartition t n) s hs})
Tactic: rcases s with ⟨s, hs⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Probability.Process.PartitionFiltration (goal)
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 (α := α)
    (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})
have 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) sorry)
    {Subtype.mk (p := fun (x : Set α) ↦ x ∈ memPartition t n) s hs})
  {x : α | memPartitionSet t n x = s}
Tactic: convert! this
-- Lean 4 proof step from Mathlib.Probability.Process.PartitionFiltration (goal)
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}
⊢ 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}
have 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) sorry)
        {Subtype.mk (p := fun (x : Set α) ↦ x ∈ memPartition t n) s hs})
      x ↔
    Membership.mem (γ := Set α) {x : α | memPartitionSet t n x = s} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.Process.PartitionFiltration (goal)
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
⊢ 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})
have suffices : MeasurableSet.{u_1} (α := α) {x : α | memPartitionSet t n x = s}
Tactic: suffices MeasurableSet[partitionFiltration ht n] {x | memPartitionSet t n x = s} by
    convert! this
    ext x
    simp
-- Lean 4 proof step from Mathlib.Probability.Process.PartitionFiltration (goal)
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
⊢ MeasurableSet.{u_1} (α := α) {x : α | memPartitionSet t n x = s}
have simp_rw : MeasurableSet.{u_1} (α := α) {x : α | x ∈ s}
Tactic: simp_rw [memPartitionSet_eq_iff _ hs]
-- Lean 4 proof step from Mathlib.Probability.Process.PartitionFiltration (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
| generateFrom (Set.range t)
have rw : ⨆ (i : ℕ), generateFrom (memPartition t i)
Tactic: rw [← generateFrom_iUnion_memPartition t, ← iSup_generateFrom]
-- Lean 4 proof step from Mathlib.Probability.Process.PartitionFiltration (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ ⨆ (n : ℕ), (↑(partitionFiltration (t := t) ht) : ℕ → MeasurableSpace α) n = generateFrom (Set.range t)
have conv_rhs : Eq.{u_1 + 1} (α := MeasurableSpace α) (⨆ (n : ℕ), (↑(partitionFiltration (t := t) ht) : ℕ → MeasurableSpace α) n)
  (⨆ (i : ℕ), generateFrom (memPartition t i))
Tactic: conv_rhs => rw [← generateFrom_iUnion_memPartition t, ← iSup_generateFrom]
-- Lean 4 proof step from Mathlib.Probability.Process.PartitionFiltration (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
ht_range rw : generateFrom (Set.range t) = m
⊢ ⨆ (n : ℕ), (↑(partitionFiltration (t := t) ht) : ℕ → MeasurableSpace α) n = m
have rw₁ : m = m
Tactic: rw [iSup_partitionFiltration_eq_generateFrom_range ht, ht_range]
-- Lean 4 proof step from Mathlib.Probability.Process.PartitionFiltration (goal)
Goal:
α : Type u_2
m : MeasurableSpace α
inst : CountablyGenerated α
| m
have rw : ⨆ (i : ℕ), generateFrom (countablePartition α i)
Tactic: rw [← generateFrom_iUnion_countablePartition α, ← iSup_generateFrom]
-- Lean 4 proof step from Mathlib.Probability.Process.PartitionFiltration (goal)
Goal:
α : Type u_2
m : MeasurableSpace α
inst : CountablyGenerated α
⊢ ⨆ (n : ℕ), (↑(countableFiltration α) : ℕ → MeasurableSpace α) n = m
have conv_rhs : Eq.{u_2 + 1} (α := MeasurableSpace α) (⨆ (n : ℕ), (↑(countableFiltration α) : ℕ → MeasurableSpace α) n)
  (⨆ (i : ℕ), generateFrom (countablePartition α i))
Tactic: conv_rhs => rw [← generateFrom_iUnion_countablePartition α, ← iSup_generateFrom]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet (Set.Ioc i j ×ˢ s)
have inl : ∀ (hij : j ≤ i), MeasurableSet (Set.Ioc i j ×ˢ s)
Tactic: obtain hij | hij := le_total j i
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
inl : ∀ (hij : j ≤ i), MeasurableSet (Set.Ioc i j ×ˢ s)
⊢ MeasurableSet (Set.Ioc i j ×ˢ s)
have inr : ∀ (hij : i ≤ j), MeasurableSet (Set.Ioc i j ×ˢ s)
Tactic: obtain hij | hij := le_total j i
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : LinearOrder ι
inst_1 : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
hij : i ≤ j
⊢ MeasurableSet (Set.Ioc i j ×ˢ s)
have inr : MeasurableSet (Set.Ioi i ×ˢ s \ Set.Ioi j ×ˢ s)
Tactic: rw [← Set.Ioi_diff_Ioi, (by simp : (Set.Ioi i \ Set.Ioi j) ×ˢ s
      = Set.Ioi i ×ˢ (s \ s) ∪ (Set.Ioi i \ Set.Ioi j) ×ˢ s), ← Set.prod_diff_prod]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
n : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet (SProd.sprod (α := Set ℕ) {n + 1} s)
have rw : MeasurableSet (Set.Ioc n (n + 1) ×ˢ s)
Tactic: rw [(_ : {n + 1} = Set.Ioc n (n + 1))]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
n : ℕ
s : Set Ω
hs : MeasurableSet s
rw : MeasurableSet (Set.Ioc n (n + 1) ×ˢ s)
⊢ MeasurableSet (SProd.sprod (α := Set ℕ) {n + 1} s)
have rw₁ : {n + 1} = Set.Ioc n (n + 1)
Tactic: rw [(_ : {n + 1} = Set.Ioc n (n + 1))]
-- Lean 4 proof step from Mathlib.Probability.Process.Predictable (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
n : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ {n + 1} = Set.Ioc n (n + 1)
have h : ∀ (m : ℕ), Membership.mem (γ := Set ℕ) {n + 1} m ↔ m ∈ Set.Ioc n (n + 1)
Tactic: ext m