-- Module: Mathlib.Probability.Martingale.Upcrossing
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) ω
neg 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) ω
neg₂ :
  ∀ (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
neg₃ :
  ∀ (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
neg₄ :
  ∀ (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
neg₅ :
  ∀ (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 ℕ)) ω)
neg₆ :
  ∀ (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 ℕ)) ω)
neg₇ :
  ∀ (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 ω) : ℝ) ≤ ∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a)
⊢ (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
    ∑ k ∈ Finset.range N, upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω

Tactic:
classical
  by_cases hN : N = 0
  · simp [hN]
  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]
  rw [Finset.sum_comm]
  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
  simp_rw [h₁]
  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')
  refine le_trans ?_ h₂
  rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_comm]

Premises used: Pi.one_apply, HSub.hSub, Finset.card_range, HAdd.hAdd, MeasureTheory.upcrossingStrat, mul_comm, nsmul_eq_mul, Finset.sum_comm, OfNat.ofNat, Set.indicator_mul_left, one_mul, Finset.sum_mul, Pi.sub_apply, Finset.sum_const