refactor(geometry/manifold): redefine some instances (#7124)
* Turn `unique_diff_within_at` into a `structure`.
* Generalize `tangent_cone_at`, `unique_diff_within_at`, and `unique_diff_on` to a `semimodule` that is a `topological_space`.
* Redefine `model_with_corners_euclidean_half_space` and `model_with_corners_euclidean_quadrant` to reuse more generic lemmas, including `unique_diff_on.pi` and `unique_diff_on.univ_pi`.
* Make `model_with_corners.unique_diff'` use `target` instead of `range I`; usually it has better defeq.
Co-authored-by: @gebner
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
