mathlib3

03a477c4 - feat(data/dfinsupp): Port over the `finsupp.lift_add_hom` API (#4821)

feat(data/dfinsupp): Port over the `finsupp.lift_add_hom` API (#4821) These lemmas are mostly copied with minimal translation from `finsupp`. A few proofs are taken from `direct_sum`. The API of `direct_sum` is deliberately unchanged in this PR.