feat(geometry/manifold/mfderiv): more lemmas (#6679)
* move section `mfderiv_fderiv` up, add aliases;
* rename old `unique_mdiff_on.unique_diff_on` to `unique_mdiff_on.unique_diff_on_target_inter`;
* add a section about `continuous_linear_map`;
* more lemmas about `model_with_corners`;
* add lemmas about `ext_chart_at`.
