Theorem: fourier_surjection_on_schwartz (PrimeNumberTheoremAnd/Wiener.lean)

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

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : 𝓢(ℝ, ℂ)
⊢ 𝓕 ⇑((fourierTransformCLE ℝ).symm f) = ⇑f
Tactic:
rw [← fourierTransformCLE_apply ℝ]
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : 𝓢(ℝ, ℂ)
⊢ ⇑((fourierTransformCLE ℝ) ((fourierTransformCLE ℝ).symm f)) = ⇑f

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : 𝓢(ℝ, ℂ)
⊢ ⇑((fourierTransformCLE ℝ) ((fourierTransformCLE ℝ).symm f)) = ⇑f
Tactic:
simp
State after:
no goals