have l1 : ∀ᶠ ε : ℝ in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2) := inter_mem_nhdsWithin _ (Iio_mem_nhds (by positivity))
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
⊢ ∀ᶠ (x : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (↑⌈x.1 * ↑x.2⌉₊ / ↑x.2) 0 < δ
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
⊢ ∀ᶠ (x : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (↑⌈x.1 * ↑x.2⌉₊ / ↑x.2) 0 < δ