mathlib

fb948808 - refactor(category_theory/shift): tighten scope of local attribute [reducible] (#13335)

refactor(category_theory/shift): tighten scope of local attribute [reducible] (#13335) In all the files dealing with shifts on categories, we have a sprinkling of `local attribute [reducible]`, without which we get somewhat mysterious errors. However with them, we produce some very fragile proof states (recently I was upset to see that shifting by `(0 : A)` and shifting by the tensor unit in `discrete A` were not definitionally commuting...). I've been attempting to refactor this part of the library so we just never need to use `local attribute [reducible]`, in the hope of making these problems go away. Having failed so far, this PR simply tightens the scopes of these local attributes as narrowly as possible (or in cases removes them entirely), so it is clearer exactly what is relying on them to work. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>