-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem hausdorffMeasure_image_le (h : HolderOnWith C r f s) (hr : 0 < r) {d : ℝ} (hd : 0 ≤ d) :
    μH[d] (f '' s) ≤ (C : ℝ≥0∞) ^ d * μH[r * d] s

Proof state:
case inr.intro.intro.refine_2
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
hCd0 : ↑C ^ d ≠ 0
hCd : ↑C ^ d ≠ ⊤
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (fun d => ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → ↑C * x ^ ↑r < R
t : ℕ → Set X
hst : s ⊆ ⋃ n, t n
htδ : ∀ (n : ℕ), diam (t n) ≤ δ
n : ℕ
⊢ (t n ∩ s).Nonempty → diam (f '' (t n ∩ s)) ^ d ≤ ⨆ (_ : (t n).Nonempty), ↑C ^ d * diam (t n) ^ (↑r * d)

Tactic:
intro hft

Result:
case inr.intro.intro.refine_2
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
hCd0 : ↑C ^ d ≠ 0
hCd : ↑C ^ d ≠ ⊤
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (fun d => ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → ↑C * x ^ ↑r < R
t : ℕ → Set X
hst : s ⊆ ⋃ n, t n
htδ : ∀ (n : ℕ), diam (t n) ≤ δ
n : ℕ
hft : (t n ∩ s).Nonempty
⊢ diam (f '' (t n ∩ s)) ^ d ≤ ⨆ (_ : (t n).Nonempty), ↑C ^ d * diam (t n) ^ (↑r * d)

Proof state:
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
r : ℝ≥0
f : X → Y
s : Set X
hr : 0 < r
d : ℝ
hd : 0 ≤ d
h : HolderOnWith 0 r f s
x : X
hx : x ∈ s
⊢ (f '' s).Subsingleton

Tactic:
simpa [diam_eq_zero_iff] using h.ediam_image_le

Result:
no goals

Proof state:
case inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
⊢ μH[d] (f '' s) ≤ ↑C ^ d * μH[↑r * d] s

Tactic:
have hCd0 : (C : ℝ≥0∞) ^ d ≠ 0 := by simp [hC0.ne']

Result:
case inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
hCd0 : ↑C ^ d ≠ 0
⊢ μH[d] (f '' s) ≤ ↑C ^ d * μH[↑r * d] s

Proof state:
case inl.inr.intro.inl
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
r : ℝ≥0
f : X → Y
s : Set X
hr : 0 < r
h : HolderOnWith 0 r f s
x : X
hx : x ∈ s
this : f '' s = {f x}
hd : 0 ≤ 0
⊢ μH[0] {f x} ≤ μH[0] s

Tactic:
rw [hausdorffMeasure_zero_singleton]

Result:
case inl.inr.intro.inl
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
r : ℝ≥0
f : X → Y
s : Set X
hr : 0 < r
h : HolderOnWith 0 r f s
x : X
hx : x ∈ s
this : f '' s = {f x}
hd : 0 ≤ 0
⊢ 1 ≤ μH[0] s

Proof state:
case inl.inr.intro
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
r : ℝ≥0
f : X → Y
s : Set X
hr : 0 < r
d : ℝ
hd : 0 ≤ d
h : HolderOnWith 0 r f s
x : X
hx : x ∈ s
⊢ μH[d] (f '' s) ≤ ↑0 ^ d * μH[↑r * d] s

Tactic:
have : f '' s = {f x} :=
  have : (f '' s).Subsingleton := by simpa [diam_eq_zero_iff] using h.ediam_image_le
  (subsingleton_iff_singleton (mem_image_of_mem f hx)).1 this

Result:
case inl.inr.intro
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
r : ℝ≥0
f : X → Y
s : Set X
hr : 0 < r
d : ℝ
hd : 0 ≤ d
h : HolderOnWith 0 r f s
x : X
hx : x ∈ s
this : f '' s = {f x}
⊢ μH[d] (f '' s) ≤ ↑0 ^ d * μH[↑r * d] s

Proof state:
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
⊢ μH[d] (f '' s) ≤ ↑C ^ d * μH[↑r * d] s

Tactic:
rcases (zero_le C).eq_or_lt with (rfl | hC0)

Result:
case inl
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
r : ℝ≥0
f : X → Y
s : Set X
hr : 0 < r
d : ℝ
hd : 0 ≤ d
h : HolderOnWith 0 r f s
⊢ μH[d] (f '' s) ≤ ↑0 ^ d * μH[↑r * d] s

case inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
⊢ μH[d] (f '' s) ≤ ↑C ^ d * μH[↑r * d] s

Proof state:
case inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
hCd0 : ↑C ^ d ≠ 0
⊢ μH[d] (f '' s) ≤ ↑C ^ d * μH[↑r * d] s

Tactic:
have hCd : (C : ℝ≥0∞) ^ d ≠ ∞ := by simp [hd]

Result:
case inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
hCd0 : ↑C ^ d ≠ 0
hCd : ↑C ^ d ≠ ⊤
⊢ μH[d] (f '' s) ≤ ↑C ^ d * μH[↑r * d] s

Proof state:
case inl.inr.intro.inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
r : ℝ≥0
f : X → Y
s : Set X
hr : 0 < r
d : ℝ
hd : 0 ≤ d
h : HolderOnWith 0 r f s
x : X
hx : x ∈ s
this✝ : f '' s = {f x}
h'd : 0 < d
this : NoAtoms μH[d]
⊢ μH[d] {f x} ≤ ↑0 ^ d * μH[↑r * d] s

Tactic:
simp only [zero_le, measure_singleton]

Result:
no goals

Proof state:
case inr.intro.intro.refine_2
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
hCd0 : ↑C ^ d ≠ 0
hCd : ↑C ^ d ≠ ⊤
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (fun d => ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → ↑C * x ^ ↑r < R
t : ℕ → Set X
hst : s ⊆ ⋃ n, t n
htδ : ∀ (n : ℕ), diam (t n) ≤ δ
n : ℕ
hft : (t n ∩ s).Nonempty
⊢ diam (f '' (t n ∩ s)) ^ d ≤ ↑C ^ d * diam (t n) ^ (↑r * d)

Tactic:
rw [ENNReal.rpow_mul, ← ENNReal.mul_rpow_of_nonneg _ _ hd]

Result:
case inr.intro.intro.refine_2
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
hCd0 : ↑C ^ d ≠ 0
hCd : ↑C ^ d ≠ ⊤
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (fun d => ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → ↑C * x ^ ↑r < R
t : ℕ → Set X
hst : s ⊆ ⋃ n, t n
htδ : ∀ (n : ℕ), diam (t n) ≤ δ
n : ℕ
hft : (t n ∩ s).Nonempty
⊢ diam (f '' (t n ∩ s)) ^ d ≤ (↑C * diam (t n) ^ ↑r) ^ d