refactor(geometry/manifold): drop some unused arguments (#6545)
API changes:
* add lemmas about `map (ext_chart_at I x) (𝓝[s] x')`;
* prove `times_cont_mdiff_within_at.comp` directly without using other charts; the new proof does not need a `smooth_manifold_with_corners` instance;
* add aliases `times_cont_mdiff.times_cont_diff` etc;
* `times_cont_mdiff_map` no longer needs a `smooth_manifold_with_corners` instance;
* `has_smooth_mul` no longer extends `smooth_manifold_with_corners` and no longer takes `has_continuous_mul` as an argument;
* `has_smooth_mul_core` is gone in favor of `has_continuous_mul_of_smooth`;
* `smooth_monoid_morphism` now works with any model space (needed, e.g., to define `smooth_monoid_morphism.prod`);
* `lie_group_morphism` is gone: we use `M →* N` both for monoids and groups, no reason to have two structures in this case;
* `lie_group` no longer extends `smooth_manifold_with_corners` and no longer takes `topological_group` as an argument;
* `lie_group_core` is gone in favor of `topological_group_of_lie_group`;
* the `I : model_with_corners 𝕜 E H` argument of `smooth_mul` and `smooth_inv` is now explicit.
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
mathlib3
02251b1e - refactor(geometry/manifold): drop some unused arguments (#6545)
