Theorem: sard (Sard/MainTheorem.lean)

State before:
E : Type u_1
inst✝¹⁸ : NormedAddCommGroup E
inst✝¹⁷ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : ChartedSpace H M
inst✝¹³ : SmoothManifoldWithCorners I M
inst✝¹² : FiniteDimensional ℝ E
inst✝¹¹ : SecondCountableTopology M
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
F : Type u_4
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
G : Type u_5
inst✝⁶ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁵ : TopologicalSpace N
inst✝⁴ : ChartedSpace G N
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
f' : (x : M) → TangentSpace I x →L[ℝ] TangentSpace J (f x)
s : Set M
hf' : ∀ x ∈ s, HasMFDerivAt I J f x (f' x)
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
⊢ MeasureZero J (f '' s)
Tactic:
sorry
State after:
no goals