∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℝ → E},
  MeasureTheory.Integrable f MeasureTheory.volume →
    Differentiable ℝ f →
      MeasureTheory.Integrable (deriv f) MeasureTheory.volume →
        FourierTransform.fourier (deriv f) = fun x => (2 * ↑Real.pi * Complex.I * ↑x) • FourierTransform.fourier f x