-- Mathlib/Probability/Martingale/OptionalStopping.lean
theorem maximal_ineq [IsFiniteMeasure μ] (hsub : Submartingale f 𝒢 μ) (hnonneg : 0 ≤ f) {ε : ℝ≥0}
    (n : ℕ) : ε • μ {ω | (ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_succ fun k => f k ω} ≤
    ENNReal.ofReal (∫ ω in {ω | (ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_succ fun k => f k ω},
      f n ω ∂μ)

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω : ω ∈ {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}
⊢ f n ω ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω

Tactic:
rw [Set.mem_setOf_eq] at hω

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω : ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε
⊢ f n ω ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} +
      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 ω ∂μ)
⊢ ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} ≤
    ENNReal.ofReal (∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω}, f n ω ∂μ)

Tactic:
rwa [hadd, ENNReal.add_le_add_iff_right ENNReal.ofReal_ne_top] at this

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ ∀ x ∈ {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}, f n x ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) x

Tactic:
intro ω hω

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω : ω ∈ {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}
⊢ f n ω ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω

Proof state:
case hst.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω₂ : ω ∈ {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}
hω₁ : ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω
⊢ ω ∈ ⊥

Tactic:
change _ < (ε : ℝ) at hω₂

Result:
case hst.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω₁ : ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω
hω₂ : ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε
⊢ ω ∈ ⊥

Proof state:
case hst.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} +
      ENNReal.ofReal (∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
ω : Ω
hω₂ : ω ∈ {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}
hω₁ : ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω
⊢ ω ∈ ⊥

Tactic:
change _ < (ε : ℝ) at hω₂

Result:
case hst.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} +
      ENNReal.ofReal (∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
ω : Ω
hω₁ : ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω
hω₂ : ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε
⊢ ω ∈ ⊥

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ ENNReal.ofReal
        (∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω},
          stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ) +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε},
          stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ) =
    ENNReal.ofReal (∫ (ω : Ω), stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ)

Tactic:
rw [← ENNReal.ofReal_add, ← setIntegral_union]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ ENNReal.ofReal
      (∫ (x : Ω) in
        {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} ∪ {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε},
        stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) x ∂μ) =
    ENNReal.ofReal (∫ (ω : Ω), stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ)

case hst
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ Disjoint {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}

case ht
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ MeasurableSet {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}

case hfs
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IntegrableOn (stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n)) {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} μ

case hft
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IntegrableOn (stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n)) {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε} μ

case hp
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ 0 ≤ ∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω}, stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ

case hq
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ 0 ≤ ∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}, stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