mathlib3

63f2525e - chore(data/finset/pi_induction): fix lint (#16224)