awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h : edist s t = 0
⊢ (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω) ^ p) 0
have rw : ∫⁻ (a : Ω), edist (X s a) (X t a) ^ p ∂P ≤ 0
Tactic: rw [← lintegral_eq_zero_iff' (hX.aemeasurable_edist.pow_const p), ← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h : edist s t = 0
⊢ ∫⁻ (a : Ω), edist (X s a) (X t a) ^ p ∂P ≤ 0
have calc : (↑M : ℝ≥0∞) * edist s t ^ q = 0
Tactic: calc ∫⁻ ω, edist (X s ω) (X t ω) ^ p ∂P
  _ ≤ M * edist s t ^ q := hX.kolmogorovCondition s t
  _ = 0 := by simp [h, hX.q_pos]
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
this : (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω) ^ p) 0
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0
have h : ∀ (ω : Ω) (hω : edist (X s ω) (X t ω) ^ p = 0 ω), edist (X s ω) (X t ω) = 0
Tactic: filter_upwards [this] with ω hω
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0
have suffices : (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω) ^ p) 0
Tactic: suffices (fun ω ↦ edist (X s ω) (X t ω) ^ p) =ᵐ[P] 0 by
    filter_upwards [this] with ω hω
    simpa [hX.p_pos, not_lt_of_gt hX.p_pos] using hω
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
⊢ (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω) ^ p) 0
have rw : ∫⁻ (a : Ω), edist (X s a) (X t a) ^ p ∂P ≤ 0
Tactic: rw [← lintegral_eq_zero_iff' (hX.aemeasurable_edist.pow_const p), ← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
⊢ ∫⁻ (a : Ω), edist (X s a) (X t a) ^ p ∂P ≤ 0
have calc : 0 * edist s t ^ q = 0
Tactic: calc ∫⁻ ω, edist (X s ω) (X t ω) ^ p ∂P
  _ ≤ 0 * edist s t ^ q := hX.kolmogorovCondition s t
  _ = 0 := by simp
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
τ σ : ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : IsLocalizingSequence 𝓕 σ P
⊢ ∀ᵐ (ω : Ω) ∂P, Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ (τ ⊓ σ) x ω) atTop (𝓝 ⊤)
have h : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω)
          {x : Ω | (fun (ω : Ω) ↦ Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ τ x ω) atTop (𝓝 ⊤)) x} x →
        Membership.mem (γ := Set Ω)
          {x : Ω |
            Membership.mem (γ := Set Ω)
                {x : Ω | (fun (ω : Ω) ↦ Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ σ x ω) atTop (𝓝 ⊤)) x} x →
              Membership.mem (γ := Set Ω)
                {x : Ω | (fun (ω : Ω) ↦ Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ (τ ⊓ σ) x ω) atTop (𝓝 ⊤)) x} x}
          x}
    a
Tactic: filter_upwards [hτ.tendsto_top, hσ.tendsto_top] with ω hτω hσω using hτω.min hσω
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
τ σ : ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : IsLocalizingSequence 𝓕 σ P
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω)
            {x : Ω | (fun (ω : Ω) ↦ Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ τ x ω) atTop (𝓝 ⊤)) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              Membership.mem (γ := Set Ω)
                  {x : Ω | (fun (ω : Ω) ↦ Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ σ x ω) atTop (𝓝 ⊤)) x} x →
                Membership.mem (γ := Set Ω)
                  {x : Ω | (fun (ω : Ω) ↦ Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ (τ ⊓ σ) x ω) atTop (𝓝 ⊤)) x}
                  x}
            x}
      a
⊢ ∀ᵐ (ω : Ω) ∂P, Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ (τ ⊓ σ) x ω) atTop (𝓝 ⊤)
have h₁ : ∀ (a : Ω),
  Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ τ x a) atTop (𝓝 ⊤) →
    Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ σ x a) atTop (𝓝 ⊤) →
      Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ (τ ⊓ σ) x a) atTop (𝓝 ⊤)
Tactic: filter_upwards [hτ.tendsto_top, hσ.tendsto_top] with ω hτω hσω using hτω.min hσω
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
τ σ : ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : IsLocalizingSequence 𝓕 σ P
⊢ ∀ᵐ (ω : Ω) ∂P, Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ (τ ⊓ σ) x ω
have h : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ τ x ω) x} x →
        Membership.mem (γ := Set Ω)
          {x : Ω |
            Membership.mem (γ := Set Ω)
                {x : Ω | (fun (ω : Ω) ↦ Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ σ x ω) x} x →
              Membership.mem (γ := Set Ω)
                {x : Ω | (fun (ω : Ω) ↦ Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ (τ ⊓ σ) x ω) x} x}
          x}
    a
Tactic: filter_upwards [hτ.mono, hσ.mono] with ω hτω hσω using hτω.min hσω
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder ι
𝓕 : Filtration ι mΩ
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
τ σ : ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : IsLocalizingSequence 𝓕 σ P
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ τ x ω) x}
            x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              Membership.mem (γ := Set Ω)
                  {x : Ω | (fun (ω : Ω) ↦ Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ σ x ω) x} x →
                Membership.mem (γ := Set Ω)
                  {x : Ω | (fun (ω : Ω) ↦ Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ (τ ⊓ σ) x ω) x} x}
            x}
      a
