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 n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : ∃ j ∈ Set.Ico (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ ∃ j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b
have obtain : ∀ (j : ℕ) (hj₁ : j ∈ Set.Ico (lowerCrossingTime a b f N n ω) N) (hj₂ : f j ω ∈ Set.Ici b),
  ∃ j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b
Tactic: obtain ⟨j, hj₁, hj₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N n ω < N
⊢ upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω
have zero : ∀ (h : upperCrossingTime a b f N 0 ω < N), upperCrossingTime a b f M 0 ω = upperCrossingTime a b f N 0 ω
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N n ω < N
zero : ∀ (h : upperCrossingTime a b f N 0 ω < N), upperCrossingTime a b f M 0 ω = upperCrossingTime a b f N 0 ω
⊢ upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω
have succ : ∀ (n : ℕ) (h : upperCrossingTime a b f N (n + 1) ω < N),
  upperCrossingTime a b f M (n + 1) ω = upperCrossingTime a b f N (n + 1) ω
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
⊢ LE.le (α := ℕ) (sSup {n : ℕ | upperCrossingTime a b f N n ω < N}) (sSup {n : ℕ | upperCrossingTime a b f M n ω < M})
have h₁ : BddAbove (α := ℕ) {n : ℕ | upperCrossingTime a b f M n ω < M}
Tactic: gcongr sSup {n | ?_} with n
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
h₁ : BddAbove (α := ℕ) {n : ℕ | upperCrossingTime a b f M n ω < M}
⊢ LE.le (α := ℕ) (sSup {n : ℕ | upperCrossingTime a b f N n ω < N}) (sSup {n : ℕ | upperCrossingTime a b f M n ω < M})
have h₂ : ∀ (n : ℕ), upperCrossingTime a b f N n ω < N → upperCrossingTime a b f M n ω < M
Tactic: gcongr sSup {n | ?_} with n
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
n : ℕ
hn : upperCrossingTime a b f N n ω < N
⊢ upperCrossingTime a b f M n ω < M
have h₂ : upperCrossingTime a b f N n ω < M
Tactic: rw [upperCrossingTime_eq_upperCrossingTime_of_lt hNM hn]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
⊢ upcrossingsBefore a b f N ω < upcrossingsBefore a b f (N₂ + 1) ω
have refine : Membership.mem (γ := Set ℕ) {n : ℕ | upperCrossingTime a b f (N₂ + 1) n ω < N₂ + 1} (upcrossingsBefore a b f N ω).succ
Tactic: refine lt_of_lt_of_le (Nat.lt_succ_self _) (le_csSup (upperCrossingTime_lt_bddAbove hab) ?_)
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | upperCrossingTime a b f (N₂ + 1) n ω < N₂ + 1} (upcrossingsBefore a b f N ω).succ
have rw : ∃ j ∈ Set.Ico (lowerCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω) (N₂ + 1), f j ω ∈ Set.Ici b
Tactic: rw [Set.mem_setOf_eq, upperCrossingTime_succ_eq, hittingBtwn_lt_iff _ le_rfl]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
⊢ ∃ j ∈ Set.Ico (lowerCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω) (N₂ + 1), f j ω ∈ Set.Ici b
have refine : lowerCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N₂
Tactic: refine ⟨N₂, ⟨?_, Nat.lt_succ_self _⟩, hN₂'.le⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
⊢ lowerCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N₂
have rw : ∃ j ∈ Set.Icc (upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω) N₂, f j ω ∈ Set.Iic a
Tactic: rw [lowerCrossingTime, hittingBtwn_le_iff_of_lt _ (Nat.lt_succ_self _)]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
⊢ ∃ j ∈ Set.Icc (upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω) N₂, f j ω ∈ Set.Iic a
have refine : upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
Tactic: refine ⟨N₁, ⟨le_trans ?_ hN₁, hN₂⟩, hN₁'.le⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
have pos : ∀ (hN : 0 < N), upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
Tactic: by_cases! hN : 0 < N
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
pos : ∀ (hN : 0 < N), upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
have neg : ∀ (hN : N ≤ 0), upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
Tactic: by_cases! hN : 0 < N
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : 0 < N
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
have this : upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω < N
Tactic: have : upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω < N :=
      Nat.sSup_mem (upperCrossingTime_lt_nonempty hN) (upperCrossingTime_lt_bddAbove hab)
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : 0 < N
this : upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω < N
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
have pos : upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω ≤ N
Tactic: rw [upperCrossingTime_eq_upperCrossingTime_of_lt (hN₁.trans (hN₂.trans <| Nat.le_succ _))
      this]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : N ≤ 0
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
have hN₃ : N = 0
Tactic: rw [Nat.le_zero] at hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : N = 0
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
have neg : upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f 0 ω) ω ≤ 0
Tactic: rw [hN, upcrossingsBefore_zero, upperCrossingTime_zero, Pi.bot_apply, bot_eq_zero']
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : N = 0
neg : upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f 0 ω) ω ≤ 0
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
have neg₁ : upperCrossingTime a b f (N₂ + 1) 0 ω ≤ 0
Tactic: rw [hN, upcrossingsBefore_zero, upperCrossingTime_zero, Pi.bot_apply, bot_eq_zero']
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : N = 0
neg : upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f 0 ω) ω ≤ 0
neg₁ : upperCrossingTime a b f (N₂ + 1) 0 ω ≤ 0
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
have neg₂ : LE.le (α := ℕ) (⊥ ω) 0
Tactic: rw [hN, upcrossingsBefore_zero, upperCrossingTime_zero, Pi.bot_apply, bot_eq_zero']
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : N = 0
neg : upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f 0 ω) ω ≤ 0
neg₁ : upperCrossingTime a b f (N₂ + 1) 0 ω ≤ 0
neg₂ : LE.le (α := ℕ) (⊥ ω) 0
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
have neg₃ : LE.le (α := ℕ) ⊥ 0
Tactic: rw [hN, upcrossingsBefore_zero, upperCrossingTime_zero, Pi.bot_apply, bot_eq_zero']
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : N = 0
neg : upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f 0 ω) ω ≤ 0
neg₁ : upperCrossingTime a b f (N₂ + 1) 0 ω ≤ 0
neg₂ : LE.le (α := ℕ) (⊥ ω) 0
neg₃ : LE.le (α := ℕ) ⊥ 0
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
have neg₄ : LE.le (α := ℕ) 0 0
Tactic: rw [hN, upcrossingsBefore_zero, upperCrossingTime_zero, Pi.bot_apply, bot_eq_zero']
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upcrossingsBefore a b f N ω < n
⊢ N ≤ upperCrossingTime a b f N n ω
have hn₁ : sSup {n : ℕ | upperCrossingTime a b f N n ω < N} < n
Tactic: rw [upcrossingsBefore] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : sSup {n : ℕ | upperCrossingTime a b f N n ω < N} < n
⊢ N ≤ upperCrossingTime a b f N n ω
have rw : ¬upperCrossingTime a b f N n ω < N
Tactic: rw [← not_lt]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upcrossingsBefore a b f N ω < n
⊢ stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω -
      stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N n ω) : WithTop ℕ)) ω =
    0
