refine intervalIntegral.integral_congr ?_
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 =
    ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x
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
⊢ Set.EqOn
    (fun x =>
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x)
    (fun x =>
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x)
    (Set.uIcc a b)