mathlib

b9b8fdfa - `simp` can't already prove this, because we're no longer going through `coe_fn_trans`