simp only [dite_true, Finset.sum_subtype _ h_mem]
E' : Type ?u.1249490
ι : 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✝²² : DecidableEq ι
inst✝²¹ : Fintype ι
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : (i : ι) → NormedAddCommGroup (M i)
inst✝¹⁸ : (i : ι) → NormedSpace ℝ (M i)
inst✝¹⁷ : NormedAddCommGroup D
inst✝¹⁶ : NormedSpace ℝ D
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : InnerProductSpace ℝ E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : InnerProductSpace ℝ E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℂ F
inst✝⁹ : NormedSpace 𝕜 F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : MeasurableSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace E'
inst✝² : FiniteDimensional ℝ E'
inst✝¹ : BorelSpace E'
inst✝ : CompleteSpace F
i : ι
f : 𝓢(ι → ℝ, F)
ξ : ι → ℝ
h_mem : ∀ (j : ι), j ∈ Finset.univ \ {i} ↔ j ≠ i
⊢ ∫ (x : { j // j ≠ i } → ℝ) (u : ℝ),
      ↑(Real.fourierChar
            (Multiplicative.ofAdd
              (-((Equiv.piSplitAt i fun a => ℝ).symm (u, x) i * ξ i +
                  ∑ i_1 in Finset.univ \ {i}, (Equiv.piSplitAt i fun a => ℝ).symm (u, x) i_1 * ξ i_1)))) •
        ((pderivCLM ℝ (Pi.single i 1)) f) ((Equiv.piSplitAt i fun a => ℝ).symm (u, x)) =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
E' : Type ?u.1249490
ι : 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✝²² : DecidableEq ι
inst✝²¹ : Fintype ι
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : (i : ι) → NormedAddCommGroup (M i)
inst✝¹⁸ : (i : ι) → NormedSpace ℝ (M i)
inst✝¹⁷ : NormedAddCommGroup D
inst✝¹⁶ : NormedSpace ℝ D
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : InnerProductSpace ℝ E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : InnerProductSpace ℝ E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℂ F
inst✝⁹ : NormedSpace 𝕜 F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : MeasurableSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace E'
inst✝² : FiniteDimensional ℝ E'
inst✝¹ : BorelSpace E'
inst✝ : CompleteSpace F
i : ι
f : 𝓢(ι → ℝ, F)
ξ : ι → ℝ
h_mem : ∀ (j : ι), j ∈ Finset.univ \ {i} ↔ j ≠ i
⊢ ∫ (x : { j // j ≠ i } → ℝ) (u : ℝ),
      ↑(Real.fourierChar
            (Multiplicative.ofAdd
              (-((Equiv.piSplitAt i fun a => ℝ).symm (u, x) i * ξ i +
                  ∑ a : { x // x ≠ i }, (Equiv.piSplitAt i fun a => ℝ).symm (u, x) ↑a * ξ ↑a)))) •
        ((pderivCLM ℝ (Pi.single i 1)) f) ((Equiv.piSplitAt i fun a => ℝ).symm (u, x)) =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