rw [← integral_sub (integrable_fourierIntegrand _ ξ) ((integrable_fourierIntegrand f ξ).smul' _)]
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
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ∫ (a : ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • ((derivCLM ℝ) f) a -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a =
    0