Commit 2023-08-01 07:19 358bd33b

feat: factorization through full subcategories is definitional (#6184) In Lean 3, the equality FullSubcategory.lift P F hF ⋙ fullSubcategoryInclusion P = F was evil because it was not definitional (though it was definitional on objects and maps). In Lean 4, it is definitional, so it should be fine to tell this to dsimp.