-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem upcrossingStrat_le_one : upcrossingStrat a b f N n ω ≤ 1

Proof state:
case h.inr
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
a✝¹ : i ∈ ↑(Finset.range N)
j : ℕ
a✝ : j ∈ ↑(Finset.range N)
hij : i ≠ j
hij' : i > j
⊢ upperCrossingTime a b f N (i + 1) ω ⊓ upperCrossingTime a b f N (j + 1) ω ≤
    lowerCrossingTime a b f N i ω ⊔ lowerCrossingTime a b f N j ω

Tactic:
rw [gt_iff_lt] at hij'

Result:
case h.inr
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
a✝¹ : i ∈ ↑(Finset.range N)
j : ℕ
a✝ : j ∈ ↑(Finset.range N)
hij : i ≠ j
hij' : j < i
⊢ upperCrossingTime a b f N (i + 1) ω ⊓ upperCrossingTime a b f N (j + 1) ω ≤
    lowerCrossingTime a b f N i ω ⊔ lowerCrossingTime a b f N j ω

Proof state:
case h
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
a✝¹ : i ∈ ↑(Finset.range N)
j : ℕ
a✝ : j ∈ ↑(Finset.range N)
hij : i ≠ j
⊢ Function.onFun Disjoint (fun k => Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)) i j

Tactic:
simp only [Set.Ico_disjoint_Ico]

Result:
case h
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
a✝¹ : i ∈ ↑(Finset.range N)
j : ℕ
a✝ : j ∈ ↑(Finset.range N)
hij : i ≠ j
⊢ upperCrossingTime a b f N (i + 1) ω ⊓ upperCrossingTime a b f N (j + 1) ω ≤
    lowerCrossingTime a b f N i ω ⊔ lowerCrossingTime a b f N j ω

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
⊢ upcrossingStrat a b f N n ω ≤ 1

Tactic:
rw [upcrossingStrat, ← Finset.indicator_biUnion_apply]

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
⊢ (⋃ i ∈ Finset.range N, Set.Ico (lowerCrossingTime a b f N i ω) (upperCrossingTime a b f N (i + 1) ω)).indicator 1 n ≤
    1

case h
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
⊢ (↑(Finset.range N)).PairwiseDisjoint fun k =>
    Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)

Proof state:
case h.inl
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
a✝¹ : i ∈ ↑(Finset.range N)
j : ℕ
a✝ : j ∈ ↑(Finset.range N)
hij : i ≠ j
hij' : i < j
⊢ upperCrossingTime a b f N i.succ ω ≤ lowerCrossingTime a b f N j ω

Tactic:
refine le_trans upperCrossingTime_le_lowerCrossingTime
  (lowerCrossingTime_mono (Nat.succ_le_of_lt hij'))

Result:
no goals

Proof state:
case h.inl
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
a✝¹ : i ∈ ↑(Finset.range N)
j : ℕ
a✝ : j ∈ ↑(Finset.range N)
hij : i ≠ j
hij' : i < j
⊢ upperCrossingTime a b f N (i + 1) ω ⊓ upperCrossingTime a b f N (j + 1) ω ≤
    lowerCrossingTime a b f N i ω ⊔ lowerCrossingTime a b f N j ω

Tactic:
rw [min_eq_left (upperCrossingTime_mono (Nat.succ_le_succ hij'.le) :
  upperCrossingTime a b f N _ ω ≤ upperCrossingTime a b f N _ ω),
  max_eq_right (lowerCrossingTime_mono hij'.le :
    lowerCrossingTime a b f N _ _ ≤ lowerCrossingTime _ _ _ _ _ _)]

Result:
case h.inl
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
a✝¹ : i ∈ ↑(Finset.range N)
j : ℕ
a✝ : j ∈ ↑(Finset.range N)
hij : i ≠ j
hij' : i < j
⊢ upperCrossingTime a b f N i.succ ω ≤ lowerCrossingTime a b f N j ω

Proof state:
case h
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
⊢ (↑(Finset.range N)).PairwiseDisjoint fun k =>
    Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)

Tactic:
intro i _ j _ hij

Result:
case h
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
a✝¹ : i ∈ ↑(Finset.range N)
j : ℕ
a✝ : j ∈ ↑(Finset.range N)
hij : i ≠ j
⊢ Function.onFun Disjoint (fun k => Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)) i j

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
⊢ (⋃ i ∈ Finset.range N, Set.Ico (lowerCrossingTime a b f N i ω) (upperCrossingTime a b f N (i + 1) ω)).indicator 1 n ≤
    1

Tactic:
exact Set.indicator_le_self' (fun _ _ => zero_le_one) _

Result:
no goals

Proof state:
case h
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
a✝¹ : i ∈ ↑(Finset.range N)
j : ℕ
a✝ : j ∈ ↑(Finset.range N)
hij : i ≠ j
⊢ upperCrossingTime a b f N (i + 1) ω ⊓ upperCrossingTime a b f N (j + 1) ω ≤
    lowerCrossingTime a b f N i ω ⊔ lowerCrossingTime a b f N j ω

Tactic:
obtain hij' | hij' := lt_or_gt_of_ne hij

Result:
case h.inl
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
a✝¹ : i ∈ ↑(Finset.range N)
j : ℕ
a✝ : j ∈ ↑(Finset.range N)
hij : i ≠ j
hij' : i < j
⊢ upperCrossingTime a b f N (i + 1) ω ⊓ upperCrossingTime a b f N (j + 1) ω ≤
    lowerCrossingTime a b f N i ω ⊔ lowerCrossingTime a b f N j ω

case h.inr
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
a✝¹ : i ∈ ↑(Finset.range N)
j : ℕ
a✝ : j ∈ ↑(Finset.range N)
hij : i ≠ j
hij' : i > j
⊢ upperCrossingTime a b f N (i + 1) ω ⊓ upperCrossingTime a b f N (j + 1) ω ≤
    lowerCrossingTime a b f N i ω ⊔ lowerCrossingTime a b f N j ω

Proof state:
case h.inr
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
a✝¹ : i ∈ ↑(Finset.range N)
j : ℕ
a✝ : j ∈ ↑(Finset.range N)
hij : i ≠ j
hij' : j < i
⊢ upperCrossingTime a b f N (i + 1) ω ⊓ upperCrossingTime a b f N (j + 1) ω ≤
    lowerCrossingTime a b f N i ω ⊔ lowerCrossingTime a b f N j ω

Tactic:
rw [min_eq_right (upperCrossingTime_mono (Nat.succ_le_succ hij'.le) :
  upperCrossingTime a b f N _ ω ≤ upperCrossingTime a b f N _ ω),
  max_eq_left (lowerCrossingTime_mono hij'.le :
    lowerCrossingTime a b f N _ _ ≤ lowerCrossingTime _ _ _ _ _ _)]

Result:
case h.inr
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
a✝¹ : i ∈ ↑(Finset.range N)
j : ℕ
a✝ : j ∈ ↑(Finset.range N)
hij : i ≠ j
hij' : j < i
⊢ upperCrossingTime a b f N j.succ ω ≤ lowerCrossingTime a b f N i ω

Proof state:
case h.inr
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
a✝¹ : i ∈ ↑(Finset.range N)
j : ℕ
a✝ : j ∈ ↑(Finset.range N)
hij : i ≠ j
hij' : j < i
⊢ upperCrossingTime a b f N j.succ ω ≤ lowerCrossingTime a b f N i ω

Tactic:
refine le_trans upperCrossingTime_le_lowerCrossingTime
  (lowerCrossingTime_mono (Nat.succ_le_of_lt hij'))

Result:
no goals