refine .congr_deriv (_root_.hasDerivAt_fourierIntegral f.integrable ?_ ξ) ?_
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ HasDerivAt (fun ξ => 𝓕 (fun x => f x) ξ) (-((2 * ↑π * I) • 𝓕 (fun x => x • f x) ξ)) ξ
case refine_1
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ Integrable fun x => x • f x

case refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ 𝓕 (fun x => (-2 * ↑π * I * ↑x) • f x) ξ = -((2 * ↑π * I) • 𝓕 (fun x => x • f x) ξ)