-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem exists_upcrossings_of_not_bounded_under {ι : Type*} {l : Filter ι} {x : ι → ℝ}
    (hf : liminf (fun i => (Real.nnabs (x i) : ℝ≥0∞)) l ≠ ∞)
    (hbdd : ¬IsBoundedUnder (· ≤ ·) l fun i => |x i|) :
    ∃ a b : ℚ, a < b ∧ (∃ᶠ i in l, x i < a) ∧ ∃ᶠ i in l, ↑b < x i

Proof state:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun i => |x i|
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i

Tactic:
rw [isBoundedUnder_le_abs, not_and_or] at hbdd

Result:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l x ∨ ¬IsBoundedUnder (fun x1 x2 => x1 ≥ x2) l x
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i

Proof state:
case inl.intro.intro.refine_1
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
⊢ ∃ᶠ (i : ι) in l, x i < ↑q

Tactic:
refine fun hcon => hR ?_

Result:
case inl.intro.intro.refine_1
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun i => x i < ↑q) x_1
⊢ ∀ᶠ (x_1 : ι) in l, ¬(fun n => x n < R) x_1

Proof state:
case inr.intro.intro.refine_1
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(Real.nnabs (x i))) l ≠ ⊤
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x a ≥ x_1
⊢ ∃ᶠ (i : ι) in l, x i < ↑(q - 1)

Tactic:
refine fun hcon => hbdd ↑(q - 1) ?_

Result:
case inr.intro.intro.refine_1
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(Real.nnabs (x i))) l ≠ ⊤
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x a ≥ x_1
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun i => x i < ↑(q - 1)) x_1
⊢ ∀ᶠ (a : ι) in l, x a ≥ ↑(q - 1)

Proof state:
case inl.intro
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i

Tactic:
obtain ⟨q, hq⟩ := exists_rat_gt R

Result:
case inl.intro.intro
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i

Proof state:
case inr.intro.intro.refine_2
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x1 x2 => x1 ≥ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun i => ↑q < x i) x_1
⊢ ∀ᶠ (x_1 : ι) in l, ¬(fun n => R < x n) x_1

Tactic:
filter_upwards [hcon] with x hx using not_lt.2 ((not_lt.1 hx).trans hq.le)

Result:
no goals

Proof state:
case inl.intro.intro.refine_2
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(Real.nnabs (x i))) l ≠ ⊤
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x a ≤ x_1
⊢ ∃ᶠ (i : ι) in l, ↑(q + 1) < x i

Tactic:
refine fun hcon => hbdd ↑(q + 1) ?_

Result:
case inl.intro.intro.refine_2
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(Real.nnabs (x i))) l ≠ ⊤
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x a ≤ x_1
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun i => ↑(q + 1) < x i) x_1
⊢ ∀ᶠ (a : ι) in l, x a ≤ ↑(q + 1)