feat(data/finset/pi): pi singleton lemmas (#4558)
feat(data/finset/pi): pi singleton lemmas (#4558)

Broken off from #4259. 
Two lemmas to reduce `finset.pi` on singletons.



leanprover-community/mathlib,leanprover-community/mathlib