mathlib

e2b33abb - refactor(data/fintype/basic): simplify the defeq of `sum.fintype` (#17236)

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`