awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
this : ∀ (i : ℕ), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}
i : ℕ
h : i ∈ Finset.range (N + 1)
⊢ Integrable (f i) (μ.restrict {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω})

Tactic:
exact (hf.integrable _).integrableOn

Premises used: MeasureTheory.Submartingale.integrable, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
this : ∀ (i : ℕ), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}
i : ℕ
hf₁ :
  i ∈ Finset.range (N + 1) → Integrable (Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i)) μ
⊢ i ∈ Finset.range (N + 1) → Integrable (Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i)) μ

Tactic:
_
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
this : ∀ (i : ℕ), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}
i : ℕ
h : i ∈ Finset.range (N + 1)
⊢ Integrable (Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i)) μ

Tactic:
Integrable.indicator (Integrable.sub (hf.integrable _) (hf.integrable _))
      (𝒢.le _ _ (this _))

Premises used: MeasureTheory.Submartingale.integrable, MeasureTheory.Integrable.sub, MeasureTheory.Filtration.le, MeasureTheory.Integrable.indicator
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
this : ∀ (i : ℕ), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}
i : ℕ
h : i ∈ Finset.range (N + 1)
⊢ Integrable (Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i)) μ

Tactic:
exact Integrable.indicator (Integrable.sub (hf.integrable _) (hf.integrable _))
      (𝒢.le _ _ (this _))

Premises used: MeasureTheory.Submartingale.integrable, MeasureTheory.Integrable.sub, MeasureTheory.Filtration.le, MeasureTheory.Integrable.indicator
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
⊢ Integrable (stoppedValue f π) μ

Tactic:
hf.integrable_stoppedValue hπ hbdd

Premises used: MeasureTheory.Submartingale.integrable_stoppedValue
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
⊢ Integrable (stoppedValue f π) μ

Tactic:
exact hf.integrable_stoppedValue hπ hbdd

Premises used: MeasureTheory.Submartingale.integrable_stoppedValue
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
⊢ Integrable (stoppedValue f τ) μ

Tactic:
hf.integrable_stoppedValue hτ fun ω => le_trans (hle ω) (hbdd ω)

Premises used: MeasureTheory.Submartingale.integrable_stoppedValue, le_trans
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
⊢ Integrable (stoppedValue f τ) μ

Tactic:
exact hf.integrable_stoppedValue hτ fun ω => le_trans (hle ω) (hbdd ω)

Premises used: MeasureTheory.Submartingale.integrable_stoppedValue, le_trans
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π →
          (∃ (N : ℕ), ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)) →
            LE.le (α := ℝ) (∫ (x : Ω), stoppedValue f τ x ∂μ) (∫ (x : Ω), stoppedValue f π x ∂μ)
⊢ Submartingale f 𝒢 μ

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

Premises used: MeasureTheory.submartingale_of_setIntegral_le
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π →
          (∃ (N : ℕ), ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)) →
            LE.le (α := ℝ) (∫ (x : Ω), stoppedValue f τ x ∂μ) (∫ (x : Ω), stoppedValue f π x ∂μ)
refine :
  ∀ (i j : ℕ) (hij : i ≤ j) (s : Set Ω) (hs : MeasurableSet s),
    LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
⊢ Submartingale f 𝒢 μ

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

Premises used: MeasureTheory.submartingale_of_setIntegral_le
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π →
          (∃ (N : ℕ), ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)) →
            LE.le (α := ℝ) (∫ (x : Ω), stoppedValue f τ x ∂μ) (∫ (x : Ω), stoppedValue f π x ∂μ)
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
specialize :
  LE.le (α := Ω → ℕ∞) (s.piecewise (β := fun (a : Ω) ↦ ℕ∞) (fun (x : Ω) ↦ (↑i : ℕ∞)) fun (x : Ω) ↦ (↑j : ℕ∞))
    fun (x : Ω) ↦ (↑j : WithTop ℕ)
specialize₁ :
  ∀
    (hf :
      LE.le (α := ℝ)
        (∫ (x : Ω),
          stoppedValue f (s.piecewise (β := fun (a : Ω) ↦ ℕ∞) (fun (x : Ω) ↦ (↑i : ℕ∞)) fun (x : Ω) ↦ (↑j : ℕ∞)) x ∂μ)
        (∫ (x : Ω), stoppedValue f (fun (x : Ω) ↦ (↑j : WithTop ℕ)) x ∂μ)),
    LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
