The simpset `mfld_simps`

records several simp lemmas that are
especially useful in manifolds. It is a subset of the whole set of simp lemmas, but it makes it
possible to have quicker proofs (when used with `squeeze_simp`

or `simp only`

) while retaining
readability.

The typical use case is the following, in a file on manifolds:
If `simp [foo, bar]`

is slow, replace it with `squeeze_simp [foo, bar, mfld_simps]`

and paste
its output. The list of lemmas should be reasonable (contrary to the output of
`squeeze_simp [foo, bar]`

which might contain tens of lemmas), and the outcome should be quick
enough.

## Equations

- One or more equations did not get rendered due to their size.