mathlib

654bbd9c - chore(data/finsupp/basic): golf a lemma (#17366)