# Commit 2023-05-24 02:31 3a69562d

View on Github →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`

.