-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem upcrossings_lt_top_iff :
    upcrossings a b f ω < ∞ ↔ ∃ k, ∀ N, upcrossingsBefore a b f N ω ≤ k

Proof state:
case mp
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
⊢ upcrossings a b f ω < ⊤ → ∃ k, upcrossings a b f ω ≤ ↑k

Tactic:
intro h

Result:
case mp
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
h : upcrossings a b f ω < ⊤
⊢ ∃ k, upcrossings a b f ω ≤ ↑k

Proof state:
case mp.intro.intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℝ≥0
hk : ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k
m : ℕ
hm : k ≤ ↑m
⊢ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k

Tactic:
refine ⟨m, fun N => Nat.cast_le.1 ((hk N).trans ?_)⟩

Result:
case mp.intro.intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℝ≥0
hk : ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k
m : ℕ
hm : k ≤ ↑m
N : ℕ
⊢ ↑k ≤ ↑m

Proof state:
case mpr
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
⊢ (∃ k, upcrossings a b f ω ≤ ↑k) → upcrossings a b f ω < ⊤

Tactic:
rintro ⟨k, hk⟩

Result:
case mpr.intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
k : ℝ≥0
hk : upcrossings a b f ω ≤ ↑k
⊢ upcrossings a b f ω < ⊤

Proof state:
case mpr.intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℕ
hk : ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
⊢ ∃ k, ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k

Tactic:
refine ⟨k, fun N => ?_⟩

Result:
case mpr.intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℕ
hk : ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
N : ℕ
⊢ ↑(upcrossingsBefore a b f N ω) ≤ ↑↑k

Proof state:
case mpr.intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℕ
hk : ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
N : ℕ
⊢ ↑(upcrossingsBefore a b f N ω) ≤ ↑↑k

Tactic:
simp only [ENNReal.coe_natCast, Nat.cast_le, hk N]

Result:
no goals

Proof state:
case mpr.intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
k : ℝ≥0
hk : upcrossings a b f ω ≤ ↑k
⊢ upcrossings a b f ω < ⊤

Tactic:
exact lt_of_le_of_lt hk ENNReal.coe_lt_top

Result:
no goals

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
⊢ upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k

Tactic:
constructor

Result:
case mp
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
⊢ upcrossings a b f ω < ⊤ → ∃ k, upcrossings a b f ω ≤ ↑k

case mpr
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
⊢ (∃ k, upcrossings a b f ω ≤ ↑k) → upcrossings a b f ω < ⊤

Proof state:
case mp.intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℝ≥0
hk : ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k
⊢ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k

Tactic:
obtain ⟨m, hm⟩ := exists_nat_ge k

Result:
case mp.intro.intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℝ≥0
hk : ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k
m : ℕ
hm : k ≤ ↑m
⊢ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k

Proof state:
case mp.intro.intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℝ≥0
hk : ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k
m : ℕ
hm : k ≤ ↑m
N : ℕ
⊢ ↑k ≤ ↑m

Tactic:
rwa [← ENNReal.coe_natCast, ENNReal.coe_le_coe]

Result:
no goals

Proof state:
case mp
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
h : upcrossings a b f ω < ⊤
⊢ ∃ k, upcrossings a b f ω ≤ ↑k

Tactic:
lift upcrossings a b f ω to ℝ≥0 using h.ne with r hr

Result:
case mp.intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ≥0
hr : ↑r = upcrossings a b f ω
upcrossings_lt_top_iff✝ upcrossings_lt_top_iff : ↑r < ⊤ ↔ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
h✝ h : ↑r < ⊤
⊢ ∃ k, ↑r ≤ ↑k

Proof state:
case mp.intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ≥0
hr : ↑r = upcrossings a b f ω
upcrossings_lt_top_iff✝ upcrossings_lt_top_iff : ↑r < ⊤ ↔ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
h✝ h : ↑r < ⊤
⊢ ∃ k, ↑r ≤ ↑k

Tactic:
exact ⟨r, le_rfl⟩

Result:
no goals

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
⊢ upcrossings a b f ω < ⊤ ↔ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k

Tactic:
simp_rw [this, upcrossings, iSup_le_iff]

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
⊢ (∃ k, ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k) ↔ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
⊢ (∃ k, ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k) ↔ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k

Tactic:
constructor <;> rintro ⟨k, hk⟩

Result:
case mp.intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℝ≥0
hk : ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k
⊢ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k

case mpr.intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℕ
hk : ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
⊢ ∃ k, ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k