Towards the SardSmale theorem
In this repository, we work towards the proof of the MorseSard and SardSmale theorems.
MorseSard theorem. Let
The SardSmale theorem is a generalisation to infinitedimensional Banach manifolds. Stating it requires a theory of Fredholm operators. See a separate file for detail and a roadmap towards that.
Applications of Sard's theorem.
 stronger version of Whitney's approximation theorem
 proving Brouwer's fixed point theorem: there is no retraction
 needs smooth approximation during the proof; otherwise it just shows this for smooth retractions
 transversality theorem (the local part uses Sard's theorem)
 already the theorem statement requires defining the strong and weak
topologies > separate project  global part of the proof uses new ideas
 already the theorem statement requires defining the strong and weak
Status
This project was initiated during Lean for the Curious Mathematician 2023, mentored by @fpvandoorn and continued thereafter. A fair amount of groundwork is done, but significant parts of that remain (and the "hard part" of the proof hasn't been started yet). I'm pausing this project for now (except possibly upstreaming the parts which are complete to mathlib) since my Lean time is limited; I intend to return to and complete this project if possible.
That said, help is very welcome! Feel free to make a PR filling in some sorry, or working towards the proof of the "hard" case.
Necessary steps/work plan
 prerequisites

define locally Lipschitz maps; show C¹ maps are locally Lipschitz mostly PRed and merged

locally Lipschitz maps preserve null sets (done; mathlib mostly has this already)

nowhere dense and meagre sets: PRed and merged

compact subsets, relation to compact spaces and basic: PRed and merged 
compact measure zero sets are meagre: PRed 
finitedimensional manifolds are locally compact: PRed and merged

define measure zero subsets of a manifold: first version complete and PRed. Needs rework to a more conceptual approach:
 define Lebesgue measure on a C¹ manifold (pull back Lebesgue measure on each chart, use a partition of unity)
 redefine: a measure zero subset of a manifold is a null set w.r.t. one (or any) Lebesgue measure
 show welldefinedness: null sets are preserved by coordinate changes (see below)
 show:
has measure zero iff for each chart , the set is a null set  define the almost everywhere filter on a manifold, show it's a CountableIntersectionFilter
 show the ae filter is induced from the charts
 perhaps not all of these are truly required

 state Sard's theorem: formalised
 reduce to a local statement: essentially done (remaining sorries are busywork)
 "easy" case of Sard: if
: essentially done  "hard" case of Sard:
: open, not started yet  show
(in Hirsch's proof) has measure zero  inductive proof: base case is the previous bullet point
 show
has measure zero (similar argument)  remaining argument: induction proof, using a coordinate change and Fubini > need to work out the details
 show
 generalise to the Hausdorff dimension version
 followup/small extensions: handle manifolds with boundary; allow complex manifolds
File organisation

MainTheorem.lean
contains the statement of Sard's theorem and the reduction to the local case. 
ManifoldAux.lean
contains miscellaneous results about smooth manifolds and their charts, used for reducing Sard's theorem to the local case. 
MeasureZero.lean
contains the definition of measure zero subsets of a manifold (not reworked yet) and shows acompact measure zero set is meagre. 
LocallyLipschitz.lean
contains additional material on locally Lipschitz functions 
LocallyLipschitzMeasureZero.lean
shows that locally Lipschitz functions preserve measure zero sets. Not PRed yet; a few sorries remain. This is essentially in mathlib (though phrased differently). 
Stuff.lean
contains other results, which are superseded now. 
ObsoleteHelpers.lean
contains results I didn't need; perhaps one or two lemmas are useful for mathlib.