⊢ LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)

Tactic:
specialize hf (s.piecewise (fun _ => i) fun _ => j) _ (isStoppingTime_piecewise_const hij hs)
    (isStoppingTime_const 𝒢 j) ?_
    ⟨j, fun _ => le_rfl⟩

Premises used: MeasureTheory.isStoppingTime_piecewise_const, le_rfl, Nat.cast, MeasureTheory.isStoppingTime_const, Exists.intro, Set.piecewise
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π →
          (∃ (N : ℕ), ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)) →
            LE.le (α := ℝ) (∫ (x : Ω), stoppedValue f τ x ∂μ) (∫ (x : Ω), stoppedValue f π x ∂μ)
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
ω : Ω
simp : LE.le (α := ℕ∞) (if ω ∈ s then (↑i : ℕ∞) else (↑j : ℕ∞)) (↑j : WithTop ℕ)
⊢ LE.le (α := (fun (a : Ω) ↦ ℕ∞) ω)
    (s.piecewise (β := fun (a : Ω) ↦ ℕ∞) (fun (x : Ω) ↦ (↑i : ℕ∞)) (fun (x : Ω) ↦ (↑j : ℕ∞)) ω : ℕ∞)
    ((fun (x : Ω) ↦ (↑j : WithTop ℕ)) ω : WithTop ℕ)

Tactic:
simp only [Set.piecewise, ENat.some_eq_coe]

Premises used: ENat.some_eq_coe, Set.piecewise
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π →
          (∃ (N : ℕ), ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)) →
            LE.le (α := ℝ) (∫ (x : Ω), stoppedValue f τ x ∂μ) (∫ (x : Ω), stoppedValue f π x ∂μ)
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
ω : Ω
pos : ∀ (hω : ω ∈ s), LE.le (α := ℕ∞) (↑i : ℕ∞) (↑j : WithTop ℕ)
neg : ∀ (hω : ω ∉ s), LE.le (α := ℕ∞) (↑j : ℕ∞) (↑j : WithTop ℕ)
⊢ LE.le (α := ℕ∞) (if ω ∈ s then (↑i : ℕ∞) else (↑j : ℕ∞)) (↑j : WithTop ℕ)

Tactic:
split_ifs with hω
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π →
          (∃ (N : ℕ), ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)) →
            LE.le (α := ℝ) (∫ (x : Ω), stoppedValue f τ x ∂μ) (∫ (x : Ω), stoppedValue f π x ∂μ)
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
ω : Ω
hω : ω ∈ s
⊢ LE.le (α := ℕ∞) (↑i : ℕ∞) (↑j : WithTop ℕ)

Tactic:
mod_cast hij

Premises used: cast, Nat.cast_le._simp_1, ENat, Eq.symm
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π →
          (∃ (N : ℕ), ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)) →
            LE.le (α := ℝ) (∫ (x : Ω), stoppedValue f τ x ∂μ) (∫ (x : Ω), stoppedValue f π x ∂μ)
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
ω : Ω
hω : ω ∈ s
⊢ LE.le (α := ℕ∞) (↑i : ℕ∞) (↑j : WithTop ℕ)

Tactic:
exact mod_cast hij
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π →
          (∃ (N : ℕ), ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)) →
            LE.le (α := ℝ) (∫ (x : Ω), stoppedValue f τ x ∂μ) (∫ (x : Ω), stoppedValue f π x ∂μ)
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
ω : Ω
hω : ω ∉ s
neg neg₁ neg₂ neg₃ : j ≤ j
⊢ LE.le (α := ℕ∞) (↑j : ℕ∞) (↑j : WithTop ℕ)

Tactic:
norm_cast
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
hf :
  LE.le (α := ℝ)
    (∫ (x : Ω),
      stoppedValue f (s.piecewise (β := fun (a : Ω) ↦ ℕ∞) (fun (x : Ω) ↦ (↑i : ℕ∞)) fun (x : Ω) ↦ (↑j : ℕ∞)) x ∂μ)
    (∫ (x : Ω), stoppedValue f (fun (x : Ω) ↦ (↑j : WithTop ℕ)) x ∂μ)
