chore: add unification hint for forgetful functor Bundled -> Type

[Vierkantor]

We have a lot of erws and rfls in files dealing with concrete categories. This seems to be mostly due to the existence of two casts: ConcreteCategory.hasCoeToSort and Bundled.coeSort which both represent the forgetful functor from concrete categories to Type. The first is only a local instance but is needed to state lemmas on these concrete categories, while the second one is always available but only applies to categories defined as Bundled. The casts are defeq but not reducibly so, causing issues when rewriting with generic lemmas in the context of a specific Bundled category.

For some specific categories we already have a workaround: a unification hint of the form ⊢ (forget CommRingCat).obj R ≟ R also fires at reducible transparency. This PR does the same for any category of the form Bundled _, fixing a lot of the issues.

Still, we have some regressions. These all seem to happen because the subtle unification order gets disrupted: where we expected CommRingCat (with many useful instances) now we get Bundled CommRing. The many improvements still weigh up to this drawback, and perhaps we can figure out how to get rid of the regressions altogether.

---

[github-actions]

PR summary 1b0e66693b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[Vierkantor]

So there is a bit of regression in the area of sheaves, most of which is easy enough to fix. But most definitions in Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated seem to just completely fail because their expected CommRingCat becomes Bundled CommRing, meaning all their nice instances are gone. Adding type ascriptions doesn't seem to help, so I'm going to try and see if the issue can be resolved a bit higher up...