have l2 : 1 + u ^ 2 = ‖(1 : ℂ) + u ^ 2‖ := by
  norm_cast ; simp only [Complex.norm_eq_abs, Complex.abs_ofReal, abs_eq_self.2 l1.le]
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
⊢ ‖𝓕 f.toFun u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
⊢ ‖𝓕 f.toFun u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