-- Mathlib/Probability/Martingale/Basic.lean
theorem submartingale_of_setIntegral_le_succ [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ}
    (hadp : Adapted 𝒢 f) (hint : ∀ i, Integrable (f i) μ)
    (hf : ∀ i, ∀ s : Set Ω, MeasurableSet[𝒢 i] s → ∫ ω in s, f i ω ∂μ ≤ ∫ ω in s, f (i + 1) ω ∂μ) :
    Submartingale f 𝒢 μ

Proof state:
case refl
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ
i j : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ

Tactic:
exact le_rfl

Result:
no goals

Proof state:
case step
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ
i j : ℕ
s : Set Ω
hs : MeasurableSet s
k : ℕ
hk₁ : i.le k
hk₂ : ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f k ω ∂μ
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f k.succ ω ∂μ

Tactic:
exact le_trans hk₂ (hf k s (𝒢.mono hk₁ _ hs))

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ
⊢ Submartingale f 𝒢 μ

Tactic:
refine submartingale_of_setIntegral_le hadp hint fun i j hij s hs => ?_

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ

Tactic:
induction' hij with k hk₁ hk₂

Result:
case refl
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ
i j : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ

case step
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ
i j : ℕ
s : Set Ω
hs : MeasurableSet s
k : ℕ
hk₁ : i.le k
hk₂ : ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f k ω ∂μ
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f k.succ ω ∂μ