mathlib

3974a774 - chore(category_theory/limits/preserves/finite): avoid instances with unbound universes (#18890)

chore(category_theory/limits/preserves/finite): avoid instances with unbound universes (#18890) There were some instances with unbounded universe variables, which Lean 4 couldn't cope with (reasonably!). This PR backports some changes made in https://github.com/leanprover-community/mathlib4/pull/3615 to remove these bad instances. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>