specialize hC u
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
C : ℝ
hC : ∀ (x : ℝ), ‖↑(1 + x ^ 2) * ψ.toFun x‖ ≤ C
u : ℝ
⊢ ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
C u : ℝ
hC : ‖↑(1 + u ^ 2) * ψ.toFun u‖ ≤ C
⊢ ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)