have r1 := tendsto_mul_ceil_div.const_mul C
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
⊢ ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
r1 : Tendsto (fun k => C * (↑⌈k.1 * ↑k.2⌉₊ / ↑k.2)) (𝓝[>] 0 ×ˢ atTop) (𝓝 (C * 0))
⊢ ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