mathlib3

6f69741b - chore(analysis/calculus/*): rename `*.of_local_homeomorph` to `local_homeomorph.*_symm` (#5358)

chore(analysis/calculus/*): rename `*.of_local_homeomorph` to `local_homeomorph.*_symm` (#5358) Rename some lemmas, and make `(f : local_homeomorph _ _)` an explicit argument: * `has_fderiv_at.of_local_homeomorph` → `local_homeomorph.has_fderiv_at_symm`; * `times_cont_diff_at.of_local_homeomorph` → `local_homeomorph.times_cont_diff_at_symm`. If we want to apply one of these lemmas to prove smoothness of, e.g., `arctan`, `log`, or `arcsin`, then the goal has no `local_homeomorph.symm`, and we need to explicitly supply a `local_homeomorph` with an appropriate `inv_fun`. Also add some lemmas that help to prove that the inverse function is **not** differentiable at a point.