Theorem: MeasureZero.empty (Sard/MeasureZero.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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ MeasureZero I ∅
Tactic:
intro μ _ x
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✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : M
⊢ ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ ∅)) = 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✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : M
⊢ ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ ∅)) = 0
Tactic:
simp only [comp_apply, inter_empty, image_empty, OuterMeasure.empty']
State after:
no goals