Theorem: image_measure_zero_of_C1_dimension_increase (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
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⟩
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

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⟩
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

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
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

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]
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

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'
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

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''
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

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) → ℝ))
μ' : Measure (E × (Fin (n - m) → ℝ)) := addHaarMeasure K''
⊢ ↑ν (g '' U) = 0
Tactic:
have aux : μ' (incl '' U) = 0 := by sorry
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''
aux : ↑μ' (incl '' U) = 0
⊢ ↑ν (g '' U) = 0

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) → ℝ))
μ' : Measure (E × (Fin (n - m) → ℝ)) := addHaarMeasure K''
aux : ↑μ' (incl '' U) = 0
⊢ ↑ν (g '' U) = 0
Tactic:
have : ν ((pi ∘ g' ∘ incl) '' U) = 0 := by
  sorry
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''
aux : ↑μ' (incl '' U) = 0
this : ↑ν (pi ∘ g' ∘ incl '' U) = 0
⊢ ↑ν (g '' U) = 0

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) → ℝ))
μ' : Measure (E × (Fin (n - m) → ℝ)) := addHaarMeasure K''
aux : ↑μ' (incl '' U) = 0
this : ↑ν (pi ∘ g' ∘ incl '' U) = 0
⊢ ↑ν (g '' U) = 0
Tactic:
rw [← commutes]
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''
aux : ↑μ' (incl '' U) = 0
this : ↑ν (pi ∘ g' ∘ incl '' U) = 0
⊢ ↑ν (pi ∘ g' ∘ incl '' U) = 0

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) → ℝ))
μ' : Measure (E × (Fin (n - m) → ℝ)) := addHaarMeasure K''
aux : ↑μ' (incl '' U) = 0
this : ↑ν (pi ∘ g' ∘ incl '' U) = 0
⊢ ↑ν (pi ∘ g' ∘ incl '' U) = 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
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
⊢ pi ∘ g' ∘ incl = g
Tactic:
ext y
State after:
case h
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
y : E
⊢ (pi ∘ g' ∘ incl) y = g y

State before:
case h
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
y : E
⊢ (pi ∘ g' ∘ incl) y = g y
Tactic:
rw [comp_apply, comp_apply]
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
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''
⊢ ↑μ' (incl '' U) = 0
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
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''
aux : ↑μ' (incl '' U) = 0
⊢ ↑ν (pi ∘ g' ∘ incl '' U) = 0
Tactic:
sorry
State after:
no goals