awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ω),
      (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 ℕ)) ω))
have refine : ∀ i ∈ Finset.range N,
  ∀ (hi : i ∉ Finset.range (upcrossingsBefore a b f N ω)),
    0 ≤
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N i ω) : WithTop ℕ)) ω
Tactic: refine Finset.sum_le_sum_of_subset_of_nonneg
          (Finset.range_subset_range.2 (upcrossingsBefore_le f ω hab)) fun i _ hi => ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ω)
⊢ 0 ≤
    stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ)) ω -
      stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N i ω) : WithTop ℕ)) ω
have pos : ∀ (hi' : i = upcrossingsBefore a b f N ω),
  0 ≤
    stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ)) ω -
      stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N i ω) : WithTop ℕ)) ω
Tactic: by_cases hi' : i = upcrossingsBefore a b f N ω
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ω)
pos :
  ∀ (hi' : i = upcrossingsBefore a b f N ω),
    0 ≤
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N i ω) : WithTop ℕ)) ω
⊢ 0 ≤
    stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ)) ω -
      stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N i ω) : WithTop ℕ)) ω
have neg : ∀ (hi' : ¬i = upcrossingsBefore a b f N ω),
  0 ≤
    stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ)) ω -
      stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N i ω) : WithTop ℕ)) ω
Tactic: by_cases hi' : i = upcrossingsBefore a b f N ω
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ω
⊢ 0 ≤
    stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ)) ω -
      stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N i ω) : WithTop ℕ)) ω
have pos : upcrossingsBefore a b f N ω ∈ Finset.range N →
  ∀ (hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)),
    0 ≤
      stoppedValue f (fun (ω_1 : Ω) ↦ (↑(upperCrossingTime a b f N (upcrossingsBefore a b f N ω + 1) ω_1) : WithTop ℕ))
          ω -
        stoppedValue f (fun (ω_1 : Ω) ↦ (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω_1) : WithTop ℕ)) ω
Tactic: subst hi'
Cleared hypotheses: i, h, hi, hi'
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ω)
⊢ 0 ≤
    stoppedValue f (fun (ω_1 : Ω) ↦ (↑(upperCrossingTime a b f N (upcrossingsBefore a b f N ω + 1) ω_1) : WithTop ℕ))
        ω -
      stoppedValue f (fun (ω_1 : Ω) ↦ (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω_1) : WithTop ℕ)) ω
have pos : 0 ≤
  f (WithTop.untopA (↑(upperCrossingTime a b f N (upcrossingsBefore a b f N ω + 1) ω) : WithTop ℕ)) ω -
    f (WithTop.untopA (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) : WithTop ℕ)) ω
Tactic: simp only [stoppedValue]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ω)
⊢ 0 ≤
    f (WithTop.untopA (↑(upperCrossingTime a b f N (upcrossingsBefore a b f N ω + 1) ω) : WithTop ℕ)) ω -
      f (WithTop.untopA (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) : WithTop ℕ)) ω
have pos : 0 ≤
  f (WithTop.untopA (↑N : WithTop ℕ)) ω -
    f (WithTop.untopA (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) : WithTop ℕ)) ω
Tactic: rw [upperCrossingTime_eq_of_upcrossingsBefore_lt hab (Nat.lt_succ_self _)]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ω)
⊢ 0 ≤
    f (WithTop.untopA (↑N : WithTop ℕ)) ω -
      f (WithTop.untopA (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) : WithTop ℕ)) ω
have 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 ℕ)) ω
Tactic: by_cases heq : lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ℕ)) ω
⊢ 0 ≤
    f (WithTop.untopA (↑N : WithTop ℕ)) ω -
      f (WithTop.untopA (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) : WithTop ℕ)) ω
have 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 ℕ)) ω
Tactic: by_cases heq : lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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
⊢ 0 ≤
    f (WithTop.untopA (↑N : WithTop ℕ)) ω -
      f (WithTop.untopA (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) : WithTop ℕ)) ω
have pos : 0 ≤ f (WithTop.untopA (↑N : WithTop ℕ)) ω - f (WithTop.untopA (↑N : WithTop ℕ)) ω
Tactic: rw [heq, sub_self]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ℕ)) ω
⊢ 0 ≤
    f (WithTop.untopA (↑N : WithTop ℕ)) ω -
      f (WithTop.untopA (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) : WithTop ℕ)) ω
have pos₁ : LE.le (α := ℝ) 0 0
Tactic: rw [heq, sub_self]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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
⊢ 0 ≤
    f (WithTop.untopA (↑N : WithTop ℕ)) ω -
      f (WithTop.untopA (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) : WithTop ℕ)) ω
have neg : f (WithTop.untopA (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) : WithTop ℕ)) ω ≤
  f (WithTop.untopA (↑N : WithTop ℕ)) ω
Tactic: rw [sub_nonneg]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ω
⊢ 0 ≤
    stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ)) ω -
      stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N i ω) : WithTop ℕ)) ω
have neg : upcrossingsBefore a b f N ω < i
Tactic: rw [sub_eq_zero_of_upcrossingsBefore_lt hab]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
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
have hi₁ : upcrossingsBefore a b f N ω ≤ i
Tactic: rw [Finset.mem_range, not_lt] at hi
Cleared hypotheses: hi, hi'
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ℕ)) ω))
have _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 ℕ)) ω))
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')
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ℕ)) ω))
⊢ 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 ℕ)) ω))
have _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 ℕ)) ω))
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')
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
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 ℕ)) ω
⊢ (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 ℕ)) ω)
have 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 ℕ)) ω))
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')
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 ℕ)) ω)
have neg : (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ ∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a)
Tactic: refine le_trans ?_ h₂