Real.fourierIntegral_conj_neg

lemma Real.fourierIntegral_conj_neg {f : ℝ → ℂ} (y : ℝ) :    𝓕 (fun x ↦ conj (f (-x))) y = conj (𝓕 f y) := by  simp only [fourier_real_eq]  have h_conj : ∀ x, 𝐞 (-(x * y)) • conj (f (-x)) = conj (𝐞 (x * y) • f (-x)) := fun x ↦ by    simp only [Circle.smul_def, Real.fourierChar_apply, map_mul, smul_eq_mul, neg_mul,      Complex.ofReal_neg, mul_neg]    congr 1    rw [← Complex.exp_conj]    simp only [map_mul, Complex.conj_I, Complex.conj_ofReal, mul_neg]  calc ∫ x, 𝐞 (-(x * y)) • conj (f (-x))      = ∫ x, conj (𝐞 (x * y) • f (-x)) := by congr 1; ext x; exact h_conj x    _ = conj (∫ x, 𝐞 (x * y) • f (-x)) := integral_conj    _ = conj (∫ x, 𝐞 (-(x * y)) • f x) := by        rw [← integral_neg_eq_self (fun x => 𝐞 (-(x * y)) • f x)]        congr 2 with x; ring_nf