mathlib3

f09322bc - feat(geometry/manifold/local_invariant_properties): simplify definitions and proofs (#15116)

feat(geometry/manifold/local_invariant_properties): simplify definitions and proofs (#15116) * Simplify the sets in `local_invariant_prop` and `lift_prop_within_at` * Simplify many proofs in `local_invariant_properties.lean` * Reorder the intersection in `cont_diff_within_at_prop` to be more consistent with all lemmas in `smooth_manifold_with_corners.lean` * New lemmas, such as `cont_mdiff_within_at_iff_of_mem_source` and properties of `local_invariant_prop` * I expect that some lemmas in `cont_mdiff.lean` can be simplified using the new definitions, but I don't do that in this PR. * Lemma renamings: ``` cont_mdiff_within_at_iff -> cont_mdiff_within_at_iff' cont_mdiff_within_at_iff' -> cont_mdiff_within_at_iff_of_mem_source' cont_mdiff_within_at_iff'' -> cont_mdiff_within_at_iff [or iff.rfl] ```