Theorem: locally_lipschitz_image_of_null_set_is_null_set (Sard/LocallyLipschitzMeasureZero.lean)

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
⊢ ↑μH[↑d] (f '' s) = 0
Tactic:
let K : ℕ → Set X := compactCovering X
State after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
⊢ ↑μH[↑d] (f '' s) = 0

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
⊢ ↑μH[↑d] (f '' s) = 0
Tactic:
have hcov : ⋃ (n : ℕ), K n = univ := iUnion_compactCovering X
State after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
⊢ ↑μH[↑d] (f '' s) = 0

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
⊢ ↑μH[↑d] (f '' s) = 0
Tactic:
have hcompact : ∀ n : ℕ, IsCompact (K n) := isCompact_compactCovering X
State after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
⊢ ↑μH[↑d] (f '' s) = 0

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
⊢ ↑μH[↑d] (f '' s) = 0
Tactic:
suffices ass : ∀ n : ℕ, μH[d] (f '' (s ∩ K n)) = 0 by
  apply null_set_from_countable_cover _ _ ass
  rw [← image_iUnion]
  have : s = ⋃ (n : ℕ), s ∩ K n := by calc s
      _ = s ∩ univ := (inter_univ s).symm
      _ = s ∩ ⋃ (n : ℕ), K n := by rw [hcov]
      _ = ⋃ (n : ℕ), s ∩ K n := by apply inter_iUnion s
  exact Eq.subset (congrArg (image f) this)
State after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
⊢ ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
⊢ ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
intro n
State after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
choose Kx t ht hfL using fun x ↦ (hf x)
State after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
choose U hut hUopen hxU using fun x ↦ mem_nhds_iff.mp (ht x)
State after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
have hcovering : K n ⊆ ⋃ (x : X), U x := fun y _ ↦ mem_iUnion_of_mem y (hxU y)
State after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
let ⟨v, hv⟩ := IsCompact.elim_finite_subcover (hcompact n) U hUopen hcovering
State after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
have hnull: ∀ i : v, μH[d] (f '' (s ∩ U i)) = 0 := by
  intro i
  have h₂ : μH[d] (s ∩ U i) = 0 := measure_mono_null (inter_subset_left s (U ↑i)) hs
  have h₁ := ((hfL i).mono (hut i)).mono (inter_subset_right s (U i))
  refine lipschitz_image_null_set_is_null_set (Nat.cast_nonneg d) h₁ h₂
State after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
have coe : ⋃ (i : v), U i = ⋃ (i : X) (_ : i ∈ v), U i := iUnion_coe_set _ _
State after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
rw [← coe] at hv
State after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
have : f '' (s ∩ (K n)) ⊆ ⋃ (i : v), f '' (s ∩ (U i)) := by
  calc f '' (s ∩ (K n))
    _ ⊆ f '' (s ∩ (⋃ (i : v), U i)) := by
      apply image_subset
      apply inter_subset_inter_right s hv
    _ = f '' ((⋃ (i : v), s ∩ (U i))) := by rw [inter_iUnion]
    _ = ⋃ (i : v), f '' ( s ∩ (U i)) := image_iUnion
State after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
this : f '' (s ∩ K n) ⊆ ⋃ i, f '' (s ∩ U ↑i)
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
this : f '' (s ∩ K n) ⊆ ⋃ i, f '' (s ∩ U ↑i)
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
have hless : μH[d] (f '' (s ∩ (K n))) ≤ 0 := by
  calc μH[d] (f '' (s ∩ (K n)))
    _ ≤ μH[d] (⋃ (i : v), f '' (s ∩ (U i))) := measure_mono this
    _ ≤ ∑' (i : v), (μH[d] (f '' (s ∩ (U i))) : ℝ≥0∞) := by apply measure_iUnion_le
    _ = ∑' (_ : v), (0 : ℝ≥0∞) := tsum_congr hnull
    _ = 0 := by simp
State after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
this : f '' (s ∩ K n) ⊆ ⋃ i, f '' (s ∩ U ↑i)
hless : ↑μH[↑d] (f '' (s ∩ K n)) ≤ 0
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
this : f '' (s ∩ K n) ⊆ ⋃ i, f '' (s ∩ U ↑i)
hless : ↑μH[↑d] (f '' (s ∩ K n)) ≤ 0
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
simp only [nonpos_iff_eq_zero, zero_le] at hless ⊢
State after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
this : f '' (s ∩ K n) ⊆ ⋃ i, f '' (s ∩ U ↑i)
hless : ↑μH[↑d] (f '' (s ∩ K n)) = 0
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
this : f '' (s ∩ K n) ⊆ ⋃ i, f '' (s ∩ U ↑i)
hless : ↑μH[↑d] (f '' (s ∩ K n)) = 0
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
exact hless
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
ass : ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
⊢ ↑μH[↑d] (f '' s) = 0
Tactic:
apply null_set_from_countable_cover _ _ ass
State after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
ass : ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
⊢ f '' s ⊆ ⋃ n, f '' (s ∩ K n)

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
ass : ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
⊢ f '' s ⊆ ⋃ n, f '' (s ∩ K n)
Tactic:
rw [← image_iUnion]
State after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
ass : ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
⊢ f '' s ⊆ f '' ⋃ i, s ∩ K i

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
ass : ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
⊢ f '' s ⊆ f '' ⋃ i, s ∩ K i
Tactic:
have : s = ⋃ (n : ℕ), s ∩ K n := by calc s
    _ = s ∩ univ := (inter_univ s).symm
    _ = s ∩ ⋃ (n : ℕ), K n := by rw [hcov]
    _ = ⋃ (n : ℕ), s ∩ K n := by apply inter_iUnion s
