chore(data/equiv/basic): simp to_fun to coe (#2256)
* chore(data/equiv/basic): simp to_fun to coe
* fix proofs
* Update src/data/equiv/basic.lean
* fix proof
* partially removing to_fun
* finish switching to coercions
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
