While formalizing Dummit and Foote's Abstract Algebra in Rocq during my second week at the Recurse Center, I found the first proof exercise's goal false. The proposition claims a function is injective iff it has a left inverse. But a counterexample exists: let A be empty and B = {1}.

The empty function f: A -> B is vacuously injective, yet no function g: B -> A exists because B is nonempty and A is empty. This corner case is easy to miss on paper, but Rocq forced me to confront it. After struggling, I checked the book's errata and found it listed.

It was frustrating but exciting to discover independently.