https://leanprover-community.github.io/mathlib_docs/tactic/delta_instance.html#tactic.delta_instance_handler
In lean3 there was a default derive handler which would run delta on the goal. That is, it would pull the instance through the type synonym. We don't have this at present in lean4, so it is necessary to construct the instance by hand.

Examples:

deriving instance LargeCategory, ConcreteCategory for HeytAlgCat

turns into

deriving instance LargeCategory for HeytAlgCat

instance : ConcreteCategory HeytAlgCat := by
  dsimp [HeytAlgCat]
  infer_instance