mathlib

8b4628e4 - feat(data/fintype/basic): induction principle for finite types (#8158)

feat(data/fintype/basic): induction principle for finite types (#8158) This lets us prove things about finite types by induction, analogously to proving things about natural numbers by induction. Here `pempty` plays the role of `0` and `option` plays the role of `nat.succ`. We need an extra hypothesis that our statement is invariant under equivalence of types. Used in #8019.