⊢ ∀ᵐ (ω : Ω) ∂P, Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ (τ ⊓ σ) x ω
have h₁ : ∀ (a : Ω),
  (Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ τ x a) →
    (Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ σ x a) →
      Monotone.{0, u_1} (β := WithTop ι) fun (x : ℕ) ↦ (τ ⊓ σ) x a
Tactic: filter_upwards [hτ.mono, hσ.mono] with ω hτω hσω using hτω.min hσω
-- 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 : LinearOrder ι
𝓕 : Filtration ι mΩ
p : (ι → Ω → E) → Prop
inst_1 : OrderBot ι
inst_2 : Zero E
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
hp : IsStable 𝓕 p
⊢ IsStable.{u_1, u_2, u_3} (E := E) 𝓕 fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P
have refine : ∀ (X : ι → Ω → E) (hX : (fun (Y : ι → Ω → E) ↦ Locally p 𝓕 Y P) X) (τ : Ω → WithTop ι) (hτ : IsStoppingTime 𝓕 τ)
  (n : ℕ),
  p
    (stoppedProcess
      (fun (i : ι) ↦
        Set.indicator {ω : Ω | ⊥ < Locally.localSeq (p := p) hX n ω}
          (stoppedProcess (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < τ ω} (X i)) τ i))
      (Locally.localSeq (p := p) hX n))
Tactic: refine fun X hX τ hτ ↦ ⟨hX.localSeq, hX.isLocalizingSequence_localSeq, fun n ↦ ?_⟩
-- 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 : 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
    (stoppedProcess
      (fun (i : ι) ↦
        Set.indicator {ω : Ω | ⊥ < Locally.localSeq (p := p) hX n ω}
          (stoppedProcess (fun (i : ι) ↦ Set.indicator {ω : Ω | ⊥ < τ ω} (X i)) τ i))
      (Locally.localSeq (p := p) hX n))
have simp_rw : p fun (i : ι) ↦
  Set.indicator {ω : Ω | ⊥ < τ ω}
    (Set.indicator {ω : Ω | ⊥ < Locally.localSeq (p := p) hX n ω}
      (stoppedProcess (stoppedProcess X (Locally.localSeq (p := p) hX n)) τ i))
Tactic: simp_rw [← stoppedProcess_indicator_comm', Set.indicator_indicator, Set.inter_comm,
    ← Set.indicator_indicator, stoppedProcess_stoppedProcess, inf_comm,
    stoppedProcess_indicator_comm', ← stoppedProcess_stoppedProcess]
-- 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 : 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
have 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))
Tactic: refine ⟨Locally.of_and, fun ⟨hpX, hqX⟩ ↦
    ⟨_, hpX.isLocalizingSequence_localSeq.min hqX.isLocalizingSequence_localSeq, fun n ↦ ?_⟩⟩
-- 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 : 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))
have 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))
Tactic: refine ⟨this p q hp hq hpX hqX, ?_⟩
-- 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 : 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 {ω : Ω | ⊥ < (hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n ω} (X i))
      ((hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n))
have 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))
Tactic: simp_rw [inf_comm hpX.localSeq]
-- 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 : 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 : ℕ
⊢ (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))
have 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))
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
-- 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 : 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 {ω : Ω | ⊥ < (hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n ω} (X i))
      ((hpX.localSeq (p := p) ⊓ hqX.localSeq (p := q)) n))
have 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))
Tactic: convert!
    hp _ (hpX.stoppedProcess_localSeq n) _ <|
      hqX.isLocalizingSequence_localSeq.isStoppingTime n using 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 : 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
⊢ 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))
have 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 ω)
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 : 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 : ι
ω : Ω
⊢ 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 ω)
have 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))
    ω
Tactic: simp_rw [stoppedProcess_indicator_comm, Pi.inf_apply, lt_inf_iff, inf_comm (hpX.localSeq n)]
-- 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 : 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 : ι
ω : Ω
⊢ 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))
      ω
have 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))
    ω
Tactic: rw [← stoppedProcess_stoppedProcess, ← stoppedProcess_indicator_comm, Set.setOf_and,
    Set.inter_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 : 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} ∩ {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))
      ω
have 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))
    ω
Tactic: simp_rw [← Set.indicator_indicator]
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (goal)
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
⊢ ∀ᵐ (ω : Ω) ∂P, Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ ⨅ (j : ℕ), ⨅ (_ : j ≥ x), τ j ω) atTop (𝓝 ⊤)
have h : ∀ (ω : Ω) (hω : Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ τ x ω) atTop (𝓝 ⊤)),
  Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ ⨅ (j : ℕ), ⨅ (_ : j ≥ x), τ j ω) atTop (𝓝 ⊤)
Tactic: filter_upwards [hτ.tendsto_top] with ω hω
-- Lean 4 proof step from Mathlib.Probability.Process.LocalProperty (hypothesis)
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 (𝓝 ⊤)
⊢ Tendsto.{0, u_1} (β := WithTop ι) (fun (x : ℕ) ↦ ⨅ (j : ℕ), ⨅ (_ : j ≥ x), τ j ω) atTop (𝓝 ⊤)
have hω₁ : Eq.{u_1 + 1} (α := WithTop ι) (liminf (fun (x : ℕ) ↦ τ x ω) atTop) ⊤
Tactic: replace hω := hω.liminf_eq
Cleared hypotheses: hω