-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem upperCrossingTime_bound_eq (f : ℕ → Ω → ℝ) (N : ℕ) (ω : Ω) (hab : a < b) :
    upperCrossingTime a b f N N ω = N

Proof state:
case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : Nat.find ⋯ ≤ N
⊢ upperCrossingTime a b f N N ω = N

Tactic:
exact upperCrossingTime_stabilize hN' (Nat.find_spec (exists_upperCrossingTime_eq f N ω hab))

Result:
no goals

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find ⋯
⊢ StrictMonoOn (fun n => upperCrossingTime a b f N n ω) (Set.Iic (Nat.find ⋯).pred)

Tactic:
refine strictMonoOn_Iic_of_lt_succ fun m hm => upperCrossingTime_lt_succ hab ?_

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find ⋯
m : ℕ
hm : m < (Nat.find ⋯).pred
⊢ upperCrossingTime a b f N (m + 1) ω ≠ N

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find ⋯
m : ℕ
hm : m.succ < Nat.find ⋯
⊢ upperCrossingTime a b f N (m + 1) ω ≠ N

Tactic:
convert Nat.find_min _ hm

Result:
no goals

Proof state:
case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find ⋯
⊢ upperCrossingTime a b f N N ω = N

Tactic:
refine le_antisymm upperCrossingTime_le ?_

Result:
case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find ⋯
⊢ N ≤ upperCrossingTime a b f N N ω

Proof state:
case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find ⋯
⊢ N ≤ upperCrossingTime a b f N N ω

Tactic:
have hmono : StrictMonoOn (fun n => upperCrossingTime a b f N n ω)
    (Set.Iic (Nat.find (exists_upperCrossingTime_eq f N ω hab)).pred) := by
  refine strictMonoOn_Iic_of_lt_succ fun m hm => upperCrossingTime_lt_succ hab ?_
  rw [Nat.lt_pred_iff] at hm
  convert Nat.find_min _ hm

Result:
case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find ⋯
hmono : StrictMonoOn (fun n => upperCrossingTime a b f N n ω) (Set.Iic (Nat.find ⋯).pred)
⊢ N ≤ upperCrossingTime a b f N N ω

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find ⋯
m : ℕ
hm : m < (Nat.find ⋯).pred
⊢ upperCrossingTime a b f N (m + 1) ω ≠ N

Tactic:
rw [Nat.lt_pred_iff] at hm

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find ⋯
m : ℕ
hm : m.succ < Nat.find ⋯
⊢ upperCrossingTime a b f N (m + 1) ω ≠ N

Proof state:
case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : ¬N < Nat.find ⋯
⊢ upperCrossingTime a b f N N ω = N

Tactic:
rw [not_lt] at hN'

Result:
case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : Nat.find ⋯ ≤ N
⊢ upperCrossingTime a b f N N ω = N

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
⊢ upperCrossingTime a b f N N ω = N

Tactic:
by_cases hN' : N < Nat.find (exists_upperCrossingTime_eq f N ω hab)

Result:
case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find ⋯
⊢ upperCrossingTime a b f N N ω = N

case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : ¬N < Nat.find ⋯
⊢ upperCrossingTime a b f N N ω = N

Proof state:
case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find ⋯
hmono : StrictMonoOn (fun n => upperCrossingTime a b f N n ω) (Set.Iic (Nat.find ⋯).pred)
⊢ N ≤ upperCrossingTime a b f N N ω

Tactic:
convert StrictMonoOn.Iic_id_le hmono N (Nat.le_sub_one_of_lt hN')

Result:
no goals