have this : N ≤ upperCrossingTime a b f N n ω
Tactic: have : N ≤ upperCrossingTime a b f N n ω := by
    rw [upcrossingsBefore] at hn
    rw [← not_lt]
    exact fun h => not_le.2 hn (le_csSup (upperCrossingTime_lt_bddAbove hab) h)
-- 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
⊢ (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
    ∑ k ∈ Finset.range N, upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω
have pos : ∀ (hN : N = 0),
  (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
    ∑ k ∈ Finset.range N, upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω
Tactic: by_cases hN : N = 0
-- 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
pos :
  ∀ (hN : N = 0),
    (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
      ∑ k ∈ Finset.range N, upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω
⊢ (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
    ∑ k ∈ Finset.range N, upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω
have neg : ∀ (hN : ¬N = 0),
  (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
    ∑ k ∈ Finset.range N, upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω
Tactic: by_cases hN : N = 0
-- 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
⊢ (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
    ∑ k ∈ Finset.range N, upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω
have neg : (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
  ∑ x ∈ Finset.range N,
    ∑ x_1 ∈ Finset.range N,
      (Set.Ico (lowerCrossingTime a b f N x_1 ω) (upperCrossingTime a b f N (x_1 + 1) ω)).indicator
        (fun (j : ℕ) ↦ f (j + 1) ω - f j ω) x
Tactic: simp_rw [upcrossingStrat, Finset.sum_mul, ←
    Set.indicator_mul_left _ _ (fun x ↦ (f (x + 1) - f x) ω), Pi.one_apply, Pi.sub_apply, one_mul]
-- 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
⊢ (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
    ∑ x ∈ Finset.range N,
      ∑ x_1 ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N x_1 ω) (upperCrossingTime a b f N (x_1 + 1) ω)).indicator
          (fun (j : ℕ) ↦ f (j + 1) ω - f j ω) x
have neg : (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
  ∑ y ∈ Finset.range N,
    ∑ x ∈ Finset.range N,
      (Set.Ico (lowerCrossingTime a b f N y ω) (upperCrossingTime a b f N (y + 1) ω)).indicator
        (fun (j : ℕ) ↦ f (j + 1) ω - f j ω) x
Tactic: rw [Finset.sum_comm]
-- 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
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 ℕ)) ω
have rw : f (upperCrossingTime a b f N (k + 1) ω) ω - f (lowerCrossingTime a b f N k ω) ω =
  stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
    stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
Tactic: rw [Finset.sum_indicator_eq_sum_filter, (_ : Finset.filter (fun i => i ∈ Set.Ico
      (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)) (Finset.range N) =
      Finset.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)),
      Finset.sum_Ico_eq_add_neg _ lowerCrossingTime_le_upperCrossingTime_succ,
      Finset.sum_range_sub fun n => f n ω, Finset.sum_range_sub fun n => f n ω, neg_sub,
      sub_add_sub_cancel]
-- 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
k : ℕ
rw :
  f (upperCrossingTime a b f N (k + 1) ω) ω - f (lowerCrossingTime a b f N k ω) ω =
    stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
      stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
⊢ ∑ 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 ℕ)) ω
have rw₁ : {i ∈ Finset.range N | i ∈ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)} =
  Finset.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)