rwa :
  ∀
    (hf :
      LE.le (α := ℝ)
        (∫ (x : Ω),
          stoppedValue f (s.piecewise (β := fun (a : Ω) ↦ ℕ∞) (fun (x : Ω) ↦ (↑i : ℕ∞)) fun (x : Ω) ↦ (↑j : ℕ∞)) x ∂μ)
        (∫ (x : Ω), f j x ∂μ)),
    LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
rwa₁ :
  ∀
    (hf :
      LE.le (α := ℝ)
        (∫ (x : Ω),
          stoppedValue f
            (s.piecewise (β := fun (a : Ω) ↦ ℕ∞) (fun (x : Ω) ↦ (↑i : WithTop ℕ)) fun (x : Ω) ↦ (↑j : WithTop ℕ)) x ∂μ)
        (∫ (x : Ω), f j x ∂μ)),
    LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
rwa₂ :
  ∀ (hf : LE.le (α := ℝ) (∫ (x : Ω), s.piecewise (β := fun (i : Ω) ↦ ℝ) (f i) (f j) x ∂μ) (∫ (x : Ω), f j x ∂μ)),
    LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
rwa₃ :
  ∀ (hf : HAdd.hAdd (α := ℝ) (∫ (x : Ω) in s, f i x ∂μ) (∫ (x : Ω) in sᶜ, f j x ∂μ) ≤ ∫ (x : Ω), f j x ∂μ),
    LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
rwa₄ :
  ∀
    (hf :
      HAdd.hAdd (α := ℝ) (∫ (x : Ω) in s, f i x ∂μ) (∫ (x : Ω) in sᶜ, f j x ∂μ) ≤
        HAdd.hAdd (α := ℝ) (∫ (x : Ω) in s, f j x ∂μ) (∫ (x : Ω) in sᶜ, f j x ∂μ)),
    LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
rwa₅ rwa₆ rwa₇ rwa₈ :
  ∀ (hf : LE.le (α := ℝ) (∫ (x : Ω) in s, f i x ∂μ) (∫ (x : Ω) in s, f j x ∂μ)),
    LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
⊢ LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)

Tactic:
rwa [stoppedValue_const, ← ENat.some_eq_coe, stoppedValue_piecewise_const,
      integral_piecewise (𝒢.le _ _ hs) (hint _).integrableOn (hint _).integrableOn, ←
      integral_add_compl (𝒢.le _ _ hs) (hint j), add_le_add_iff_right] at hf

Premises used: ENat.some_eq_coe, MeasureTheory.stoppedValue_const, MeasureTheory.stoppedValue_piecewise_const, MeasureTheory.integral_add_compl, add_le_add_iff_right, MeasureTheory.Filtration.le, MeasureTheory.Integrable.integrableOn, MeasureTheory.integral_piecewise
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π →
          (∃ (N : ℕ), ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)) →
            LE.le (α := ℝ) (∫ (x : Ω), stoppedValue f τ x ∂μ) (∫ (x : Ω), stoppedValue f π x ∂μ)
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
specialize :
  LE.le (α := Ω → ℕ∞) (s.piecewise (β := fun (a : Ω) ↦ ℕ∞) (fun (x : Ω) ↦ (↑i : ℕ∞)) fun (x : Ω) ↦ (↑j : ℕ∞))
    fun (x : Ω) ↦ (↑j : WithTop ℕ)
specialize₁ specialize₂ :
  ∀
    (hf :
      LE.le (α := ℝ)
        (∫ (x : Ω),
          stoppedValue f (s.piecewise (β := fun (a : Ω) ↦ ℕ∞) (fun (x : Ω) ↦ (↑i : ℕ∞)) fun (x : Ω) ↦ (↑j : ℕ∞)) x ∂μ)
        (∫ (x : Ω), stoppedValue f (fun (x : Ω) ↦ (↑j : WithTop ℕ)) x ∂μ)),
    LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
⊢ LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)

