Commit 2022-10-31 12:47 e2b33abb

refactor(data/fintype/basic): simplify the defeq of sum.fintype (#17236) Using finset.disj_sum instead of finset.union removes a handful of proof obligations, and makes some results defeq. This removes the generalization on univ_sum_type that includes handling fintype.subsingleton, as it probably isn't useful; but the new version holds without decidable equality. This removes finset.prod_on_sum which is a duplicate of fintype.prod_sum_type