# Commit 2022-07-06 11:16 f09322bc

View on Github →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]
```