Theorem: measure_zero_image_iff_chart_domains (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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
⊢ MeasureZero J (f '' s)
Tactic:
let U : M → Set M := fun x ↦ (ChartedSpace.chartAt x : PartialHomeomorph M H).source
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
⊢ MeasureZero J (f '' 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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
⊢ MeasureZero J (f '' s)
Tactic:
have hcovering : univ ⊆ ⋃ (x : M), U x := by
  intro x _
  rw [mem_iUnion]
  exact ⟨x, mem_chart_source 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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
⊢ MeasureZero J (f '' 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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
⊢ MeasureZero J (f '' s)
Tactic:
have hopen : ∀ x : M, IsOpen (U x) := fun x => (ChartedSpace.chartAt x).open_source
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
⊢ MeasureZero J (f '' 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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
⊢ MeasureZero J (f '' s)
Tactic:
let ⟨T, ⟨hTCountable, hTcover⟩⟩ := TopologicalSpace.isOpen_iUnion_countable U hopen
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
⊢ MeasureZero J (f '' 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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
⊢ MeasureZero J (f '' s)
Tactic:
have : ∀ i : T, MeasureZero J (f '' ((U i) ∩ s)) := by
  intro i
  let e : PartialHomeomorph M H := ChartedSpace.chartAt i
  have h : MeasureZero J (f '' (e.source ∩ s)) := hs i
  have h₃ : U i = e.source := by rw [← Filter.principal_eq_iff_eq]
  apply h.mono _
  apply image_subset
  rw [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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
⊢ MeasureZero J (f '' 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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
⊢ MeasureZero J (f '' s)
Tactic:
have decomp : ⋃ (i : T), f '' ((U i) ∩ s) = f '' s :=
  calc ⋃ (i : T), f '' ((U i) ∩ s)
    _ = f '' (⋃ (i : T), (U i) ∩ s) := by rw [image_iUnion]
    _ = f '' ((⋃ (i : T), (U i)) ∩ s) := by rw [iUnion_inter]
    _ = f '' ((⋃ (i : M) (_ : i ∈ T), U i) ∩ s) := by rw [iUnion_coe_set]
    _ = f '' ((⋃ (i : M), U i) ∩ s) := by rw [hTcover]
    _ = f '' (univ ∩ s) := by rw [subset_antisymm (by simp) (hcovering)]
    _ = f '' s := by rw [univ_inter]
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
decomp : ⋃ i, f '' (U ↑i ∩ s) = f '' s
⊢ MeasureZero J (f '' 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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
decomp : ⋃ i, f '' (U ↑i ∩ s) = f '' s
⊢ MeasureZero J (f '' s)
Tactic:
rw [← decomp]
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
decomp : ⋃ i, f '' (U ↑i ∩ s) = f '' s
⊢ MeasureZero J (⋃ i, f '' (U ↑i ∩ 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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
decomp : ⋃ i, f '' (U ↑i ∩ s) = f '' s
⊢ MeasureZero J (⋃ i, f '' (U ↑i ∩ s))
Tactic:
have todo : Encodable T := by sorry
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
decomp : ⋃ i, f '' (U ↑i ∩ s) = f '' s
todo : Encodable ↑T
⊢ MeasureZero J (⋃ i, f '' (U ↑i ∩ 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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
decomp : ⋃ i, f '' (U ↑i ∩ s) = f '' s
todo : Encodable ↑T
⊢ MeasureZero J (⋃ i, f '' (U ↑i ∩ s))
Tactic:
apply MeasureZero.iUnion (ι := T) 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✝²⁰ : FiniteDimensional ℝ E✝
inst✝¹⁹ : MeasurableSpace E✝
inst✝¹⁸ : BorelSpace E✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
⊢ univ ⊆ ⋃ x, U x
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
x : M
a✝ : x ∈ univ
⊢ x ∈ ⋃ x, U x

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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
x : M
a✝ : x ∈ univ
⊢ x ∈ ⋃ x, U x
Tactic:
rw [mem_iUnion]
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
x : M
a✝ : x ∈ univ
⊢ ∃ i, x ∈ U i

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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
x : M
a✝ : x ∈ univ
⊢ ∃ i, x ∈ U i
Tactic:
exact ⟨x, mem_chart_source H x⟩
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
⊢ ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
Tactic:
intro i
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
i : ↑T
⊢ MeasureZero J (f '' (U ↑i ∩ 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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
i : ↑T
⊢ MeasureZero J (f '' (U ↑i ∩ s))
Tactic:
let e : PartialHomeomorph M H := ChartedSpace.chartAt i
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
i : ↑T
e : PartialHomeomorph M H := ChartedSpace.chartAt ↑i
⊢ MeasureZero J (f '' (U ↑i ∩ 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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
i : ↑T
e : PartialHomeomorph M H := ChartedSpace.chartAt ↑i
⊢ MeasureZero J (f '' (U ↑i ∩ s))
Tactic:
have h : MeasureZero J (f '' (e.source ∩ s)) := hs i
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
i : ↑T
e : PartialHomeomorph M H := ChartedSpace.chartAt ↑i
h : MeasureZero J (f '' (e.source ∩ s))
⊢ MeasureZero J (f '' (U ↑i ∩ 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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
i : ↑T
e : PartialHomeomorph M H := ChartedSpace.chartAt ↑i
h : MeasureZero J (f '' (e.source ∩ s))
⊢ MeasureZero J (f '' (U ↑i ∩ s))
Tactic:
have h₃ : U i = e.source := by rw [← Filter.principal_eq_iff_eq]
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
i : ↑T
e : PartialHomeomorph M H := ChartedSpace.chartAt ↑i
h : MeasureZero J (f '' (e.source ∩ s))
h₃ : U ↑i = e.source
⊢ MeasureZero J (f '' (U ↑i ∩ 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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
i : ↑T
e : PartialHomeomorph M H := ChartedSpace.chartAt ↑i
h : MeasureZero J (f '' (e.source ∩ s))
h₃ : U ↑i = e.source
⊢ MeasureZero J (f '' (U ↑i ∩ s))
Tactic:
apply h.mono _
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
i : ↑T
e : PartialHomeomorph M H := ChartedSpace.chartAt ↑i
h : MeasureZero J (f '' (e.source ∩ s))
h₃ : U ↑i = e.source
⊢ f '' (U ↑i ∩ s) ⊆ f '' (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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
i : ↑T
e : PartialHomeomorph M H := ChartedSpace.chartAt ↑i
h : MeasureZero J (f '' (e.source ∩ s))
h₃ : U ↑i = e.source
⊢ f '' (U ↑i ∩ s) ⊆ f '' (e.source ∩ s)
Tactic:
apply image_subset
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✝²⁰ : FiniteDimensional ℝ E✝
inst✝¹⁹ : MeasurableSpace E✝
inst✝¹⁸ : BorelSpace E✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
i : ↑T
e : PartialHomeomorph M H := ChartedSpace.chartAt ↑i
h : MeasureZero J (f '' (e.source ∩ s))
h₃ : U ↑i = e.source
⊢ U ↑i ∩ s ⊆ e.source ∩ s

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✝²⁰ : FiniteDimensional ℝ E✝
inst✝¹⁹ : MeasurableSpace E✝
inst✝¹⁸ : BorelSpace E✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
i : ↑T
e : PartialHomeomorph M H := ChartedSpace.chartAt ↑i
h : MeasureZero J (f '' (e.source ∩ s))
h₃ : U ↑i = e.source
⊢ U ↑i ∩ s ⊆ e.source ∩ s
Tactic:
rw [h₃]
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
i : ↑T
e : PartialHomeomorph M H := ChartedSpace.chartAt ↑i
h : MeasureZero J (f '' (e.source ∩ s))
⊢ U ↑i = e.source
Tactic:
rw [← Filter.principal_eq_iff_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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
⊢ ⋃ i, f '' (U ↑i ∩ s) = f '' ⋃ i, U ↑i ∩ s
Tactic:
rw [image_iUnion]
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
⊢ f '' ⋃ i, U ↑i ∩ s = f '' ((⋃ i, U ↑i) ∩ s)
Tactic:
rw [iUnion_inter]
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
⊢ f '' ((⋃ i, U ↑i) ∩ s) = f '' ((⋃ i ∈ T, U i) ∩ s)
Tactic:
rw [iUnion_coe_set]
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
⊢ f '' ((⋃ i ∈ T, U i) ∩ s) = f '' ((⋃ i, U i) ∩ s)
Tactic:
rw [hTcover]
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
⊢ f '' ((⋃ i, U i) ∩ s) = f '' (univ ∩ s)
Tactic:
rw [subset_antisymm (by simp) (hcovering)]
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
⊢ ⋃ x, U x ⊆ univ
Tactic:
simp
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
⊢ f '' (univ ∩ s) = f '' s
Tactic:
rw [univ_inter]
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✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
decomp : ⋃ i, f '' (U ↑i ∩ s) = f '' s
⊢ Encodable ↑T
Tactic:
sorry
State after:
no goals