mathlib3

c9fca154 - chore(algebra/category): remove some [reducible] after Lean 3.8 (#2389)

chore(algebra/category): remove some [reducible] after Lean 3.8 (#2389) Now that Lean 3.8 has arrived, we can essentially revert #2290, but leave in the examples verifying that everything still works. Lovely!