mathlib

e9e08778 - refactor(data/dfinsupp/basic): Improve definitional equalities of coercions

refactor(data/dfinsupp/basic): Improve definitional equalities of coercions This means that `dfinsupp.coe_add` etc are true by definition, rather than requiring the application of `quotient.induction` first.