-- Mathlib/Probability/Martingale/OptionalStopping.lean
theorem smul_le_stoppedValue_hitting [IsFiniteMeasure μ] (hsub : Submartingale 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 ω},
      stoppedValue f (hitting f {y : ℝ | ↑ε ≤ y} 0 n) ω ∂μ)

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
hn : Set.Icc 0 n = {k | k ≤ n}
this : ∀ (ω : Ω), (↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω) → ↑ε ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω
h :
  ↑ε * (μ {a | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k a}).toReal ≤
    ∫ (x : Ω) in {a | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k a}, stoppedValue f (hitting 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 (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ

Tactic:
exact h

Result:
no goals

Proof state:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n x : ℕ
⊢ x ∈ Set.Icc 0 n ↔ x ∈ {k | k ≤ n}

Tactic:
simp

Result:
no goals

Proof state:
case hb
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
hn : Set.Icc 0 n = {k | k ≤ n}
this : ∀ (ω : Ω), (↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω) → ↑ε ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω
h :
  ↑ε * (μ {a | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k a}).toReal ≤
    ∫ (x : Ω) in {a | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k a}, stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) x ∂μ
⊢ 0 ≤ ∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω}, stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ

Tactic:
exact le_trans (mul_nonneg ε.coe_nonneg ENNReal.toReal_nonneg) h

Result:
no goals

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

Tactic:
have hn : Set.Icc 0 n = {k | k ≤ n} := by ext x; simp

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

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

Tactic:
have : ∀ ω, ((ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_succ fun k => f k ω) →
    (ε : ℝ) ≤ stoppedValue f (hitting f {y : ℝ | ↑ε ≤ y} 0 n) ω := by
  intro x hx
  simp_rw [le_sup'_iff, mem_range, Nat.lt_succ_iff] at hx
  refine stoppedValue_hitting_mem ?_
  simp only [Set.mem_setOf_eq, exists_prop, hn]
  exact
    let ⟨j, hj₁, hj₂⟩ := hx
    ⟨j, hj₁, hj₂⟩

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

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

Tactic:
have h := setIntegral_ge_of_const_le (measurableSet_le measurable_const
  (Finset.measurable_range_sup'' fun n _ => (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)))
    (measure_ne_top _ _) this (Integrable.integrableOn (hsub.integrable_stoppedValue
      (hitting_isStoppingTime hsub.adapted measurableSet_Ici) hitting_le))

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