Tactic: rw [Finset.sum_indicator_eq_sum_filter, (_ : Finset.filter (fun i => i ∈ Set.Ico
      (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)) (Finset.range N) =
      Finset.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)),
      Finset.sum_Ico_eq_add_neg _ lowerCrossingTime_le_upperCrossingTime_succ,
      Finset.sum_range_sub fun n => f n ω, Finset.sum_range_sub fun n => f n ω, neg_sub,
      sub_add_sub_cancel]
-- 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
k : ℕ
⊢ {i ∈ Finset.range N | i ∈ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)} =
    Finset.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)
have h : ∀ (i : ℕ),
  i ∈ {i ∈ Finset.range N | i ∈ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)} ↔
    i ∈ Finset.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)
Tactic: ext i
-- 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
k i : ℕ
⊢ i ∈ {i ∈ Finset.range N | i ∈ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)} ↔
    i ∈ Finset.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)
have h : lowerCrossingTime a b f N k ω ≤ i → i < upperCrossingTime a b f N (k + 1) ω → i < N
Tactic: simp only [Set.mem_Ico, Finset.mem_filter, Finset.mem_range, Finset.mem_Ico,
        and_iff_right_iff_imp, and_imp]
-- 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
⊢ (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
    ∑ y ∈ Finset.range N,
      ∑ x ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N y ω) (upperCrossingTime a b f N (y + 1) ω)).indicator
          (fun (j : ℕ) ↦ f (j + 1) ω - f j ω) x
have 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 ℕ)) ω
Tactic: have 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) ω : ℕ)) ω -
        stoppedValue f (fun ω ↦ (lowerCrossingTime a b f N k ω : ℕ)) ω := by
    intro k
    rw [Finset.sum_indicator_eq_sum_filter, (_ : Finset.filter (fun i => i ∈ Set.Ico
      (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)) (Finset.range N) =
      Finset.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)),
      Finset.sum_Ico_eq_add_neg _ lowerCrossingTime_le_upperCrossingTime_succ,
      Finset.sum_range_sub fun n => f n ω, Finset.sum_range_sub fun n => f n ω, neg_sub,
      sub_add_sub_cancel]
    · rfl
    · ext i
      simp only [Set.mem_Ico, Finset.mem_filter, Finset.mem_range, Finset.mem_Ico,
        and_iff_right_iff_imp, and_imp]
      exact fun _ h => lt_of_lt_of_le h upperCrossingTime_le
-- 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 ℕ)) ω
⊢ (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
    ∑ y ∈ Finset.range N,
      ∑ x ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N y ω) (upperCrossingTime a b f N (y + 1) ω)).indicator
          (fun (j : ℕ) ↦ f (j + 1) ω - f j ω) x
have neg : (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: simp_rw [h₁]
-- 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 (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 ℕ)) ω))
have h : ∀ (i : ℕ) (hi : i ∈ Finset.range (upcrossingsBefore a b f N ω)),
  b - a ≤
    stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ)) ω -
      stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N i ω) : WithTop ℕ)) ω
Tactic: gcongr ∑ k ∈ _, ?_ with 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 : ℕ
hi : i ∈ Finset.range (upcrossingsBefore a b f N ω)
⊢ b - a ≤
    stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ)) ω -
      stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N i ω) : WithTop ℕ)) ω
have h : i < upcrossingsBefore a b f N ω
Tactic: refine le_sub_of_le_upcrossingsBefore (zero_lt_iff.2 hN) hab ?_
-- 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 : ℕ
hi : i ∈ Finset.range (upcrossingsBefore a b f N ω)
⊢ i < upcrossingsBefore a b f N ω
have h : ∀ (hi : i < upcrossingsBefore a b f N ω), i < upcrossingsBefore a b f N ω
Tactic: rwa [Finset.mem_range] at hi
Cleared hypotheses: hi