feat (data/finset/lattice): add more finset induction lemmas (#10889)
feat (data/finset/lattice): add more finset induction lemmas (#10889)

2 more finset induction lemmas based on the order imposed by a function.



Co-authored-by: Mantas Bakšys <70b74b8dfe3b61f2ae3017d529744bafb6de8b29@users.noreply.github.com>
Co-authored-by: Rob Lewis <f89db59e6074667375662ee222555a187f42739f@gmail.com>
Co-authored-by: Eric Wieser <da64e90baec5d084ce3d8e05f3b022ae6d118ff5@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib