Commit 2021-02-22 10:42 69b93fcb

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 dsimped in order to make progress with rw. With this change, dsimp now fails as the goal is already fully delta-reduced.