mathlib

6610e8f5 - feat(data/fintype): golf, move and dualise proof (#7126)

feat(data/fintype): golf, move and dualise proof (#7126) This PR moves `fintype.exists_max` higher up in the import tree, and golfs it, and adds the dual version, `fintype.exists_min`. The name and statement are unchanged.