chore(analysis/calculus/{f,}deriv): fix, add missing lemmas (#8574)
* use `prod.fst` and `prod.snd` in lemmas like `has_fderiv_at_fst`;
* add `has_strict_deriv_at.prod`,
`has_strict_fderiv_at.comp_has_strict_deriv_at`;
* use `set.maps_to` in some lemmas;
* golf some proofs.