-- Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
theorem eventually_le_limsup (hf : IsBoundedUnder (· ≤ ·) f u

Proof state:
case pos.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u✝ : β → α
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u✝) _auto✝
ha : ∃ b, limsup u✝ f < b
H : IsGLB (Set.Ioi (limsup u✝ f)) (limsup u✝ f)
u : ℕ → α
hua : Tendsto u atTop (𝓝 (limsup u✝ f))
hu : ∀ (n : ℕ), u n ∈ Set.Ioi (limsup u✝ f)
⊢ ∀ᶠ (b : β) in f, u✝ b ≤ limsup u✝ f

Tactic:
have := fun n => eventually_lt_of_limsup_lt (hu n) hf

Result:
case pos.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u✝ : β → α
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u✝) _auto✝
ha : ∃ b, limsup u✝ f < b
H : IsGLB (Set.Ioi (limsup u✝ f)) (limsup u✝ f)
u : ℕ → α
hua : Tendsto u atTop (𝓝 (limsup u✝ f))
hu : ∀ (n : ℕ), u n ∈ Set.Ioi (limsup u✝ f)
this : ∀ (n : ℕ), ∀ᶠ (a : β) in f, u✝ a < u n
⊢ ∀ᶠ (b : β) in f, u✝ b ≤ limsup u✝ f

Proof state:
case neg.intro.intro
α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
ha : ∃ b, limsup u f < b
H : ¬IsGLB (Set.Ioi (limsup u f)) (limsup u f)
x : α
hx : ∀ ⦃b : α⦄, limsup u f < b → x ≤ b
xa : limsup u f < x
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f

Tactic:
filter_upwards [eventually_lt_of_limsup_lt xa hf] with y hy

Result:
case h
α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
ha : ∃ b, limsup u f < b
H : ¬IsGLB (Set.Ioi (limsup u f)) (limsup u f)
x : α
hx : ∀ ⦃b : α⦄, limsup u f < b → x ≤ b
xa : limsup u f < x
y : β
hy : u y < x
⊢ u y ≤ limsup u f

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f

Tactic:
obtain ha | ha := isTop_or_exists_gt (f.limsup u)

Result:
case inl
α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
ha : IsTop (limsup u f)
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f

case inr
α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
ha : ∃ b, limsup u f < b
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f