Commit 2025-02-12 15:26 c54f94ff

refactor(*): get rid of (forget _).obj and (forget _).map (#21727) This PR tries getting rid of HasForget.forget by searching for \(forget .*\).(obj|map) and removing all the occurrences where they could become ConcreteCategory.hom. In particular, they should no longer be written in any theorem statement. There are still a few places, generally in the middle of proving properties of the forgetful functor itself, where it was nicer to keep HasForget. The final step is to modify the elementwise attribute to produce ConcreteCategory lemmas, and the refactor itself is done. After that point, we should still go through and try to clean up the workarounds left behind. But that can be done at a lower priority.