-- 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:
case h.e'_3.h.e'_1.h.e'_6.h.e'_4.h
Ω : 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 ∂μ)
ω : Ω
⊢ ω ∈ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} ∪ {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε} ↔
    ω ∈ Set.univ

Tactic:
change (ε : ℝ) ≤ _ ∨ _ < (ε : ℝ) ↔ _

Result:
case h.e'_3.h.e'_1.h.e'_6.h.e'_4.h
Ω : 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 ∂μ)
ω : Ω
⊢ (↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω) ∨ ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε ↔ ω ∈ Set.univ

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 ω) < ↑ε
this : hitting f {y | ↑ε ≤ y} 0 n ω = n
⊢ f n ω ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω

Tactic:
simp_rw [stoppedValue, this, le_rfl]

Result:
no goals

Proof state:
Ω : 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 (∫ (x : Ω) in Set.univ, stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) x ∂μ)

Tactic:
convert rfl

Result:
case h.e'_3.h.e'_1.h.e'_6.h.e'_4
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ Set.univ = {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} ∪ {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}

Proof state:
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 ω) < ↑ε}

Tactic:
rw [disjoint_iff_inf_le]

Result:
case hst
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} ⊓ {ω | ((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 : ℕ
ω : Ω
hω : ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε
m : ℕ
hm : m ∈ Set.Icc 0 n
hεm : ↑ε ≤ f m ω
⊢ sInf (Set.Icc 0 n ∩ {i | ↑ε ≤ f i ω}) = n

Tactic:
exact False.elim
  ((not_le.2 hω) ((le_sup'_iff _).2 ⟨m, mem_range.2 (Nat.lt_succ_of_le hm.2), hεm⟩))

Result:
no goals

Proof state:
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 ω} μ

Tactic:
exact Integrable.integrableOn (hsub.integrable_stoppedValue
  (hitting_isStoppingTime hsub.adapted measurableSet_Ici) hitting_le)

Result:
no goals

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:
exact (not_le.2 hω₂) hω₁

Result:
no goals

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 ω) < ↑ε
⊢ ∀ x ∈ Set.Icc 0 n, ↑ε ≤ f x ω → sInf (Set.Icc 0 n ∩ {i | ↑ε ≤ f i ω}) = n

Tactic:
intro m hm hεm

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 ω) < ↑ε
m : ℕ
hm : m ∈ Set.Icc 0 n
hεm : ↑ε ≤ f m ω
⊢ sInf (Set.Icc 0 n ∩ {i | ↑ε ≤ f i ω}) = n

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

Tactic:
refine add_le_add (smul_le_stoppedValue_hitting hsub _)
  (ENNReal.ofReal_le_ofReal (setIntegral_mono_on (hsub.integrable n).integrableOn
    (Integrable.integrableOn (hsub.integrable_stoppedValue
      (hitting_isStoppingTime hsub.adapted measurableSet_Ici) hitting_le))
        (measurableSet_lt (Finset.measurable_range_sup'' fun n _ =>
          (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)) measurable_const) ?_))

Result:
Ω : 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

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 ω) < ↑ε
⊢ hitting f {y | ↑ε ≤ y} 0 n ω = n

Tactic:
simp only [hitting, Set.mem_setOf_eq, exists_prop, Pi.natCast_def, Nat.cast_id,
ite_eq_right_iff, forall_exists_index, and_imp]

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 ω) < ↑ε
⊢ ∀ x ∈ Set.Icc 0 n, ↑ε ≤ f x ω → sInf (Set.Icc 0 n ∩ {i | ↑ε ≤ f i ω}) = 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:
exact (not_le.2 hω₂) hω₁

Result:
no goals