まとめ

微分では，まず HasDerivAt，DifferentiableAt，deriv の違いを押さえることが重要です． 初等的な計算は simp や既存の微分公式で進みます． より一般の解析では，ノルム空間，連続線形写像，Frechet 微分 HasFDerivAt が基本語彙になります．

形式化の tips

微分の形式化では，deriv の値を直接計算するより，まず HasDerivAt の証明を作る方が安定することがあります．

1. 点での微分係数を主張するなら HasDerivAt．
2. 微分可能性だけなら DifferentiableAt．
3. 導関数の値を式として使うなら deriv．
4. 多変数・ノルム空間なら HasFDerivAt．
5. 計算が詰まったら，#check HasDerivAt.add のように公式を探す．