Tactic:
classical
  specialize hf (s.piecewise (fun _ => i) fun _ => j) _ (isStoppingTime_piecewise_const hij hs)
    (isStoppingTime_const 𝒢 j) ?_
    ⟨j, fun _ => le_rfl⟩
  · intro ω
    simp only [Set.piecewise, ENat.some_eq_coe]
    split_ifs with hω
    · exact mod_cast hij
    · norm_cast
  · rwa [stoppedValue_const, ← ENat.some_eq_coe, stoppedValue_piecewise_const,
      integral_piecewise (𝒢.le _ _ hs) (hint _).integrableOn (hint _).integrableOn, ←
      integral_add_compl (𝒢.le _ _ hs) (hint j), add_le_add_iff_right] at hf

Premises used: ENat.some_eq_coe, MeasureTheory.stoppedValue_const, MeasureTheory.stoppedValue_piecewise_const, MeasureTheory.integral_add_compl, add_le_add_iff_right, MeasureTheory.Filtration.le, Set.piecewise
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
⊢ Submartingale f 𝒢 μ ↔
    ∀ (τ π : Ω → ℕ∞),
      IsStoppingTime 𝒢 τ →
        IsStoppingTime 𝒢 π →
          τ ≤ π →
            (∃ (N : ℕ), ∀ (x : Ω), π x ≤ (↑N : ℕ∞)) →
              LE.le (α := ℝ) (∫ (x : Ω), stoppedValue f τ x ∂μ) (∫ (x : Ω), stoppedValue f π x ∂μ)

Tactic:
⟨fun hf _ _ hτ hπ hle ⟨_, hN⟩ => hf.expected_stoppedValue_mono hτ hπ hle hN,
    submartingale_of_expected_stoppedValue_mono hadp hint⟩

Premises used: MeasureTheory.stoppedValue, MeasureTheory.Submartingale.expected_stoppedValue_mono, LE.le, _private.0.MeasureTheory.submartingale_iff_expected_stoppedValue_mono.match_1, MeasureTheory.submartingale_of_expected_stoppedValue_mono, MeasureTheory.integral, Iff.intro
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
rw :
  ∀ (τ_1 π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ_1 →
      IsStoppingTime 𝒢 π →
        τ_1 ≤ π →
          (∃ (N : ℕ), ∀ (x : Ω), π x ≤ (↑N : ℕ∞)) →
            LE.le (α := ℝ) (∫ (x : Ω), stoppedValue (stoppedProcess f τ) τ_1 x ∂μ)
              (∫ (x : Ω), stoppedValue (stoppedProcess f τ) π x ∂μ)
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 (stoppedProcess f τ)
hint : ∀ (i : ℕ), Integrable (stoppedProcess f τ i) μ
⊢ Submartingale (stoppedProcess f τ) 𝒢 μ

Tactic:
rw [submartingale_iff_expected_stoppedValue_mono]

Premises used: MeasureTheory.submartingale_iff_expected_stoppedValue_mono
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
σ π : Ω → ℕ∞
hσ : IsStoppingTime 𝒢 σ
hπ : IsStoppingTime 𝒢 π
hσ_le_π : σ ≤ π
hπ_bdd : ∃ (N : ℕ), ∀ (x : Ω), π x ≤ (↑N : ℕ∞)
simp_rw :
  LE.le (α := ℝ)
    (∫ (x : Ω),
      if σ x ≠ ⊤ then stoppedValue f (fun (ω : Ω) ↦ min (σ ω) (τ ω)) x
      else stoppedValue f (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ℕ) : WithTop ℕ) (τ ω)) x ∂μ)
    (∫ (x : Ω),
      if π x ≠ ⊤ then stoppedValue f (fun (ω : Ω) ↦ min (π ω) (τ ω)) x
      else stoppedValue f (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ℕ) : WithTop ℕ) (τ ω)) x ∂μ)
⊢ LE.le (α := ℝ) (∫ (x : Ω), stoppedValue (stoppedProcess f τ) σ x ∂μ)
    (∫ (x : Ω), stoppedValue (stoppedProcess f τ) π x ∂μ)

Tactic:
simp_rw [stoppedValue_stoppedProcess]

