Commit 2026-09-17 11:05 06d0b85b
View on Github →chore(CategoryTheory): mark bi- and trifunctor constructions implicit_reducible (#43865)
Marks the bi- and trifunctor constructions and their localization lifts as implicit_reducible. Generates the four trifunctor currying map lemmas with simps!, preserving their names and allowing dsimp to use them without compatibility options.