Theorem: image_null_of_C1_of_null (Sard/Stuff.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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
⊢ ↑ν (f '' s) = 0
Tactic:
have h₁ : μ = μH[m] := by
  have aux : μH[m] = volume := by
    rw [← Fintype.card_fin m]
    exact hausdorffMeasure_pi_real (ι := Fin m)
  sorry
State after:
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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
h₁ : μ = μH[↑m]
⊢ ↑ν (f '' s) = 0

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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
h₁ : μ = μH[↑m]
⊢ ↑ν (f '' s) = 0
Tactic:
have h₂ : ν = μH[n] := by sorry
State after:
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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
h₁ : μ = μH[↑m]
h₂ : ν = μH[↑n]
⊢ ↑ν (f '' s) = 0

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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
h₁ : μ = μH[↑m]
h₂ : ν = μH[↑n]
⊢ ↑ν (f '' s) = 0
Tactic:
rw [h₁] at h₂s
State after:
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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μH[↑m] s = 0
h₁ : μ = μH[↑m]
h₂ : ν = μH[↑n]
⊢ ↑ν (f '' s) = 0

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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μH[↑m] s = 0
h₁ : μ = μH[↑m]
h₂ : ν = μH[↑n]
⊢ ↑ν (f '' s) = 0
Tactic:
have : μH[m] (f '' s) = 0 := by
  have scifi : Convex ℝ U := sorry
  apply locally_lipschitz_image_of_null_set_is_null_set_open (of_C1_on_open hU scifi hf) h₁s h₂s
State after:
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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μH[↑m] s = 0
h₁ : μ = μH[↑m]
h₂ : ν = μH[↑n]
this : ↑μH[↑m] (f '' s) = 0
⊢ ↑ν (f '' s) = 0

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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μH[↑m] s = 0
h₁ : μ = μH[↑m]
h₂ : ν = μH[↑n]
this : ↑μH[↑m] (f '' s) = 0
⊢ ↑ν (f '' s) = 0
Tactic:
rw [h₂, ← hd]
State after:
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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μH[↑m] s = 0
h₁ : μ = μH[↑m]
h₂ : ν = μH[↑n]
this : ↑μH[↑m] (f '' s) = 0
⊢ ↑μH[↑m] (f '' s) = 0

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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μH[↑m] s = 0
h₁ : μ = μH[↑m]
h₂ : ν = μH[↑n]
this : ↑μH[↑m] (f '' s) = 0
⊢ ↑μH[↑m] (f '' s) = 0
Tactic:
exact this
State after:
no goals

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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
⊢ μ = μH[↑m]
Tactic:
have aux : μH[m] = volume := by
  rw [← Fintype.card_fin m]
  exact hausdorffMeasure_pi_real (ι := Fin m)
State after:
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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
aux : μH[↑m] = volume
⊢ μ = μH[↑m]

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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
aux : μH[↑m] = volume
⊢ μ = μH[↑m]
Tactic:
sorry
State after:
no goals

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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
⊢ μH[↑m] = volume
Tactic:
rw [← Fintype.card_fin m]
State after:
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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
⊢ μH[↑(Fintype.card (Fin m))] = volume

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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
⊢ Type ?u.6703

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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
⊢ MeasureSpace ?m.6704

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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
⊢ EMetricSpace ?m.6704

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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
⊢ BorelSpace ?m.6704

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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
⊢ μH[↑(Fintype.card (Fin m))] = volume

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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
⊢ Type ?u.6703

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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
⊢ MeasureSpace ?m.6704

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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
⊢ EMetricSpace ?m.6704

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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
⊢ BorelSpace ?m.6704
Tactic:
exact hausdorffMeasure_pi_real (ι := Fin m)
State after:
no goals

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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
h₁ : μ = μH[↑m]
⊢ ν = μH[↑n]
Tactic:
sorry
State after:
no goals

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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μH[↑m] s = 0
h₁ : μ = μH[↑m]
h₂ : ν = μH[↑n]
⊢ ↑μH[↑m] (f '' s) = 0
Tactic:
have scifi : Convex ℝ U := sorry
State after:
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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μH[↑m] s = 0
h₁ : μ = μH[↑m]
h₂ : ν = μH[↑n]
scifi : Convex ℝ U
⊢ ↑μH[↑m] (f '' s) = 0

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✝¹⁷ : I.Boundaryless
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✝⁶ : J.Boundaryless
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 : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μH[↑m] s = 0
h₁ : μ = μH[↑m]
h₂ : ν = μH[↑n]
scifi : Convex ℝ U
⊢ ↑μH[↑m] (f '' s) = 0
Tactic:
apply locally_lipschitz_image_of_null_set_is_null_set_open (of_C1_on_open hU scifi hf) h₁s h₂s
State after:
no goals