refine ⟨(fourierTransformCLE ℝ).symm f, ?_⟩
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : 𝓢(ℝ, ℂ)
⊢ ∃ g, 𝓕 ⇑g = ⇑f
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : 𝓢(ℝ, ℂ)
⊢ 𝓕 ⇑((fourierTransformCLE ℝ).symm f) = ⇑f