Commit 2025-02-09 15:10 a04abe9b

refactor(CategoryTheory/Sites,Topology/Sheaves): upgrade HasForget to ConcreteCategory (#21575) This PR goes through all the files in CategoryTheory/Sites and Topology/Sheaves and replaces HasForget with ConcreteCategory so that we don't need to worry about HasForget.instFunLike or HasForget.hasCoeToSort mismatching with the actual coercions to functions/types. Some sources of friction remain: Type is not (globally) a ConcreteCategory, since to make it so needs to break the assumption that forget Type is reducibly defeq to the identity functor. The solution of this PR is to copy instances such as PreservesLimits (forget Type) over from the identity functor, and enabling the ConcreteCategory instance locally (see CategoryTheory/Limits/ConcreteCategory/Basic.lean). In the longer term I think we can enable that instance globally, but it would require quite some more downstream fixes. Limits are still based on HasForget, so we have to insert some show and rfl to change the goal from one spelling to another. Similarly for elementwise-generated lemmas. This should go away once we update the rest of the files to the same standards. Despite those uglifications mentioned above, I think the overall result is a clear improvement.