-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem upcrossingsBefore_mono (hab : a < b) : Monotone fun N ω => upcrossingsBefore a b f N ω

Proof state:
case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
hemp : {n | upperCrossingTime a b f N n ω < N}.Nonempty
n : ℕ
hn : n ∈ {n | upperCrossingTime a b f N n ω < N}
⊢ n ∈ {n | upperCrossingTime a b f M n ω < M}

Tactic:
rw [Set.mem_setOf_eq, upperCrossingTime_eq_upperCrossingTime_of_lt hNM hn]

Result:
case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
hemp : {n | upperCrossingTime a b f N n ω < N}.Nonempty
n : ℕ
hn : n ∈ {n | upperCrossingTime a b f N n ω < N}
⊢ upperCrossingTime a b f N n ω < M

Proof state:
case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
hemp : {n | upperCrossingTime a b f N n ω < N}.Nonempty
⊢ sSup {n | upperCrossingTime a b f N n ω < N} ≤ sSup {n | upperCrossingTime a b f M n ω < M}

Tactic:
refine csSup_le_csSup (upperCrossingTime_lt_bddAbove hab) hemp fun n hn => ?_

Result:
case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
hemp : {n | upperCrossingTime a b f N n ω < N}.Nonempty
n : ℕ
hn : n ∈ {n | upperCrossingTime a b f N n ω < N}
⊢ n ∈ {n | upperCrossingTime a b f M n ω < M}

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
⊢ sSup {n | upperCrossingTime a b f N n ω < N} ≤ sSup {n | upperCrossingTime a b f M n ω < M}

Tactic:
by_cases hemp : {n : ℕ | upperCrossingTime a b f N n ω < N}.Nonempty

Result:
case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
hemp : {n | upperCrossingTime a b f N n ω < N}.Nonempty
⊢ sSup {n | upperCrossingTime a b f N n ω < N} ≤ sSup {n | upperCrossingTime a b f M n ω < M}

case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
hemp : ¬{n | upperCrossingTime a b f N n ω < N}.Nonempty
⊢ sSup {n | upperCrossingTime a b f N n ω < N} ≤ sSup {n | upperCrossingTime a b f M n ω < M}

Proof state:
case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
hemp : {n | upperCrossingTime a b f N n ω < N}.Nonempty
n : ℕ
hn : n ∈ {n | upperCrossingTime a b f N n ω < N}
⊢ upperCrossingTime a b f N n ω < M

Tactic:
exact lt_of_lt_of_le hn hNM

Result:
no goals

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
⊢ (fun N ω => upcrossingsBefore a b f N ω) N ω ≤ (fun N ω => upcrossingsBefore a b f N ω) M ω

Tactic:
simp only [upcrossingsBefore]

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
⊢ sSup {n | upperCrossingTime a b f N n ω < N} ≤ sSup {n | upperCrossingTime a b f M n ω < M}

Proof state:
case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
hemp : ¬{n | upperCrossingTime a b f N n ω < N}.Nonempty
⊢ sSup {n | upperCrossingTime a b f N n ω < N} ≤ sSup {n | upperCrossingTime a b f M n ω < M}

Tactic:
rw [Set.not_nonempty_iff_eq_empty] at hemp

Result:
case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
hemp : {n | upperCrossingTime a b f N n ω < N} = ∅
⊢ sSup {n | upperCrossingTime a b f N n ω < N} ≤ sSup {n | upperCrossingTime a b f M n ω < M}

Proof state:
case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
hemp : {n | upperCrossingTime a b f N n ω < N} = ∅
⊢ sSup {n | upperCrossingTime a b f N n ω < N} ≤ sSup {n | upperCrossingTime a b f M n ω < M}

Tactic:
simp [hemp, csSup_empty, bot_eq_zero', zero_le']

Result:
no goals

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
⊢ Monotone fun N ω => upcrossingsBefore a b f N ω

Tactic:
intro N M hNM ω

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
⊢ (fun N ω => upcrossingsBefore a b f N ω) N ω ≤ (fun N ω => upcrossingsBefore a b f N ω) M ω