mathlib

6c6597fa - chore(category_theory/concrete_category): remove imports (#17093)

chore(category_theory/concrete_category): remove imports (#17093) Remove unneeded imports. This had resulted in someone incorrectly thinking that it was block for porting to mathlib4, so may as well clean up. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>