feat(analysis/calculus): drop unneeded assumptions (#19045)
* Prove more precise congruence lemmas for derivatives. In particular, adding or removing a single point from `s` doesn't change anything about derivatives within `s`.
* Drop `has_fderiv_within_at.antimono` and `has_deriv_within_at.antimono`, use stronger `*.mono_of_mem` lemmas instead.
* Prove some equalities about `(f)deriv_within` by using `simp` instead of `slit_ifs`: if `has_fderiv_within_at f f' s x ↔ has_fderiv_within_at g g' t y`, then `fderiv_within f s x = fderiv_within g t y`.
