-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem HolderOnWith.dimH_image_le (h : HolderOnWith C r f s) (hr : 0 < r) :
    dimH (f '' s) ≤ dimH s / r

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

Tactic:
have Hrd : μH[(r * d : ℝ≥0)] s = ⊤ := by
  contrapose this
  exact ENNReal.mul_ne_top ENNReal.coe_ne_top this

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ⊤
this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ⊤
Hrd : μH[↑(r * d)] s = ⊤
⊢ ↑d ≤ dimH s / ↑r

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

Tactic:
have := h.hausdorffMeasure_image_le hr d.coe_nonneg

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ⊤
this : μH[↑d] (f '' s) ≤ ↑C ^ ↑d * μH[↑r * ↑d] s
⊢ ↑d ≤ dimH s / ↑r

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

case h0
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ⊤
this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ⊤
Hrd : μH[↑(r * d)] s = ⊤
⊢ ↑r ≠ 0 ∨ dimH s ≠ 0

case ht
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ⊤
this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ⊤
Hrd : μH[↑(r * d)] s = ⊤
⊢ ↑r ≠ ⊤ ∨ dimH s ≠ ⊤

Tactic:
exacts [le_dimH_of_hausdorffMeasure_eq_top Hrd, Or.inl (mt ENNReal.coe_eq_zero.1 hr.ne'),
  Or.inl ENNReal.coe_ne_top]

Result:
no goals

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

Tactic:
rw [hd, ← ENNReal.coe_rpow_of_nonneg _ d.coe_nonneg, top_le_iff] at this

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ⊤
this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ⊤
⊢ ↑d ≤ dimH s / ↑r

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
⊢ dimH (f '' s) ≤ dimH s / ↑r

Tactic:
borelize X Y

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
⊢ dimH (f '' s) ≤ dimH s / ↑r

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

Tactic:
exact ENNReal.mul_ne_top ENNReal.coe_ne_top this

Result:
no goals

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

Tactic:
rw [ENNReal.le_div_iff_mul_le, mul_comm, ← ENNReal.coe_mul]

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ⊤
this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ⊤
Hrd : μH[↑(r * d)] s = ⊤
⊢ ↑(r * d) ≤ dimH s

case h0
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ⊤
this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ⊤
Hrd : μH[↑(r * d)] s = ⊤
⊢ ↑r ≠ 0 ∨ dimH s ≠ 0

case ht
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ⊤
this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ⊤
Hrd : μH[↑(r * d)] s = ⊤
⊢ ↑r ≠ ⊤ ∨ dimH s ≠ ⊤

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
⊢ dimH (f '' s) ≤ dimH s / ↑r

Tactic:
refine dimH_le fun d hd => ?_

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ⊤
⊢ ↑d ≤ dimH s / ↑r

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

Tactic:
contrapose this

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ⊤
this : ¬μH[↑(r * d)] s = ⊤
⊢ ¬↑(C ^ ↑d) * μH[↑r * ↑d] s = ⊤