mathlib3

0afd3a0f - chore(data/finsupp/basic): Add single_of_single_apply (#5219)