simp_rw [Filter.eventually_smallSets, bddAbove_def]
case intro.intro.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y)
y' : β
hy' : y < y'
s : Set α
hsl : s ∈ l
hs : ∀ y ∈ s, f y ≤ y'
⊢ ∀ᶠ (s : Set α) in l.smallSets, BddAbove (f '' s)
case intro.intro.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y)
y' : β
hy' : y < y'
s : Set α
hsl : s ∈ l
hs : ∀ y ∈ s, f y ≤ y'
⊢ ∃ s ∈ l, ∀ t ⊆ s, ∃ x, ∀ y ∈ f '' t, y ≤ x