mathlib3

322ccc54 - feat(finset/basic): downward induction for finsets (#7379)