field_simp [pi_ne_zero]
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 =
    𝓕 (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 * 𝓕 f.toFun u) * (↑π ^ 2 * 4) =
    𝓕 (fun x => f.toFun x) u * (↑π ^ 2 * 4) - 2 * ↑π * I * ↑u * (2 * ↑π * I * ↑u * 𝓕 f.toFun u)