Moreira's version of Sard's Theorem This project aims to formalize Moreira's version of Sard's Theorem.