-- Mathlib/Probability/Martingale/OptionalStopping.lean
theorem Submartingale.expected_stoppedValue_mono [SigmaFiniteFiltration μ 𝒢]
    (hf : Submartingale f 𝒢 μ) (hτ : IsStoppingTime 𝒢 τ) (hπ : IsStoppingTime 𝒢 π) (hle : τ ≤ π)
    {N : ℕ} (hbdd : ∀ ω, π ω ≤ N) : μ[stoppedValue f τ] ≤ μ[stoppedValue f π]

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ i ∧ i < π ω}
⊢ 0 ≤ ∫ (a : Ω), ∑ c ∈ Finset.range (N + 1), {ω | τ ω ≤ c ∧ c < π ω}.indicator (f (c + 1) - f c) a ∂μ

Tactic:
rw [integral_finset_sum]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ i ∧ i < π ω}
⊢ 0 ≤ ∑ i ∈ Finset.range (N + 1), ∫ (a : Ω), {ω | τ ω ≤ i ∧ i < π ω}.indicator (f (i + 1) - f i) a ∂μ

case hf
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ i ∧ i < π ω}
⊢ ∀ i ∈ Finset.range (N + 1), Integrable ({ω | τ ω ≤ i ∧ i < π ω}.indicator (f (i + 1) - f i)) μ

Proof state:
case h.e'_3
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
i : ℕ
⊢ (fun ω => i.succ.le (π ω)) = {ω | π ω ≤ i}ᶜ

Tactic:
ext x

Result:
case h.e'_3.h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
i : ℕ
x : Ω
⊢ (x ∈ fun ω => i.succ.le (π ω)) ↔ x ∈ {ω | π ω ≤ i}ᶜ

Proof state:
case hf
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ i ∧ i < π ω}
⊢ ∀ i ∈ Finset.range (N + 1), Integrable ({ω | τ ω ≤ i ∧ i < π ω}.indicator (f (i + 1) - f i)) μ

Tactic:
intro i _

Result:
case hf
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ i ∧ i < π ω}
i : ℕ
a✝ : i ∈ Finset.range (N + 1)
⊢ Integrable ({ω | τ ω ≤ i ∧ i < π ω}.indicator (f (i + 1) - f i)) μ

Proof state:
case hf
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
⊢ Integrable (stoppedValue f π) μ

Tactic:
exact hf.integrable_stoppedValue hπ hbdd

Result:
no goals

Proof state:
case h.e'_3.h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
i : ℕ
x : Ω
⊢ (x ∈ fun ω => i.succ.le (π ω)) ↔ x ∈ {ω | π ω ≤ i}ᶜ

Tactic:
simp

Result:
case h.e'_3.h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
i : ℕ
x : Ω
⊢ (x ∈ fun ω => i + 1 ≤ π ω) ↔ i < π x

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ i ∧ i < π ω}
⊢ 0 ≤ ∑ i ∈ Finset.range (N + 1), ∫ (a : Ω), {ω | τ ω ≤ i ∧ i < π ω}.indicator (f (i + 1) - f i) a ∂μ

Tactic:
refine Finset.sum_nonneg fun i _ => ?_

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ i ∧ i < π ω}
i : ℕ
x✝ : i ∈ Finset.range (N + 1)
⊢ 0 ≤ ∫ (a : Ω), {ω | τ ω ≤ i ∧ i < π ω}.indicator (f (i + 1) - f i) a ∂μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
⊢ ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ

Tactic:
rw [← sub_nonneg, ← integral_sub', stoppedValue_sub_eq_sum' hle hbdd]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
⊢ 0 ≤ ∫ (a : Ω), (fun ω => (∑ i ∈ Finset.range (N + 1), {ω | τ ω ≤ i ∧ i < π ω}.indicator (f (i + 1) - f i)) ω) a ∂μ

case hf
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
⊢ Integrable (stoppedValue f π) μ

case hg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
⊢ Integrable (stoppedValue f τ) μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
⊢ 0 ≤ ∫ (a : Ω), ∑ c ∈ Finset.range (N + 1), {ω | τ ω ≤ c ∧ c < π ω}.indicator (f (c + 1) - f c) a ∂μ

Tactic:
have : ∀ i, MeasurableSet[𝒢 i] {ω : Ω | τ ω ≤ i ∧ i < π ω} := by
  intro i
  refine (hτ i).inter ?_
  convert (hπ i).compl using 1
  ext x
  simp; rfl

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ i ∧ i < π ω}
⊢ 0 ≤ ∫ (a : Ω), ∑ c ∈ Finset.range (N + 1), {ω | τ ω ≤ c ∧ c < π ω}.indicator (f (c + 1) - f c) a ∂μ