Theorem: measure_zero_image_iff_chart_domains
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✝
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]
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✝
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)