rfl
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : EuclideanSpace ℝ ι → F
ξ : EuclideanSpace ℝ ι
⊢ ∫ (x : ι → ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) ((EuclideanSpace.measurableEquiv ι).symm x)) ξ))) •
        f ((EuclideanSpace.measurableEquiv ι).symm x) ∂volume =
    𝓕ₙ f ξ
no goals