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.