mathlib3

69b93fcb - fix(data/finsupp/basic): delta-reduce the definition of coe_fn_injective (#6344)

fix(data/finsupp/basic): delta-reduce the definition of coe_fn_injective (#6344) Without this, `apply coe_fn_injective` leaves a messy goal that usually has to be `dsimp`ed in order to make progress with `rw`. With this change, `dsimp` now fails as the goal is already fully delta-reduced.