have := intervalIntegral.integral_deriv_smul_eq_sub (a := a) (b := b)
  (u := fun x ↦ Real.fourierChar[-(x * ξ)])
  (v := fun x ↦ f x)
  (u' := fun x ↦ (-ξ) • (2 * π * I * Real.fourierChar[-(x * ξ)]))
  (v' := fun x ↦ deriv f x)
  (fun x _ ↦ .comp_of_tower x (Real.hasDerivAt_fourierChar _) (hasDerivAt_mul_const ξ).neg)
  (fun x _ ↦ f.differentiableAt.hasDerivAt)
  (Continuous.continuousOn <|
    .const_smul (.mul continuous_const (continuous_mul_right ξ).neg.realFourierChar) _)
  (by simpa [derivCLM_apply ℝ] using (derivCLM ℝ f).continuous.continuousOn)
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
⊢ ∫ (x : ℝ) in a..b,
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (fun x => -ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) x • (fun x => f x) x +
        (fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))) x • (fun x => deriv (⇑f) x) x =
    (fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))) b • (fun x => f x) b -
      (fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))) a • (fun x => f x) a
⊢ ∫ (x : ℝ) in a..b,
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a