Solving f'' = -f in Lean without ODE theory: energy of the error term

To show that f with HasDerivAt f f' and HasDerivAt f' (-f) equals A cos + B sin (A = f 0, B = f' 0), set e = f - (A cos + B sin) and e' = f' - (-A sin + B cos). Prove HasDerivAt e e' and HasDerivAt e' (-e) by convert (...).sub (...) using 1. The function-equality goal comes out in Pi form, so close it with funext x; simp only [Pi.sub_apply, Pi.add_apply, Pi.neg_apply]; ring. Then e² + e'² has derivative 0, it is 0 at 0, so is_const_of_deriv_eq_zero gives e ≡ 0 (nlinarith with the squares). I used this to show that if f is also π-periodic then f ≡ 0, because cos and sin flip sign under θ ↦ θ+π. Needs import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv for Real.hasDerivAt_cos/sin.