internlm/Lean-Github huggingface dataset:
Theorem: image_null_of_C1_of_null
Proof 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
Proof state after:
no goals
Theorem: image_null_of_C1_of_null
Proof 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
Proof state after:
no goals
Theorem: image_null_of_C1_of_null
Proof 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
Proof 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
Theorem: image_null_of_C1_of_null
Proof 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
Proof state after:
no goals
Theorem: image_null_of_C1_of_null'
Proof 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
hf : ContDiff ℝ 1 f
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
hs : ↑μ s = 0
⊢ ↑ν (f '' s) = 0
Tactic:
let hdiff := Iff.mpr contDiffOn_univ hf
Proof 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
hf : ContDiff ℝ 1 f
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
hs : ↑μ s = 0
hdiff : ContDiffOn ℝ 1 f univ := contDiffOn_univ.mpr hf
⊢ ↑ν (f '' s) = 0
Theorem: image_null_of_C1_of_null'
Proof 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
hf : ContDiff ℝ 1 f
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
hs : ↑μ s = 0
hdiff : ContDiffOn ℝ 1 f univ := contDiffOn_univ.mpr hf
⊢ ↑ν (f '' s) = 0
Tactic:
apply image_null_of_C1_of_null isOpen_univ hdiff μ ν hd (subset_univ s) hs
Proof state after:
no goals
Theorem: image_measure_zero_of_C1_dimension_increase
Proof 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
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
⊢ ↑ν (g '' U) = 0
Tactic:
let incl : E → E × (Fin (n-m) → ℝ) := fun x ↦ ⟨x, 0⟩
Proof 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
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
⊢ ↑ν (g '' U) = 0
Theorem: image_measure_zero_of_C1_dimension_increase
Proof 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
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
⊢ ↑ν (g '' U) = 0
Tactic:
let g' : E × (Fin (n-m) → ℝ) → F × (Fin (n-m) → ℝ) := fun ⟨y, _⟩ ↦ ⟨g y, 0⟩
Proof 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
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
g' : E × (Fin (n - m) → ℝ) → F × (Fin (n - m) → ℝ) :=
  fun x =>
    match x with
    | (y, snd) => (g y, 0)
⊢ ↑ν (g '' U) = 0
Theorem: image_measure_zero_of_C1_dimension_increase
Proof 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
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
g' : E × (Fin (n - m) → ℝ) → F × (Fin (n - m) → ℝ) :=
  fun x =>
    match x with
    | (y, snd) => (g y, 0)
⊢ ↑ν (g '' U) = 0
Tactic:
let pi : F × (Fin (n-m) → ℝ) → F := fun ⟨f, _⟩ ↦ f
Proof 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
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
g' : E × (Fin (n - m) → ℝ) → F × (Fin (n - m) → ℝ) :=
  fun x =>
    match x with
    | (y, snd) => (g y, 0)
pi : F × (Fin (n - m) → ℝ) → F :=
  fun x =>
    match x with
    | (f, snd) => f
⊢ ↑ν (g '' U) = 0
Theorem: image_measure_zero_of_C1_dimension_increase
Proof 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
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
g' : E × (Fin (n - m) → ℝ) → F × (Fin (n - m) → ℝ) :=
  fun x =>
    match x with
    | (y, snd) => (g y, 0)
pi : F × (Fin (n - m) → ℝ) → F :=
  fun x =>
    match x with
    | (f, snd) => f
⊢ ↑ν (g '' U) = 0
Tactic:
have commutes: pi ∘ g' ∘ incl = g := by
   ext y
   rw [comp_apply, comp_apply]
Proof 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
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
g' : E × (Fin (n - m) → ℝ) → F × (Fin (n - m) → ℝ) :=
  fun x =>
    match x with
    | (y, snd) => (g y, 0)
pi : F × (Fin (n - m) → ℝ) → F :=
  fun x =>
    match x with
    | (f, snd) => f
commutes : pi ∘ g' ∘ incl = g
⊢ ↑ν (g '' U) = 0
Theorem: image_measure_zero_of_C1_dimension_increase
Proof 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
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
g' : E × (Fin (n - m) → ℝ) → F × (Fin (n - m) → ℝ) :=
  fun x =>
    match x with
    | (y, snd) => (g y, 0)
pi : F × (Fin (n - m) → ℝ) → F :=
  fun x =>
    match x with
    | (f, snd) => f
commutes : pi ∘ g' ∘ incl = g
⊢ ↑ν (g '' U) = 0
Tactic:
obtain ⟨K''⟩ : Nonempty (PositiveCompacts (E × (Fin (n-m) → ℝ))) := PositiveCompacts.nonempty'
Proof state after:
case intro
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
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
g' : E × (Fin (n - m) → ℝ) → F × (Fin (n - m) → ℝ) :=
  fun x =>
    match x with
    | (y, snd) => (g y, 0)
pi : F × (Fin (n - m) → ℝ) → F :=
  fun x =>
    match x with
    | (f, snd) => f
commutes : pi ∘ g' ∘ incl = g
K'' : PositiveCompacts (E × (Fin (n - m) → ℝ))
⊢ ↑ν (g '' U) = 0
Theorem: image_measure_zero_of_C1_dimension_increase
Proof state before:
case intro
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
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
g' : E × (Fin (n - m) → ℝ) → F × (Fin (n - m) → ℝ) :=
  fun x =>
    match x with
    | (y, snd) => (g y, 0)
pi : F × (Fin (n - m) → ℝ) → F :=
  fun x =>
    match x with
    | (f, snd) => f
commutes : pi ∘ g' ∘ incl = g
K'' : PositiveCompacts (E × (Fin (n - m) → ℝ))
⊢ ↑ν (g '' U) = 0
Tactic:
let μ' : Measure (E × (Fin (n-m) → ℝ)) := addHaarMeasure K''
Proof state after:
case intro
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
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
g' : E × (Fin (n - m) → ℝ) → F × (Fin (n - m) → ℝ) :=
  fun x =>
    match x with
    | (y, snd) => (g y, 0)
pi : F × (Fin (n - m) → ℝ) → F :=
  fun x =>
    match x with
    | (f, snd) => f
commutes : pi ∘ g' ∘ incl = g
K'' : PositiveCompacts (E × (Fin (n - m) → ℝ))
μ' : Measure (E × (Fin (n - m) → ℝ)) := addHaarMeasure K''
⊢ ↑ν (g '' U) = 0