rw [Metric.tendsto_nhdsWithin_nhdsWithin]
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
⊢ Tendsto (fun c => b - a - c / A) (𝓝[<] (A * (b - a))) (𝓝[>] 0)
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ {x : ℝ}, x ∈ Iio (A * (b - a)) → dist x (A * (b - a)) < δ → b - a - x / A ∈ Ioi 0 ∧ dist (b - a - x / A) 0 < ε