Proof of `Cancelling injective and surjective terms`
groundedproofs/Lax149335Proofs/Results/Preliminaries.lean · lax-149335
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Compose with the one-sided inverse and use the category axioms.