mathlib

d2b46abb - chore(category_theory/punit): use discrete punit instead of punit (#3201)

chore(category_theory/punit): use discrete punit instead of punit (#3201) Analogous to #3191 for `punit`. I also removed some `simp` lemmas which can be generated instead by `[simps]`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>