chore(analysis/calculus/fderiv): squeeze simps (#17344)
chore(analysis/calculus/fderiv): squeeze simps (#17344)

Profiling:
* differentiable_at.fderiv_within: 9.56ms -> 5.49ms
* differentiable_on_univ: 40.6ms -> 6.23ms
* has_fderiv_at_filter.tendsto_nhds: 962ms -> 452ms
* has_strict_fderiv_at.add: 21.5s -> 4.79s 
* has_fderiv_at_filter.add: 11.3s -> 2.84s





leanprover-community/mathlib,leanprover-community/mathlib