mathlib

27f315c5 - feat(analysis/calculus/cont_diff): Prove that `fderiv_within` is `C^n` for functions with parameters (#16946)

feat(analysis/calculus/cont_diff): Prove that `fderiv_within` is `C^n` for functions with parameters (#16946) * Prove that `fderiv_within` is `C^n` (at a point within a set) for a function with parameters * There are some inconvenient side-conditions needed for the lemmas, feel free to recommend improvements * `set.diag_image` is not used, but a (useful) left-over used before a refactor. * This is useful for lemmas about `mfderiv` and the smooth vector bundle refactor * From the sphere eversion project