by_cases h : n = 0 <;> simp [h, nterm]
case intro.refine_2.hp
n✝ : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
σ' : ℝ
hσ' : 1 < σ'
n : ℕ
⊢ nterm f σ' n ≤ ‖f n‖ / ↑n
case neg
n✝ : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
σ' : ℝ
hσ' : 1 < σ'
n : ℕ
h : ¬n = 0
⊢ Complex.abs (f n) / ↑n ^ σ' ≤ Complex.abs (f n) / ↑n