Theorem: sard_local (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
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
⊢ ↑μ (f '' s) = 0
Tactic:
by_cases hyp: m < n
State after:
case pos
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
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
hyp : m < n
⊢ ↑μ (f '' s) = 0

case neg
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
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
hyp : ¬m < n
⊢ ↑μ (f '' s) = 0

State before:
case pos
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
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
hyp : m < n
⊢ ↑μ (f '' s) = 0
Tactic:
have hr : 1 ≤ (r : ℕ∞) := Nat.one_le_cast.mpr (Nat.one_le_of_lt hr)
State after:
case pos
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
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
hyp : m < n
hr : 1 ≤ ↑r
⊢ ↑μ (f '' s) = 0

State before:
case pos
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
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
hyp : m < n
hr : 1 ≤ ↑r
⊢ ↑μ (f '' s) = 0
Tactic:
have hless: μ (f '' s) ≤ 0 := calc
  μ (f '' s)
  _ ≤ μ (f '' w) := measure_mono (image_subset f hsw)
  _ = 0 := image_measure_zero_of_C1_dimension_increase' hw μ (hf.of_le hr) hyp
State after:
case pos
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
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
hyp : m < n
hr : 1 ≤ ↑r
hless : ↑μ (f '' s) ≤ 0
⊢ ↑μ (f '' s) = 0

State before:
case pos
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
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
hyp : m < n
hr : 1 ≤ ↑r
hless : ↑μ (f '' s) ≤ 0
⊢ ↑μ (f '' s) = 0
Tactic:
simp only [nonpos_iff_eq_zero, zero_le] at hless ⊢
State after:
case pos
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
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
hyp : m < n
hr : 1 ≤ ↑r
hless : ↑μ (f '' s) = 0
⊢ ↑μ (f '' s) = 0

State before:
case pos
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
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
hyp : m < n
hr : 1 ≤ ↑r
hless : ↑μ (f '' s) = 0
⊢ ↑μ (f '' s) = 0
Tactic:
exact hless
State after:
no goals

State before:
case neg
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
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
hyp : ¬m < n
⊢ ↑μ (f '' s) = 0
Tactic:
sorry
State after:
no goals