Commit 2025-09-06 21:16 6d82afcd

View on Github →

feat(Logic/Equiv/Defs): Equiv.trans_cancel_left / right (#29229) Given an equation e.trans f = g, lets you move either e or f over to the rhs with a rewrite.

Estimated changes

Modified Mathlib/Logic/Equiv/Defs.lean

modified theorem Equiv.leftInverse_symm

modified theorem Equiv.rightInverse_symm

added theorem Equiv.trans_cancel_left

added theorem Equiv.trans_cancel_right