awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
h : upcrossingsBefore a b f N ω ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)
pos :
  ∀ (heq : lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N),
    0 ≤
      f (WithTop.untopA (↑N : WithTop ℕ)) ω -
        f (WithTop.untopA (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) : WithTop ℕ)) ω
neg :
  ∀ (heq : ¬lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N),
    0 ≤
      f (WithTop.untopA (↑N : WithTop ℕ)) ω -
        f (WithTop.untopA (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) : WithTop ℕ)) ω
⊢ 0 ≤
    f (WithTop.untopA (↑N : WithTop ℕ)) ω -
      f (WithTop.untopA (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) : WithTop ℕ)) ω

Tactic:
by_cases heq : lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N

Premises used: MeasureTheory.lowerCrossingTime, MeasureTheory.upcrossingsBefore
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
h : upcrossingsBefore a b f N ω ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)
heq : lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
pos : 0 ≤ f (WithTop.untopA (↑N : WithTop ℕ)) ω - f (WithTop.untopA (↑N : WithTop ℕ)) ω
pos₁ pos₂ : LE.le (α := ℝ) 0 0
⊢ 0 ≤
    f (WithTop.untopA (↑N : WithTop ℕ)) ω -
      f (WithTop.untopA (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) : WithTop ℕ)) ω

Tactic:
rw [heq, sub_self]

Premises used: sub_self
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
h : upcrossingsBefore a b f N ω ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)
heq : ¬lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
neg :
  f (WithTop.untopA (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) : WithTop ℕ)) ω ≤
    f (WithTop.untopA (↑N : WithTop ℕ)) ω
⊢ 0 ≤
    f (WithTop.untopA (↑N : WithTop ℕ)) ω -
      f (WithTop.untopA (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) : WithTop ℕ)) ω

Tactic:
rw [sub_nonneg]

Premises used: sub_nonneg
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
h : upcrossingsBefore a b f N ω ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)
heq : ¬lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
⊢ f (WithTop.untopA (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) : WithTop ℕ)) ω ≤
    f (WithTop.untopA (↑N : WithTop ℕ)) ω

Tactic:
le_trans (stoppedValue_lowerCrossingTime heq) hf

Premises used: MeasureTheory.stoppedValue_lowerCrossingTime, le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
h : upcrossingsBefore a b f N ω ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)
heq : ¬lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
⊢ f (WithTop.untopA (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) : WithTop ℕ)) ω ≤
    f (WithTop.untopA (↑N : WithTop ℕ)) ω

Tactic:
exact le_trans (stoppedValue_lowerCrossingTime heq) hf

Premises used: MeasureTheory.stoppedValue_lowerCrossingTime, le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
i : ℕ
h : i ∈ Finset.range N
hi : i ∉ Finset.range (upcrossingsBefore a b f N ω)
hi' : ¬i = upcrossingsBefore a b f N ω
neg : upcrossingsBefore a b f N ω < i
⊢ 0 ≤
    stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ)) ω -
      stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N i ω) : WithTop ℕ)) ω

Tactic:
rw [sub_eq_zero_of_upcrossingsBefore_lt hab]

Premises used: MeasureTheory.sub_eq_zero_of_upcrossingsBefore_lt
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
i : ℕ
h : i ∈ Finset.range N
hi : i ∉ Finset.range (upcrossingsBefore a b f N ω)
hi' : ¬i = upcrossingsBefore a b f N ω
⊢ upcrossingsBefore a b f N ω ≤ i

Tactic:
rw [Finset.mem_range, not_lt] at hi

Premises used: Finset.mem_range, not_lt
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
i : ℕ
h : i ∈ Finset.range N
hi : i ∉ Finset.range (upcrossingsBefore a b f N ω)
hi' : ¬i = upcrossingsBefore a b f N ω
hi₁ : upcrossingsBefore a b f N ω ≤ i
⊢ ¬i = upcrossingsBefore a b f N ω

Tactic:
rw [Finset.mem_range, not_lt] at hi

Premises used: Finset.mem_range, not_lt
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
i : ℕ
h : i ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ≤ i
hi' : ¬i = upcrossingsBefore a b f N ω
⊢ upcrossingsBefore a b f N ω < i

Tactic:
lt_of_le_of_ne hi (Ne.symm hi')

Premises used: Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
i : ℕ
h : i ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ≤ i
hi' : ¬i = upcrossingsBefore a b f N ω
⊢ upcrossingsBefore a b f N ω < i

Tactic:
exact lt_of_le_of_ne hi (Ne.symm hi')

Premises used: Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
_k :
  LE.le (α := ℝ) (∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a))
    (∑ k ∈ Finset.range (upcrossingsBefore a b f N ω),
      (stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω))
_k₁ :
  LE.le (α := ℝ)
    (∑ k ∈ Finset.range (upcrossingsBefore a b f N ω),
      (stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω))
    (∑ k ∈ Finset.range N,
      (stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω))
⊢ LE.le (α := ℝ) (∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a))
    (∑ k ∈ Finset.range N,
      (stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω))

