chore(category_theory/*): reduce imports (#13305)
An unnecessary import of `tactic.monotonicity` earlier in the hierarchy was pulling in quite a lot. A few compensatory imports are needed later.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
