internlm/Lean-Github huggingface dataset:
Theorem: MeasureZero.iUnion
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✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
ι : Type u_4
inst✝ : Encodable ι
s : ι → Set M
hs : ∀ (n : ι), MeasureZero I (s n)
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
e : PartialHomeomorph M H := chartAt H x
⊢ ↑I ∘ ↑e '' (e.source ∩ ⋃ n, s n) = ⋃ n, ↑I ∘ ↑e '' (e.source ∩ s n)
Tactic:
rw [inter_iUnion]
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✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
ι : Type u_4
inst✝ : Encodable ι
s : ι → Set M
hs : ∀ (n : ι), MeasureZero I (s n)
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
e : PartialHomeomorph M H := chartAt H x
⊢ ↑I ∘ ↑e '' ⋃ i, e.source ∩ s i = ⋃ n, ↑I ∘ ↑e '' (e.source ∩ s n)
Theorem: MeasureZero.iUnion
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✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
ι : Type u_4
inst✝ : Encodable ι
s : ι → Set M
hs : ∀ (n : ι), MeasureZero I (s n)
μ : Measure E
hμ : μ.IsAddHaarMeasure
x : M
e : PartialHomeomorph M H := chartAt H x
⊢ ↑I ∘ ↑e '' ⋃ i, e.source ∩ s i = ⋃ n, ↑I ∘ ↑e '' (e.source ∩ s n)
Tactic:
exact image_iUnion
Proof state after:
no goals
Theorem: MeasureZero.union
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s t : Set M
hs : MeasureZero I s
ht : MeasureZero I t
⊢ MeasureZero I (s ∪ t)
Tactic:
let u : Bool → Set M := fun b ↦ cond b s t
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s t : Set M
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
⊢ MeasureZero I (s ∪ t)
Theorem: MeasureZero.union
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s t : Set M
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
this : ∀ (i : Bool), MeasureZero I (u i)
⊢ MeasureZero I (s ∪ t)
Tactic:
rw [union_eq_iUnion]
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s t : Set M
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
this : ∀ (i : Bool), MeasureZero I (u i)
⊢ MeasureZero I (⋃ b, bif b then s else t)
Theorem: MeasureZero.union
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s t : Set M
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
this : ∀ (i : Bool), MeasureZero I (u i)
⊢ MeasureZero I (⋃ b, bif b then s else t)
Tactic:
exact MeasureZero.iUnion this
Proof state after:
no goals
Theorem: MeasureZero.union
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s t : Set M
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
⊢ ∀ (i : Bool), MeasureZero I (u i)
Tactic:
intro i
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s t : Set M
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
i : Bool
⊢ MeasureZero I (u i)
Theorem: MeasureZero.union
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s t : Set M
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
i : Bool
⊢ MeasureZero I (u i)
Tactic:
cases i
Proof state after:
case false
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 t : Set M
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
⊢ MeasureZero I (u false)

case true
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 t : Set M
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
⊢ MeasureZero I (u true)
Theorem: MeasureZero.union
Proof state before:
case false
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 t : Set M
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
⊢ MeasureZero I (u false)
Tactic:
exact ht
Proof state after:
no goals
Theorem: MeasureZero.union
Proof state before:
case true
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 t : Set M
hs : MeasureZero I s
ht : MeasureZero I t
u : Bool → Set M := fun b => bif b then s else t
⊢ MeasureZero I (u true)
Tactic:
exact hs
Proof state after:
no goals
Theorem: MeasureZero.open_implies_empty
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✝² : 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
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✝² : 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 = ∅
Theorem: MeasureZero.open_implies_empty
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✝² : 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
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✝² : 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 = ∅
Theorem: MeasureZero.open_implies_empty
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✝² : 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
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✝² : 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 = ∅
Theorem: MeasureZero.open_implies_empty
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✝² : 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'
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✝² : 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 = ∅
Theorem: MeasureZero.open_implies_empty
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✝² : 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''
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✝² : 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 = ∅
Theorem: MeasureZero.open_implies_empty
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✝² : 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
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✝² : 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 = ∅
Theorem: MeasureZero.open_implies_empty
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✝² : 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
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✝² : 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
Theorem: MeasureZero.open_implies_empty
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✝² : 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]
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✝² : 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
Theorem: MeasureZero.open_implies_empty
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✝² : 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
Proof state after:
no goals
Theorem: MeasureZero.open_implies_empty
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✝² : 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
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✝² : 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
Theorem: MeasureZero.open_implies_empty
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✝² : 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
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✝² : 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
Theorem: MeasureZero.open_implies_empty
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✝² : 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
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✝² : 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
Theorem: MeasureZero.open_implies_empty
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✝² : 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
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✝² : 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
Theorem: MeasureZero.open_implies_empty
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✝² : 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₂
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✝² : 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
Theorem: MeasureZero.open_implies_empty
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✝² : 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
Proof state after:
no goals
Theorem: MeasureZero.open_implies_empty
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✝² : 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
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✝² : 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