-- 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 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
⊢ μH[d] {f x} ≤ ↑0 ^ d * μH[↑r * d] s

Tactic:
haveI := noAtoms_hausdorff Y h'd

Result:
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

Proof state:
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

Tactic:
rcases eq_empty_or_nonempty s with (rfl | ⟨x, hx⟩)

Result:
case inl.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
hr : 0 < r
d : ℝ
hd : 0 ≤ d
h : HolderOnWith 0 r f ∅
⊢ μH[d] (f '' ∅) ≤ ↑0 ^ d * μH[↑r * d] ∅

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

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
hC0 : 0 < C
hCd0 : ↑C ^ d ≠ 0
⊢ ↑C ^ d ≠ ⊤

Tactic:
simp [hd]

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
hCd0 : ↑C ^ d ≠ 0
hCd : ↑C ^ d ≠ ⊤
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (fun d => ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
⊢ ⨅ t,
      ⨅ (_ : f '' s ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ R), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ d ≤
    ⨆ i,
      ⨆ (_ : 0 < i),
        ⨅ i_1,
          ⨅ (_ : s ⊆ ⋃ n, i_1 n),
            ⨅ (_ : ∀ (n : ℕ), diam (i_1 n) ≤ i), ∑' (i : ℕ), ⨆ (_ : (i_1 i).Nonempty), ↑C ^ d * diam (i_1 i) ^ (↑r * d)

Tactic:
rcases ENNReal.nhds_zero_basis_Iic.eventually_iff.1 (this.eventually (gt_mem_nhds hR)) with
  ⟨δ, δ0, H⟩

Result:
case inr.intro.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
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,
      ⨅ (_ : f '' s ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ R), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ d ≤
    ⨆ i,
      ⨆ (_ : 0 < i),
        ⨅ i_1,
          ⨅ (_ : s ⊆ ⋃ n, i_1 n),
            ⨅ (_ : ∀ (n : ℕ), diam (i_1 n) ≤ i), ∑' (i : ℕ), ⨆ (_ : (i_1 i).Nonempty), ↑C ^ d * diam (i_1 i) ^ (↑r * d)

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 : ℕ
⊢ ⨆ (_ : ((fun n => f '' (t n ∩ s)) n).Nonempty), diam ((fun n => f '' (t n ∩ s)) n) ^ d ≤
    ⨆ (_ : (t n).Nonempty), ↑C ^ d * diam (t n) ^ (↑r * d)

Tactic:
simp only [iSup_le_iff, image_nonempty]

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 : ℕ
⊢ (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
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
⊢ ↑C ^ d ≠ 0

Tactic:
simp [hC0.ne']

Result:
no goals

Proof state:
case inl.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
hr : 0 < r
d : ℝ
hd : 0 ≤ d
h : HolderOnWith 0 r f ∅
⊢ μH[d] (f '' ∅) ≤ ↑0 ^ d * μH[↑r * d] ∅

Tactic:
simp only [measure_empty, nonpos_iff_eq_zero, mul_zero, image_empty]

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 : ℕ), ⨆ (_ : ((fun n => f '' (t n ∩ s)) n).Nonempty), diam ((fun n => f '' (t n ∩ s)) n) ^ d ≤
    ∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), ↑C ^ d * diam (t i) ^ (↑r * d)

Tactic:
refine ENNReal.tsum_le_tsum fun n => ?_

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 : ℕ
⊢ ⨆ (_ : ((fun n => f '' (t n ∩ s)) n).Nonempty), diam ((fun n => f '' (t n ∩ s)) n) ^ d ≤
    ⨆ (_ : (t n).Nonempty), ↑C ^ d * diam (t n) ^ (↑r * d)