Premises used: MeasureTheory.stoppedValue_stoppedProcess
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
σ π : Ω → ℕ∞
hσ : IsStoppingTime 𝒢 σ
hπ : IsStoppingTime 𝒢 π
hσ_le_π : σ ≤ π
hπ_bdd : ∃ (N : ℕ), ∀ (x : Ω), π x ≤ (↑N : ℕ∞)
obtain :
  ∀ (n : ℕ) (hπ_le_n : ∀ (x : Ω), π x ≤ (↑n : ℕ∞)),
    LE.le (α := ℝ)
      (∫ (x : Ω),
        if σ x ≠ ⊤ then stoppedValue f (fun (ω : Ω) ↦ min (σ ω) (τ ω)) x
        else stoppedValue f (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ℕ) : WithTop ℕ) (τ ω)) x ∂μ)
      (∫ (x : Ω),
        if π x ≠ ⊤ then stoppedValue f (fun (ω : Ω) ↦ min (π ω) (τ ω)) x
        else stoppedValue f (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ℕ) : WithTop ℕ) (τ ω)) x ∂μ)
⊢ LE.le (α := ℝ)
    (∫ (x : Ω),
      if σ x ≠ ⊤ then stoppedValue f (fun (ω : Ω) ↦ min (σ ω) (τ ω)) x
      else stoppedValue f (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ℕ) : WithTop ℕ) (τ ω)) x ∂μ)
    (∫ (x : Ω),
      if π x ≠ ⊤ then stoppedValue f (fun (ω : Ω) ↦ min (π ω) (τ ω)) x
      else stoppedValue f (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ℕ) : WithTop ℕ) (τ ω)) x ∂μ)

Tactic:
obtain ⟨n, hπ_le_n⟩ := hπ_bdd
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
σ π : Ω → ℕ∞
hσ : IsStoppingTime 𝒢 σ
hπ : IsStoppingTime 𝒢 π
hσ_le_π : σ ≤ π
n : ℕ
hπ_le_n : ∀ (x : Ω), π x ≤ (↑n : ℕ∞)
ω : Ω
⊢ Ne (α := ℕ∞) (↑n : ℕ∞) ⊤

Tactic:
simp
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
σ π : Ω → ℕ∞
hσ : IsStoppingTime 𝒢 σ
hπ : IsStoppingTime 𝒢 π
hσ_le_π : σ ≤ π
n : ℕ
hπ_le_n : ∀ (x : Ω), π x ≤ (↑n : ℕ∞)
⊢ ∀ (ω : Ω), π ω ≠ ⊤

Tactic:
have hπ_top ω : π ω ≠ ⊤ := ne_top_of_le_ne_top (by simp) (hπ_le_n ω)
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
σ π : Ω → ℕ∞
hσ : IsStoppingTime 𝒢 σ
hπ : IsStoppingTime 𝒢 π
hσ_le_π : σ ≤ π
n : ℕ
hπ_le_n : ∀ (x : Ω), π x ≤ (↑n : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
⊢ ∀ (ω : Ω), σ ω ≠ ⊤

Tactic:
have hσ_top ω : σ ω ≠ ⊤ := ne_top_of_le_ne_top (hπ_top ω) (hσ_le_π ω)
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
σ π : Ω → ℕ∞
hσ : IsStoppingTime 𝒢 σ
hπ : IsStoppingTime 𝒢 π
hσ_le_π : σ ≤ π
n : ℕ
hπ_le_n : ∀ (x : Ω), π x ≤ (↑n : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hσ_top : ∀ (ω : Ω), σ ω ≠ ⊤
simp :
  LE.le (α := ℝ) (∫ (x : Ω), stoppedValue f (fun (ω : Ω) ↦ min (σ ω) (τ ω)) x ∂μ)
    (∫ (x : Ω), stoppedValue f (fun (ω : Ω) ↦ min (π ω) (τ ω)) x ∂μ)
⊢ LE.le (α := ℝ)
    (∫ (x : Ω),
      if σ x ≠ ⊤ then stoppedValue f (fun (ω : Ω) ↦ min (σ ω) (τ ω)) x
      else stoppedValue f (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ℕ) : WithTop ℕ) (τ ω)) x ∂μ)
    (∫ (x : Ω),
      if π x ≠ ⊤ then stoppedValue f (fun (ω : Ω) ↦ min (π ω) (τ ω)) x
      else stoppedValue f (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ℕ) : WithTop ℕ) (τ ω)) x ∂μ)

Tactic:
simp only [ne_eq, hσ_top, not_false_eq_true, ↓reduceIte, hπ_top, ge_iff_le]

Premises used: ge_iff_le, ne_eq, reduceIte, not_false_eq_true