Theorem CategoryTheory.Limits.CatCospanTransform.id_whiskerLeft

Modification history

2025-08-05 23:45
Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/CatCospanTransform.lean
feat: replace aesop_cat with a configurable discharger (#27938) …
Modified CategoryTheory.Limits.CatCospanTransform.id_whiskerLeftView on Github →
2025-07-15 10:09
Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/CatCospanTransform.lean
feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): bicategory-like lemmas for `CatCospanTransforms` (#26447) …
Added CategoryTheory.Limits.CatCospanTransform.id_whiskerLeftView on Github →