Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: Ω : 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 ω)) ω
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 ω)) x ∂μ
⊢ ε • (μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω}).toReal ≤
    ∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω},
      stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω ∂μ

pp: case ha
Ω : 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 ω)) ω
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 ω)) x ∂μ
⊢ ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} ≠ ∞

pp: case hb
Ω : 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 ω)) ω
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 ω)) x ∂μ
⊢ 0 ≤
    ∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω},
      stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω ∂μ

Tactic:
]

Goal state after:
Ω : 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 ω)) ω
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 ω)) x ∂μ
⊢ ε • (μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω}).toReal ≤
    ∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω},
      stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω ∂μ

case ha
Ω : 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 ω)) ω
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 ω)) x ∂μ
⊢ ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} ≠ ∞

case hb
Ω : 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 ω)) ω
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 ω)) x ∂μ
⊢ 0 ≤
    ∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω},
      stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω ∂μ