mathlib3

chore(data/equiv/basic): simp to_fun to coe

#2256

Merged