-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem mul_upcrossingsBefore_le (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) ω

Proof state:
case neg
Ω : 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) ω

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]

Result:
case neg
Ω : 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

Proof state:
Ω : 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 (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω
i : ℕ
hi : i ∈ Finset.range (upcrossingsBefore a b f N ω)
⊢ i < upcrossingsBefore a b f N ω

Tactic:
rwa [Finset.mem_range] at hi

Result:
no goals

Proof state:
case neg
Ω : 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 (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω
i : ℕ
x✝ : 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')

Result:
no goals

Proof state:
case neg
Ω : 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 (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω
⊢ (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:
simp_rw [h₁]

Result:
case neg
Ω : 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 (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤
    ∑ x ∈ Finset.range N,
      (stoppedValue f (upperCrossingTime a b f N (x + 1)) ω - stoppedValue f (lowerCrossingTime a b f N x) ω)

Proof state:
case pos
Ω : 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 (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω
i : ℕ
x✝ : i ∈ Finset.range N
hi : i ∉ Finset.range (upcrossingsBefore a b f N ω)
hi' : i = upcrossingsBefore a b f N ω
⊢ 0 ≤ stoppedValue f (upperCrossingTime a b f N (i + 1)) ω - stoppedValue f (lowerCrossingTime a b f N i) ω

Tactic:
subst hi'

Result:
case pos
Ω : 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 (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω
x✝ : upcrossingsBefore a b f N ω ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)
⊢ 0 ≤
    stoppedValue f (upperCrossingTime a b f N (upcrossingsBefore a b f N ω + 1)) ω -
      stoppedValue f (lowerCrossingTime a b f N (upcrossingsBefore a b f N ω)) ω