Tactic:
calc
      ∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a) ≤
          ∑ k ∈ Finset.range (upcrossingsBefore a b f N ω),
            (stoppedValue f (fun ω ↦ (upperCrossingTime a b f N (k + 1) ω : ℕ)) ω -
              stoppedValue f (fun ω ↦ (lowerCrossingTime a b f N k ω : ℕ)) ω) := by
        gcongr ∑ k ∈ _, ?_ with i hi
        refine le_sub_of_le_upcrossingsBefore (zero_lt_iff.2 hN) hab ?_
        rwa [Finset.mem_range] at hi
      _ ≤ ∑ k ∈ Finset.range N,
          (stoppedValue f (fun ω ↦ (upperCrossingTime a b f N (k + 1) ω : ℕ)) ω -
          stoppedValue f (fun ω ↦ (lowerCrossingTime a b f N k ω : ℕ)) ω) := by
        refine Finset.sum_le_sum_of_subset_of_nonneg
          (Finset.range_subset_range.2 (upcrossingsBefore_le f ω hab)) fun i _ hi => ?_
        by_cases hi' : i = upcrossingsBefore a b f N ω
        · subst hi'
          simp only [stoppedValue]
          rw [upperCrossingTime_eq_of_upcrossingsBefore_lt hab (Nat.lt_succ_self _)]
          by_cases heq : lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
          · rw [heq, sub_self]
          · rw [sub_nonneg]
            exact le_trans (stoppedValue_lowerCrossingTime heq) hf
        · rw [sub_eq_zero_of_upcrossingsBefore_lt hab]
          rw [Finset.mem_range, not_lt] at hi
          exact lt_of_le_of_ne hi (Ne.symm hi')

Premises used: HSub.hSub, Finset.range, MeasureTheory.upcrossingsBefore
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
⊢ LE.le (α := ℝ) (∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a))
    (∑ k ∈ Finset.range N,
      (stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω))

Tactic:
have h₂ : ∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a) ≤
      ∑ k ∈ Finset.range N, (stoppedValue f (fun ω ↦ (upperCrossingTime a b f N (k + 1) ω : ℕ)) ω -
        stoppedValue f (fun ω ↦ (lowerCrossingTime a b f N k ω : ℕ)) ω) := by
    calc
      ∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a) ≤
          ∑ k ∈ Finset.range (upcrossingsBefore a b f N ω),
            (stoppedValue f (fun ω ↦ (upperCrossingTime a b f N (k + 1) ω : ℕ)) ω -
              stoppedValue f (fun ω ↦ (lowerCrossingTime a b f N k ω : ℕ)) ω) := by
        gcongr ∑ k ∈ _, ?_ with i hi
        refine le_sub_of_le_upcrossingsBefore (zero_lt_iff.2 hN) hab ?_
        rwa [Finset.mem_range] at hi
      _ ≤ ∑ k ∈ Finset.range N,
          (stoppedValue f (fun ω ↦ (upperCrossingTime a b f N (k + 1) ω : ℕ)) ω -
          stoppedValue f (fun ω ↦ (lowerCrossingTime a b f N k ω : ℕ)) ω) := by
        refine Finset.sum_le_sum_of_subset_of_nonneg
          (Finset.range_subset_range.2 (upcrossingsBefore_le f ω hab)) fun i _ hi => ?_
        by_cases hi' : i = upcrossingsBefore a b f N ω
        · subst hi'
          simp only [stoppedValue]
          rw [upperCrossingTime_eq_of_upcrossingsBefore_lt hab (Nat.lt_succ_self _)]
          by_cases heq : lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
          · rw [heq, sub_self]
          · rw [sub_nonneg]
            exact le_trans (stoppedValue_lowerCrossingTime heq) hf
        · rw [sub_eq_zero_of_upcrossingsBefore_lt hab]
          rw [Finset.mem_range, not_lt] at hi
          exact lt_of_le_of_ne hi (Ne.symm hi')
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
h₂ :
  LE.le (α := ℝ) (∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a))
    (∑ k ∈ Finset.range N,
      (stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω))
⊢ (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
    ∑ x ∈ Finset.range N,
      (stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (x + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N x ω) : WithTop ℕ)) ω)

Tactic:
le_trans ?_ h₂

Premises used: le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
h₂ :
  LE.le (α := ℝ) (∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a))
    (∑ k ∈ Finset.range N,
      (stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω))
