ring_nf
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
l5 : Differentiable ℝ (deriv f.toFun)
⊢ (𝓕 f.toFun u + ↑u ^ 2 * 𝓕 f.toFun u) * (↑π ^ 2 * 4) =
    𝓕 (fun x => f.toFun x) u * (↑π ^ 2 * 4) - 2 * ↑π * I * ↑u * (2 * ↑π * I * ↑u * 𝓕 f.toFun u)
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
l5 : Differentiable ℝ (deriv f.toFun)
⊢ 𝓕 f.toFun u * ↑u ^ 2 * ↑π ^ 2 * 4 + 𝓕 f.toFun u * ↑π ^ 2 * 4 =
    -(𝓕 f.toFun u * ↑u ^ 2 * ↑π ^ 2 * I ^ 2 * 4) + 𝓕 (fun x => f.toFun x) u * ↑π ^ 2 * 4