Commit 2025-01-17 18:04 383fdb64

feat(Tactic): basic ConcreteCategory support for elementwise (#20811) This is a step towards a concrete category redesign, as outlined in this Zulip post: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Concrete.20category.20class.20redesign/near/493903980 This PR adds basic support for ConcreteCategory to the elementwise attribute and elaborator: it still uses HasForget when a fresh instance is needed, but now will replace the forget-based operations with ConcreteCategory-based ones. So as long as there is only a HasForget instance, or no instance at all, in scope, elementwise will behave the same. But when there is a ConcreteCategory instance, all the (forget C).obj Xes turn into ToType X and (forget C).map fs turn into hom f. In the future, when we have replaced enough HasForget instances with ConcreteCategory, we can apply the changes from the branch redesign-ConcreteCategory to make elementwise use ConcreteCategory when it creates fresh instances.