Theorem: MeasureZero.open_implies_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
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
⊢ s = ∅
Tactic:
suffices ∀ x : M, ((chartAt H x).source ∩ s) = ∅ by
  by_contra h
  obtain ⟨x, hx⟩ : Set.Nonempty s := Iff.mp nmem_singleton_empty h
  specialize this x
  have h₂: x ∈ (chartAt H x).toPartialEquiv.source ∩ s := by
    simp
    exact hx
  rw [this] at h₂
  contradiction
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
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
⊢ ∀ (x : M), (chartAt H x).source ∩ s = ∅

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
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
⊢ ∀ (x : M), (chartAt H x).source ∩ s = ∅
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
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
x : M
⊢ (chartAt H x).source ∩ s = ∅

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
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
x : M
⊢ (chartAt H x).source ∩ s = ∅
Tactic:
let e := chartAt H 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
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
x : M
e : PartialHomeomorph M H := chartAt H x
⊢ (chartAt H x).source ∩ s = ∅

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
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
x : M
e : PartialHomeomorph M H := chartAt H x
⊢ (chartAt H x).source ∩ s = ∅
Tactic:
obtain ⟨K''⟩ : Nonempty (PositiveCompacts E) := 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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
⊢ (chartAt H x).source ∩ s = ∅

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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
⊢ (chartAt H x).source ∩ s = ∅
Tactic:
let μ : Measure E := 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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
⊢ (chartAt H x).source ∩ s = ∅

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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
⊢ (chartAt H x).source ∩ s = ∅
Tactic:
specialize h₂s μ x
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
⊢ (chartAt H x).source ∩ s = ∅

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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
⊢ (chartAt H x).source ∩ s = ∅
Tactic:
by_contra h
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
h : ¬(chartAt H x).source ∩ s = ∅
⊢ False

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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
h : ¬(chartAt H x).source ∩ s = ∅
⊢ False
Tactic:
have h' : Set.Nonempty (interior (I ∘ e '' (e.source ∩ s))) := by
  have : Set.Nonempty (I ∘ e '' (e.source ∩ s)) := (Iff.mp Set.nmem_singleton_empty h).image _
  have : IsOpen (I ∘ e '' (e.source ∩ s)) := by
    rw [Set.image_comp]
    exact I.toHomeomorph.isOpenMap _ (e.isOpen_image_source_inter h₁s)
  rwa [this.interior_eq]
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
h : ¬(chartAt H x).source ∩ s = ∅
h' : (interior (↑I ∘ ↑e '' (e.source ∩ s))).Nonempty
⊢ False

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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
h : ¬(chartAt H x).source ∩ s = ∅
h' : (interior (↑I ∘ ↑e '' (e.source ∩ s))).Nonempty
⊢ False
Tactic:
exact (measure_pos_of_nonempty_interior (μ := μ) h').ne' h₂s
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
this : ∀ (x : M), (chartAt H x).source ∩ s = ∅
⊢ s = ∅
Tactic:
by_contra h
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
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
this : ∀ (x : M), (chartAt H x).source ∩ s = ∅
h : ¬s = ∅
⊢ False

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
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
this : ∀ (x : M), (chartAt H x).source ∩ s = ∅
h : ¬s = ∅
⊢ False
Tactic:
obtain ⟨x, hx⟩ : Set.Nonempty s := Iff.mp nmem_singleton_empty h
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
this : ∀ (x : M), (chartAt H x).source ∩ s = ∅
h : ¬s = ∅
x : M
hx : x ∈ s
⊢ False

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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
this : ∀ (x : M), (chartAt H x).source ∩ s = ∅
h : ¬s = ∅
x : M
hx : x ∈ s
⊢ False
Tactic:
specialize this x
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
h : ¬s = ∅
x : M
hx : x ∈ s
this : (chartAt H x).source ∩ s = ∅
⊢ False

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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
h : ¬s = ∅
x : M
hx : x ∈ s
this : (chartAt H x).source ∩ s = ∅
⊢ False
Tactic:
have h₂: x ∈ (chartAt H x).toPartialEquiv.source ∩ s := by
  simp
  exact hx
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
h : ¬s = ∅
x : M
hx : x ∈ s
this : (chartAt H x).source ∩ s = ∅
h₂ : x ∈ (chartAt H x).source ∩ s
⊢ False

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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
h : ¬s = ∅
x : M
hx : x ∈ s
this : (chartAt H x).source ∩ s = ∅
h₂ : x ∈ (chartAt H x).source ∩ s
⊢ False
Tactic:
rw [this] at h₂
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
h : ¬s = ∅
x : M
hx : x ∈ s
this : (chartAt H x).source ∩ s = ∅
h₂ : x ∈ ∅
⊢ False

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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
h : ¬s = ∅
x : M
hx : x ∈ s
this : (chartAt H x).source ∩ s = ∅
h₂ : x ∈ ∅
⊢ False
Tactic:
contradiction
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
h : ¬s = ∅
x : M
hx : x ∈ s
this : (chartAt H x).source ∩ s = ∅
⊢ x ∈ (chartAt H x).source ∩ s
Tactic:
simp
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
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
h : ¬s = ∅
x : M
hx : x ∈ s
this : (chartAt H x).source ∩ s = ∅
⊢ x ∈ s

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
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
h : ¬s = ∅
x : M
hx : x ∈ s
this : (chartAt H x).source ∩ s = ∅
⊢ x ∈ s
Tactic:
exact hx
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
h : ¬(chartAt H x).source ∩ s = ∅
⊢ (interior (↑I ∘ ↑e '' (e.source ∩ s))).Nonempty
Tactic:
have : Set.Nonempty (I ∘ e '' (e.source ∩ s)) := (Iff.mp Set.nmem_singleton_empty h).image _
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
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
h : ¬(chartAt H x).source ∩ s = ∅
this : (↑I ∘ ↑e '' (e.source ∩ s)).Nonempty
⊢ (interior (↑I ∘ ↑e '' (e.source ∩ s))).Nonempty

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
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
h : ¬(chartAt H x).source ∩ s = ∅
this : (↑I ∘ ↑e '' (e.source ∩ s)).Nonempty
⊢ (interior (↑I ∘ ↑e '' (e.source ∩ s))).Nonempty
Tactic:
have : IsOpen (I ∘ e '' (e.source ∩ s)) := by
  rw [Set.image_comp]
  exact I.toHomeomorph.isOpenMap _ (e.isOpen_image_source_inter 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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
h : ¬(chartAt H x).source ∩ s = ∅
this✝ : (↑I ∘ ↑e '' (e.source ∩ s)).Nonempty
this : IsOpen (↑I ∘ ↑e '' (e.source ∩ s))
⊢ (interior (↑I ∘ ↑e '' (e.source ∩ s))).Nonempty

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
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
h : ¬(chartAt H x).source ∩ s = ∅
this✝ : (↑I ∘ ↑e '' (e.source ∩ s)).Nonempty
this : IsOpen (↑I ∘ ↑e '' (e.source ∩ s))
⊢ (interior (↑I ∘ ↑e '' (e.source ∩ s))).Nonempty
Tactic:
rwa [this.interior_eq]
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
h : ¬(chartAt H x).source ∩ s = ∅
this : (↑I ∘ ↑e '' (e.source ∩ s)).Nonempty
⊢ IsOpen (↑I ∘ ↑e '' (e.source ∩ s))
Tactic:
rw [Set.image_comp]
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
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
h : ¬(chartAt H x).source ∩ s = ∅
this : (↑I ∘ ↑e '' (e.source ∩ s)).Nonempty
⊢ IsOpen (↑I '' (↑e '' (e.source ∩ s)))

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
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
h : ¬(chartAt H x).source ∩ s = ∅
this : (↑I ∘ ↑e '' (e.source ∩ s)).Nonempty
⊢ IsOpen (↑I '' (↑e '' (e.source ∩ s)))
Tactic:
exact I.toHomeomorph.isOpenMap _ (e.isOpen_image_source_inter h₁s)
State after:
no goals