neg : (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ ∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a)
⊢ (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
    ∑ x ∈ Finset.range N,
      (stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (x + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N x ω) : WithTop ℕ)) ω)

Tactic:
refine le_trans ?_ h₂

Premises used: le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
h₂ :
  LE.le (α := ℝ) (∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a))
    (∑ k ∈ Finset.range N,
      (stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω))
neg : (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ (Finset.range (upcrossingsBefore a b f N ω)).card • (b - a)
neg₁ : (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ upcrossingsBefore a b f N ω • (b - a)
neg₂ : (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ (↑(upcrossingsBefore a b f N ω) : ℝ) * (b - a)
neg₃ neg₄ : (↑(upcrossingsBefore a b f N ω) : ℝ) * (b - a) ≤ (↑(upcrossingsBefore a b f N ω) : ℝ) * (b - a)
⊢ (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ ∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a)

Tactic:
rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_comm]

Premises used: Finset.card_range, mul_comm, nsmul_eq_mul, Finset.sum_const
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
rw :
  LE.le (α := ℝ) (∫ (a_1 : Ω), (b - a) * (↑(upcrossingsBefore a b f N a_1) : ℝ) ∂μ)
    (∫ (x : Ω), (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ)
⊢ (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ ≤
    ∫ (x : Ω), (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ

Tactic:
rw [← integral_const_mul]

Premises used: MeasureTheory.integral_const_mul
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
⊢ LE.le (α := ℝ) (∫ (a_1 : Ω), (b - a) * (↑(upcrossingsBefore a b f N a_1) : ℝ) ∂μ)
    (∫ (x : Ω), (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ)

Tactic:
integral_mono_of_nonneg ?_ ((hf.sum_upcrossingStrat_mul a b N).integrable N) ?_

Premises used: MeasureTheory.Submartingale.sum_upcrossingStrat_mul, MeasureTheory.Submartingale.integrable, MeasureTheory.integral_mono_of_nonneg
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
refine_1 : (ae μ).EventuallyLE (β := ℝ) 0 fun (a_1 : Ω) ↦ (b - a) * (↑(upcrossingsBefore a b f N a_1) : ℝ)
refine_2 :
  (ae μ).EventuallyLE (β := ℝ) (fun (a_1 : Ω) ↦ (b - a) * (↑(upcrossingsBefore a b f N a_1) : ℝ))
    (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k))
⊢ LE.le (α := ℝ) (∫ (a_1 : Ω), (b - a) * (↑(upcrossingsBefore a b f N a_1) : ℝ) ∂μ)
    (∫ (x : Ω), (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ)

Tactic:
refine integral_mono_of_nonneg ?_ ((hf.sum_upcrossingStrat_mul a b N).integrable N) ?_

Premises used: MeasureTheory.Submartingale.sum_upcrossingStrat_mul, MeasureTheory.Submartingale.integrable, MeasureTheory.integral_mono_of_nonneg
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (a_1 : Ω) ↦ (b - a) * (↑(upcrossingsBefore a b f N a_1) : ℝ)

Tactic:
Eventually.of_forall fun ω => mul_nonneg (sub_nonneg.2 hab.le) (Nat.cast_nonneg _)

Premises used: Iff.mpr, mul_nonneg, Nat.cast_nonneg, LT.lt.le, Filter.Eventually.of_forall, Filter.EventuallyLE, sub_nonneg, MeasureTheory.upcrossingsBefore
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (a_1 : Ω) ↦ (b - a) * (↑(upcrossingsBefore a b f N a_1) : ℝ)

Tactic:
exact Eventually.of_forall fun ω => mul_nonneg (sub_nonneg.2 hab.le) (Nat.cast_nonneg _)

Premises used: Iff.mpr, mul_nonneg, Nat.cast_nonneg, LT.lt.le, Filter.Eventually.of_forall, sub_nonneg
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
refine_2 :
  ∀ (ω : Ω),
    (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
      (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)) ω
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (a_1 : Ω) ↦ (b - a) * (↑(upcrossingsBefore a b f N a_1) : ℝ))
    (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k))

Tactic:
filter_upwards with ω
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
ω : Ω
⊢ (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
    (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)) ω

Tactic:
simpa using mul_upcrossingsBefore_le (hfN ω) hab

Premises used: MeasureTheory.mul_upcrossingsBefore_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
⊢ 0 < b - a

Tactic:
have hab' : 0 < b - a := sub_pos.2 hab
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
⊢ b - a ≤ (f ω i - a)⁺ ↔ b ≤ f ω i

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
refine_1 : ∀ (h : b - a ≤ (f ω i - a)⁺), b ≤ f ω i
refine_2 : ∀ (h : b ≤ f ω i), b - a ≤ (f ω i - a)⁺
⊢ b - a ≤ (f ω i - a)⁺ ↔ b ≤ f ω i

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