simp only at this
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
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f 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