State after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
ass : ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
this : s = ⋃ n, s ∩ K n
⊢ f '' s ⊆ f '' ⋃ i, s ∩ K i

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
ass : ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
this : s = ⋃ n, s ∩ K n
⊢ f '' s ⊆ f '' ⋃ i, s ∩ K i
Tactic:
exact Eq.subset (congrArg (image f) this)
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
ass : ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
⊢ s = ⋃ n, s ∩ K n
Tactic:
calc s
_ = s ∩ univ := (inter_univ s).symm
_ = s ∩ ⋃ (n : ℕ), K n := by rw [hcov]
_ = ⋃ (n : ℕ), s ∩ K n := by apply inter_iUnion s
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
ass : ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
⊢ s ∩ univ = s ∩ ⋃ n, K n
Tactic:
rw [hcov]
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
ass : ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
⊢ s ∩ ⋃ n, K n = ⋃ n, s ∩ K n
Tactic:
apply inter_iUnion s
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
⊢ ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
Tactic:
intro i
State after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
i : { x // x ∈ v }
⊢ ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
i : { x // x ∈ v }
⊢ ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
Tactic:
have h₂ : μH[d] (s ∩ U i) = 0 := measure_mono_null (inter_subset_left s (U ↑i)) hs
State after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
i : { x // x ∈ v }
h₂ : ↑μH[↑d] (s ∩ U ↑i) = 0
⊢ ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
i : { x // x ∈ v }
h₂ : ↑μH[↑d] (s ∩ U ↑i) = 0
⊢ ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
Tactic:
have h₁ := ((hfL i).mono (hut i)).mono (inter_subset_right s (U i))
State after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
i : { x // x ∈ v }
h₂ : ↑μH[↑d] (s ∩ U ↑i) = 0
h₁ : LipschitzOnWith (Kx ↑i) f (s ∩ U ↑i)
⊢ ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
i : { x // x ∈ v }
h₂ : ↑μH[↑d] (s ∩ U ↑i) = 0
h₁ : LipschitzOnWith (Kx ↑i) f (s ∩ U ↑i)
⊢ ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
Tactic:
refine lipschitz_image_null_set_is_null_set (Nat.cast_nonneg d) h₁ h₂
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
⊢ f '' (s ∩ K n) ⊆ ⋃ i, f '' (s ∩ U ↑i)
Tactic:
calc f '' (s ∩ (K n))
  _ ⊆ f '' (s ∩ (⋃ (i : v), U i)) := by
    apply image_subset
    apply inter_subset_inter_right s hv
  _ = f '' ((⋃ (i : v), s ∩ (U i))) := by rw [inter_iUnion]
  _ = ⋃ (i : v), f '' ( s ∩ (U i)) := image_iUnion
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
⊢ f '' (s ∩ K n) ⊆ f '' (s ∩ ⋃ i, U ↑i)
Tactic:
apply image_subset
State after:
case h
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
⊢ s ∩ K n ⊆ s ∩ ⋃ i, U ↑i

State before:
case h
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
⊢ s ∩ K n ⊆ s ∩ ⋃ i, U ↑i
Tactic:
apply inter_subset_inter_right s hv
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
⊢ f '' (s ∩ ⋃ i, U ↑i) = f '' ⋃ i, s ∩ U ↑i
Tactic:
rw [inter_iUnion]
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
this : f '' (s ∩ K n) ⊆ ⋃ i, f '' (s ∩ U ↑i)
⊢ ↑μH[↑d] (f '' (s ∩ K n)) ≤ 0
Tactic:
calc μH[d] (f '' (s ∩ (K n)))
  _ ≤ μH[d] (⋃ (i : v), f '' (s ∩ (U i))) := measure_mono this
  _ ≤ ∑' (i : v), (μH[d] (f '' (s ∩ (U i))) : ℝ≥0∞) := by apply measure_iUnion_le
  _ = ∑' (_ : v), (0 : ℝ≥0∞) := tsum_congr hnull
  _ = 0 := by simp
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
this : f '' (s ∩ K n) ⊆ ⋃ i, f '' (s ∩ U ↑i)
⊢ ↑μH[↑d] (⋃ i, f '' (s ∩ U ↑i)) ≤ ∑' (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i))
Tactic:
apply measure_iUnion_le
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
this : f '' (s ∩ K n) ⊆ ⋃ i, f '' (s ∩ U ↑i)
⊢ ∑' (x : { x // x ∈ v }), 0 = 0
Tactic:
simp
State after:
no goals