Commit 2025-09-06 06:21 e71ae4c6

View on Github →

chore(CategoryTheory): golf entire preinclusion_map₂, mapForget_eq, uSwitch_map_uSwitch_map and more using rfl (#28559)

Estimated changes

Modified Mathlib/CategoryTheory/Bicategory/Coherence.lean

Modified Mathlib/CategoryTheory/Comma/Over/Basic.lean

Modified Mathlib/CategoryTheory/FintypeCat.lean

Modified Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Basic.lean

Modified Mathlib/CategoryTheory/Pi/Basic.lean

modified theorem CategoryTheory.Functor.pi'_eval

Modified Mathlib/CategoryTheory/Quotient.lean