Commit 2026-06-24 10:57 6e988082

View on Github →

chore(CategoryTheory/LiftingProperties/Basic): use to_dual more (#40943) This PR finishes using to_dual in LiftingProperties/Basic, finishing the work in #38174. Some missing prerequisites have also been tagged, in particular Retract.

Estimated changes

Modified Mathlib/CategoryTheory/Balanced.lean

Modified Mathlib/CategoryTheory/Comma/Arrow.lean

Modified Mathlib/CategoryTheory/LiftingProperties/Basic.lean

deleted theorem CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_right

deleted theorem CategoryTheory.HasLiftingProperty.of_arrow_iso_right

deleted theorem CategoryTheory.RetractArrow.leftLiftingProperty

Modified Mathlib/CategoryTheory/Retract.lean

modified def CategoryTheory.Retract.splitEpi

deleted def CategoryTheory.Retract.splitMono

deleted theorem CategoryTheory.RetractArrow.retract_right

deleted def CategoryTheory.RetractArrow.right