Commit 2025-08-27 19:15 71e57acb

View on Github →

chore(CategoryTheory): process remaining porting notes for CategoryTheory (#28782) Thiis should cover all the remaining easy to deal with porting notes for CategoryTheory. Most of those that were not easily fixed are about Lean 4 being stricter about defeq, which is not going to change. The most important sources of remaining porting notes in CategoryTheory are ext not firing (due to defeq issues), and congr not firing (due to reasons I don't know).

Estimated changes