Commit 2020-12-14 08:35 6f69741b

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.