awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
this :
  ∀ (ω : Ω),
    ((↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) →
      (↑ε : ℝ) ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω
h :
  (↑ε : ℝ) * μ.real {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a} ≤
    ∫ (x : Ω) in {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ
rw :
  ε • ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}) ≤
    ∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ
ha :
  HSMul.hSMul (β := ℝ≥0∞) ε
      ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) ≠
    ∞
⊢ HSMul.hSMul (β := ℝ≥0∞) ε
      ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) ≤
    ENNReal.ofReal
      (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω},
        stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
have hb : LE.le (α := ℝ) 0
  (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω},
    stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
Tactic: rw [ENNReal.le_ofReal_iff_toReal_le, ENNReal.toReal_smul]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}, f n ω ∂μ) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ)
have rw : ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
  ENNReal.ofReal
    (∫ (x : Ω) in
      {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω} ∪
        {ω : Ω | ((range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
      f n x ∂μ)
Tactic: rw [← ENNReal.ofReal_add, ← setIntegral_union]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
rw :
  ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal
      (∫ (x : Ω) in
        {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
        f n x ∂μ)
⊢ ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}, f n ω ∂μ) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ)
have hst : Disjoint.{u_1} (α := Set Ω) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω}
  {ω : Ω | ((range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}
Tactic: rw [← ENNReal.ofReal_add, ← setIntegral_union]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
rw :
  ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal
      (∫ (x : Ω) in
        {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
        f n x ∂μ)
hst :
  Disjoint.{u_1} (α := Set Ω) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}
    {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}
⊢ ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}, f n ω ∂μ) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ)
have ht : MeasurableSet.{u_1} (α := Ω) {ω : Ω | ((range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}
Tactic: rw [← ENNReal.ofReal_add, ← setIntegral_union]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
rw :
  ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal
      (∫ (x : Ω) in
        {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
        f n x ∂μ)
hst :
  Disjoint.{u_1} (α := Set Ω) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}
    {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}
ht : MeasurableSet.{u_1} (α := Ω) {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}
⊢ ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}, f n ω ∂μ) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ)
have hfs : IntegrableOn (f n) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω} μ
Tactic: rw [← ENNReal.ofReal_add, ← setIntegral_union]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
rw :
  ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal
      (∫ (x : Ω) in
        {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
        f n x ∂μ)
hst :
  Disjoint.{u_1} (α := Set Ω) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}
    {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}
ht : MeasurableSet.{u_1} (α := Ω) {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}
hfs : IntegrableOn (f n) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} μ
⊢ ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}, f n ω ∂μ) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ)
have hft : IntegrableOn (f n) {ω : Ω | ((range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)} μ
Tactic: rw [← ENNReal.ofReal_add, ← setIntegral_union]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
rw :
  ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal
      (∫ (x : Ω) in
        {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
        f n x ∂μ)
hst :
  Disjoint.{u_1} (α := Set Ω) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}
    {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}
ht : MeasurableSet.{u_1} (α := Ω) {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}
hfs : IntegrableOn (f n) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} μ
hft : IntegrableOn (f n) {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)} μ
⊢ ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}, f n ω ∂μ) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ)
have hp : LE.le (α := ℝ) 0 (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω}, f n ω ∂μ)
Tactic: rw [← ENNReal.ofReal_add, ← setIntegral_union]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
rw :
  ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal
      (∫ (x : Ω) in
        {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
        f n x ∂μ)
hst :
  Disjoint.{u_1} (α := Set Ω) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}
    {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}
ht : MeasurableSet.{u_1} (α := Ω) {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}
hfs : IntegrableOn (f n) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} μ
hft : IntegrableOn (f n) {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)} μ
hp : LE.le (α := ℝ) 0 (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}, f n ω ∂μ)
⊢ ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}, f n ω ∂μ) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ)
have hq : LE.le (α := ℝ) 0 (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ)
Tactic: rw [← ENNReal.ofReal_add, ← setIntegral_union]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal
      (∫ (x : Ω) in
        {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
        f n x ∂μ)
have rw : ENNReal.ofReal (∫ (x : Ω) in Set.univ, f n x ∂μ) =
  ENNReal.ofReal
    (∫ (x : Ω) in
      {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω} ∪
        {ω : Ω | ((range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
      f n x ∂μ)
Tactic: rw [← setIntegral_univ]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ ENNReal.ofReal (∫ (x : Ω) in Set.univ, f n x ∂μ) =
    ENNReal.ofReal
      (∫ (x : Ω) in
        {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
        f n x ∂μ)
have h : Eq.{u_1 + 1} (α := Set Ω)
  ({ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω} ∪
    {ω : Ω | ((range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)})
  Set.univ
Tactic: convert! rfl
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ Eq.{u_1 + 1} (α := Set Ω)
    ({ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
      {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)})
    Set.univ
have h : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω)
      ({ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω} ∪
        {ω : Ω | ((range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)})
      ω ↔
    Membership.mem (γ := Set Ω) Set.univ ω
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) ≤
    ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}, f n ω ∂μ)
have hadd : ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
  ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω}, f n ω ∂μ) +
    ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ)
Tactic: have hadd : ENNReal.ofReal (∫ ω, f n ω ∂μ) =
      ENNReal.ofReal
        (∫ ω in {ω | ε ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω}, f n ω ∂μ) +
      ENNReal.ofReal
        (∫ ω in {ω | ((range (n + 1)).sup' nonempty_range_add_one fun k => f k ω) < ε},
          f n ω ∂μ) := by
      rw [← ENNReal.ofReal_add, ← setIntegral_union]
      · rw [← setIntegral_univ]
        convert! rfl
        ext ω
        change (ε : ℝ) ≤ _ ∨ _ < (ε : ℝ) ↔ _
        simp only [le_or_gt, Set.mem_univ]
      · grind
      · exact measurableSet_lt (measurable_range_sup'' fun n _ =>
          (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)) measurable_const
      exacts [(hsub.integrable _).integrableOn, (hsub.integrable _).integrableOn,
        integral_nonneg (hnonneg _), integral_nonneg (hnonneg _)]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
hadd :
  ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}, f n ω ∂μ) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ)
⊢ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) ≤
    ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}, f n ω ∂μ)
have rwa : ∀
  (this :
    HSMul.hSMul (β := ℝ≥0∞) ε
          ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
        ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω}, f n ω ∂μ) +
        ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ))
  (hadd :
    ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω}, f n ω ∂μ) +
        ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ)),
  HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) ≤
    ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω}, f n ω ∂μ)
Tactic: rwa [hadd, ENNReal.add_le_add_iff_right ENNReal.ofReal_ne_top] at this
Cleared hypotheses: this, hadd
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
hadd :
  ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}, f n ω ∂μ) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ)
rwa :
  ∀
    (this :
      HSMul.hSMul (β := ℝ≥0∞) ε
            ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
          ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
        ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}, f n ω ∂μ) +
          ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ))
    (hadd :
      ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
        ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}, f n ω ∂μ) +
          ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ)),
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) ≤
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}, f n ω ∂μ)
⊢ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) ≤
    ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}, f n ω ∂μ)
have rwa₁ : ∀
  (this :
    HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) ≤
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω}, f n ω ∂μ))
  (hadd :
    ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω}, f n ω ∂μ) +
        ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ)),
  HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) ≤
    ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω}, f n ω ∂μ)
Tactic: rwa [hadd, ENNReal.add_le_add_iff_right ENNReal.ofReal_ne_top] at this
Cleared hypotheses: this, hadd