mathlib

77821571 - 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 <39908973+MantasBaksys@users.noreply.github.com> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>