# Commit 2020-05-06 19:39 460d9d43

View on Github →refactor(data/equiv/local_equiv, topology/local_homeomorph): use coercions (#2603)
Local equivs and local homeomorphisms use `e.to_fun x`

and `e.inv_fun x`

, instead of coercions as in most of mathlib, as there were problems with coercions that made them unusable in manifolds. These problems have been fixed in Lean 3.10, so we switch to coercions for them also.
This is 95% a refactor PR, erasing `.to_fun`

and replacing `.inv_fun`

with `.symm`

in several files, and fixing proofs. Plus a few simp lemmas on the coercions to let things go smoothly. I have also linted all the files I have touched.