mathlib

b395a671 - chore(data/finsupp/pointwise): golf using injective lemmas (#12086)