Theorem: SchwartzMap.Real.hasDerivAt_fourierIntegral (ForML/SchwartzRealFourier.lean)

State before:
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) ξ)) ξ
Tactic:
refine .congr_deriv (_root_.hasDerivAt_fourierIntegral f.integrable ?_ ξ) ?_
State after:
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) ξ)

State before:
case refine_1
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ Integrable fun x => x • f x
Tactic:
exact (hasTemperateGrowth_smul Function.hasTemperateGrowth_id f).integrable
State after:
no goals

State before:
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) ξ)
Tactic:
simp [Real.fourierIntegral_def, integral_neg,
  ← smul_smul (2 * π * I), smul_comm _ (2 * π * I), integral_smul]
State after:
no goals