simp only [← derivCLM_apply (𝕜 := ℝ)]
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (∫ (v : ℝ), ↑(Real.fourierChar (Multiplicative.ofAdd (-(v * ξ)))) • deriv (fun y => f y) v) -
      ∫ (a : ℝ), (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a =
    0
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (∫ (v : ℝ), ↑(Real.fourierChar (Multiplicative.ofAdd (-(v * ξ)))) • ((derivCLM ℝ) f) v) -
      ∫ (a : ℝ), (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a =
    0