…rentials:

- make variables implicit;
- make more variables implicit and re-use some other variables.

Move Diffeomorph.toPartialDiffeomorph further down.

Touch up the docs; introduce PartialDiffeomorph.toLocalHomeomorph.

and PartialHomeomorph.continuous_{to,inv}Fun to continuousOn_{to,inv}Fun.

…rentials

…rentials

might need to read up on the variable command.

This is mathematically cleaner (I show injectivity and surjectivity of the
differential separately), cleaner in Lean (it's good practice to avoid heavy
tactic blocks in definitions) and makes all proofs by rfl work.

This requires completeness of the tangent spaces; this is slightly unfortunate,
as it was automatic in the previous approaches. Opinions welcome.

I'm a bit unsure about the local instances; we'll see if this can be avoided.

Unsure if the extChartAt statements are really necessary...

These are only one rewrite away and don't feel worth it, for me.

…ffeos-v3