awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 = {f x}

Tactic:
have : f '' s = {f x} :=
      have : (f '' s).Subsingleton := by simpa [ediam_eq_zero_iff] using h.ediam_image_le
      (subsingleton_iff_singleton (mem_image_of_mem f hx)).1 this
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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}
inl :
  ((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) {f x} ≤
    HMul.hMul (β := ℝ≥0∞) ((↑0 : ℝ≥0∞) ^ d) (((μH[(↑r : ℝ) * d] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' s) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑0 : ℝ≥0∞) ^ d) (((μH[(↑r : ℝ) * d] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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}
inl :
  ∀ (hd : LE.le (α := ℝ) 0 0),
    ((μH[0] : Measure Y) : (a : Set Y) → ℝ≥0∞) {f x} ≤
      HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℝ) (↑0 : ℝ≥0∞) 0)
        (((μH[(↑r : ℝ) * 0] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
inl₁ :
  ∀ (h'd : 0 < d),
    ((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) {f x} ≤
      HMul.hMul (β := ℝ≥0∞) ((↑0 : ℝ≥0∞) ^ d) (((μH[(↑r : ℝ) * d] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) {f x} ≤
    HMul.hMul (β := ℝ≥0∞) ((↑0 : ℝ≥0∞) ^ d) (((μH[(↑r : ℝ) * d] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rcases eq_or_lt_of_le hd with (rfl | h'd)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : LE.le (α := ℝ) 0 0
inl :
  LE.le (α := ℝ≥0∞) (((μH[0] : Measure Y) : (a : Set Y) → ℝ≥0∞) {f x} : ℝ≥0∞)
    (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[0] : Measure Y) : (a : Set Y) → ℝ≥0∞) {f x} ≤
    HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℝ) (↑0 : ℝ≥0∞) 0)
      (((μH[(↑r : ℝ) * 0] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [ENNReal.rpow_zero, one_mul, mul_zero]

Premises used: MulZeroClass.mul_zero, ENNReal.rpow_zero, one_mul
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : LE.le (α := ℝ) 0 0
inl : LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((μH[0] : Measure Y) : (a : Set Y) → ℝ≥0∞) {f x} : ℝ≥0∞)
    (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [hausdorffMeasure_zero_singleton]

Premises used: MeasureTheory.Measure.hausdorffMeasure_zero_singleton
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : LE.le (α := ℝ) 0 0
⊢ LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
one_le_hausdorffMeasure_zero_of_nonempty ⟨x, hx⟩

Premises used: Set.Mem, MeasureTheory.Measure.one_le_hausdorffMeasure_zero_of_nonempty, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : LE.le (α := ℝ) 0 0
⊢ LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact one_le_hausdorffMeasure_zero_of_nonempty ⟨x, hx⟩

Premises used: MeasureTheory.Measure.one_le_hausdorffMeasure_zero_of_nonempty, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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
⊢ NoAtoms.{u_3} (α := Y) (m0 := inst_4) μH[d]

Tactic:
haveI := noAtoms_hausdorff Y h'd
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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_1 : f '' s = {f x}
h'd : 0 < d
this : NoAtoms.{u_3} (α := Y) (m0 := inst_4) μH[d]
⊢ ((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) {f x} ≤
    HMul.hMul (β := ℝ≥0∞) ((↑0 : ℝ≥0∞) ^ d) (((μH[(↑r : ℝ) * d] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [zero_le, measure_singleton]

Premises used: zero_le, MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : ℝ≥0∞) ^ d ≠ 0

Tactic:
simp [hC0.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : ℝ≥0∞) ^ d ≠ 0

Tactic:
have hCd0 : (C : ℝ≥0∞) ^ d ≠ 0 := by simp [hC0.ne']
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : ℝ≥0∞) ^ d ≠ 0
⊢ (↑C : ℝ≥0∞) ^ d ≠ ∞

Tactic:
simp [hd]
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : ℝ≥0∞) ^ d ≠ 0
⊢ (↑C : ℝ≥0∞) ^ d ≠ ∞

Tactic:
have hCd : (C : ℝ≥0∞) ^ d ≠ ∞ := by simp [hd]
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : ℝ≥0∞) ^ d ≠ 0
hCd : (↑C : ℝ≥0∞) ^ d ≠ ∞
inr :
  LE.le (α := ℝ≥0∞)
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : 0 < r),
        ⨅ (t : ℕ → Set Y),
          ⨅ (_ : f '' s ⊆ ⋃ (n : ℕ), t n),
            ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d)
    (⨆ (i : ℝ≥0∞),
      ⨆ (_ : 0 < i),
        ⨅ (i_1 : ℕ → Set X),
          ⨅ (_ : s ⊆ ⋃ (n : ℕ), i_1 n),
            ⨅ (_ : ∀ (n : ℕ), ediam (i_1 n) ≤ i),
              ∑' (i : ℕ), ⨆ (_ : (i_1 i).Nonempty), (↑C : ℝ≥0∞) ^ d * ediam (i_1 i) ^ ((↑r : ℝ) * d))
⊢ ((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' s) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ d) (((μH[(↑r : ℝ) * d] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [hausdorffMeasure_apply, ENNReal.mul_iSup, ENNReal.mul_iInf_of_ne hCd0 hCd,
      ← ENNReal.tsum_mul_left]

Premises used: ENNReal.tsum_mul_left, ENNReal.mul_iInf_of_ne, MeasureTheory.Measure.hausdorffMeasure_apply, ENNReal.mul_iSup
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : ℝ≥0∞) ^ d ≠ 0
hCd : (↑C : ℝ≥0∞) ^ d ≠ ∞
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : 0 < r),
        ⨅ (t : ℕ → Set Y),
          ⨅ (_ : f '' s ⊆ ⋃ (n : ℕ), t n),
            ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d)
    (⨆ (i : ℝ≥0∞),
      ⨆ (_ : 0 < i),
        ⨅ (i_1 : ℕ → Set X),
          ⨅ (_ : s ⊆ ⋃ (n : ℕ), i_1 n),
            ⨅ (_ : ∀ (n : ℕ), ediam (i_1 n) ≤ i),
              ∑' (i : ℕ), ⨆ (_ : (i_1 i).Nonempty), (↑C : ℝ≥0∞) ^ d * ediam (i_1 i) ^ ((↑r : ℝ) * d))

Tactic:
iSup_le fun R => iSup_le fun hR => ?_

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : ℝ≥0∞) ^ d ≠ 0
hCd : (↑C : ℝ≥0∞) ^ d ≠ ∞
inr :
  ∀ (R : ℝ≥0∞) (hR : 0 < R),
    LE.le (α := ℝ≥0∞)
      (⨅ (t : ℕ → Set Y),
        ⨅ (_ : f '' s ⊆ ⋃ (n : ℕ), t n),
          ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ R), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d)
      (⨆ (i : ℝ≥0∞),
        ⨆ (_ : 0 < i),
          ⨅ (i_1 : ℕ → Set X),
            ⨅ (_ : s ⊆ ⋃ (n : ℕ), i_1 n),
              ⨅ (_ : ∀ (n : ℕ), ediam (i_1 n) ≤ i),
                ∑' (i : ℕ), ⨆ (_ : (i_1 i).Nonempty), (↑C : ℝ≥0∞) ^ d * ediam (i_1 i) ^ ((↑r : ℝ) * d))
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : 0 < r),
        ⨅ (t : ℕ → Set Y),
          ⨅ (_ : f '' s ⊆ ⋃ (n : ℕ), t n),
            ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d)
    (⨆ (i : ℝ≥0∞),
      ⨆ (_ : 0 < i),
        ⨅ (i_1 : ℕ → Set X),
          ⨅ (_ : s ⊆ ⋃ (n : ℕ), i_1 n),
            ⨅ (_ : ∀ (n : ℕ), ediam (i_1 n) ≤ i),
              ∑' (i : ℕ), ⨆ (_ : (i_1 i).Nonempty), (↑C : ℝ≥0∞) ^ d * ediam (i_1 i) ^ ((↑r : ℝ) * d))

Tactic:
refine iSup_le fun R => iSup_le fun hR => ?_

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : ℝ≥0∞) ^ d ≠ 0
hCd : (↑C : ℝ≥0∞) ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
⊢ Tendsto (β := ℝ≥0∞) (fun (d : ℝ≥0∞) ↦ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)) (𝓝 0) (𝓝 0)

Tactic:
have : Tendsto (fun d : ℝ≥0∞ => (C : ℝ≥0∞) * d ^ (r : ℝ)) (𝓝 0) (𝓝 0) :=
      ENNReal.tendsto_const_mul_rpow_nhds_zero_of_pos ENNReal.coe_ne_top hr
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : ℝ≥0∞) ^ d ≠ 0
hCd : (↑C : ℝ≥0∞) ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (β := ℝ≥0∞) (fun (d : ℝ≥0∞) ↦ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)) (𝓝 0) (𝓝 0)
inr :
  ∀ (δ : ℝ≥0∞) (δ0 : 0 < δ) (H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → (↑C : ℝ≥0∞) * x ^ (↑r : ℝ) < R),
    LE.le (α := ℝ≥0∞)
      (⨅ (t : ℕ → Set Y),
        ⨅ (_ : f '' s ⊆ ⋃ (n : ℕ), t n),
          ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ R), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d)
      (⨆ (i : ℝ≥0∞),
        ⨆ (_ : 0 < i),
          ⨅ (i_1 : ℕ → Set X),
            ⨅ (_ : s ⊆ ⋃ (n : ℕ), i_1 n),
              ⨅ (_ : ∀ (n : ℕ), ediam (i_1 n) ≤ i),
                ∑' (i : ℕ), ⨆ (_ : (i_1 i).Nonempty), (↑C : ℝ≥0∞) ^ d * ediam (i_1 i) ^ ((↑r : ℝ) * d))
⊢ LE.le (α := ℝ≥0∞)
    (⨅ (t : ℕ → Set Y),
      ⨅ (_ : f '' s ⊆ ⋃ (n : ℕ), t n),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ R), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d)
    (⨆ (i : ℝ≥0∞),
      ⨆ (_ : 0 < i),
        ⨅ (i_1 : ℕ → Set X),
          ⨅ (_ : s ⊆ ⋃ (n : ℕ), i_1 n),
            ⨅ (_ : ∀ (n : ℕ), ediam (i_1 n) ≤ i),
              ∑' (i : ℕ), ⨆ (_ : (i_1 i).Nonempty), (↑C : ℝ≥0∞) ^ d * ediam (i_1 i) ^ ((↑r : ℝ) * d))

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

Premises used: gt_mem_nhds, ENNReal.nhds_zero_basis_Iic, Filter.Tendsto.eventually, Iff.mp, Filter.HasBasis.eventually_iff
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : ℝ≥0∞) ^ d ≠ 0
hCd : (↑C : ℝ≥0∞) ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (β := ℝ≥0∞) (fun (d : ℝ≥0∞) ↦ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → (↑C : ℝ≥0∞) * x ^ (↑r : ℝ) < R
⊢ LE.le (α := ℝ≥0∞)
    (⨅ (t : ℕ → Set Y),
      ⨅ (_ : f '' s ⊆ ⋃ (n : ℕ), t n),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ R), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d)
    (⨆ (i : ℝ≥0∞),
      ⨆ (_ : 0 < i),
        ⨅ (i_1 : ℕ → Set X),
          ⨅ (_ : s ⊆ ⋃ (n : ℕ), i_1 n),
            ⨅ (_ : ∀ (n : ℕ), ediam (i_1 n) ≤ i),
              ∑' (i : ℕ), ⨆ (_ : (i_1 i).Nonempty), (↑C : ℝ≥0∞) ^ d * ediam (i_1 i) ^ ((↑r : ℝ) * d))

Tactic:
le_iSup₂_of_le δ δ0 <| iInf₂_mono' fun t hst ↦
      ⟨fun n => f '' (t n ∩ s), ?_, iInf_mono' fun htδ ↦
        ⟨fun n => (h.ediam_image_inter_le (t n)).trans (H (htδ n)).le, ?_⟩⟩

Premises used: LT.lt.le, Inter.inter, iInf₂_mono', Exists.intro, Set.image, HolderOnWith.ediam_image_inter_le, LE.le.trans, le_iSup₂_of_le, iInf_mono'
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : ℝ≥0∞) ^ d ≠ 0
hCd : (↑C : ℝ≥0∞) ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (β := ℝ≥0∞) (fun (d : ℝ≥0∞) ↦ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → (↑C : ℝ≥0∞) * x ^ (↑r : ℝ) < R
inr : ∀ (t : ℕ → Set X) (hst : s ⊆ ⋃ (n : ℕ), t n), f '' s ⊆ ⋃ (n : ℕ), (fun (n : ℕ) ↦ f '' (t n ∩ s)) n
inr₁ :
  ∀ (t : ℕ → Set X) (hst : s ⊆ ⋃ (n : ℕ), t n) (htδ : ∀ (n : ℕ), ediam (t n) ≤ δ),
    LE.le (α := ℝ≥0∞)
      (∑' (n : ℕ),
        ⨆ (_ : Set.Nonempty.{u_3} (α := Y) ((fun (n : ℕ) ↦ f '' (t n ∩ s)) n)),
          ediam.{u_3} (X := Y) ((fun (n : ℕ) ↦ f '' (t n ∩ s)) n) ^ d)
      (∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), (↑C : ℝ≥0∞) ^ d * ediam (t i) ^ ((↑r : ℝ) * d))
⊢ LE.le (α := ℝ≥0∞)
    (⨅ (t : ℕ → Set Y),
      ⨅ (_ : f '' s ⊆ ⋃ (n : ℕ), t n),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ R), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d)
    (⨆ (i : ℝ≥0∞),
      ⨆ (_ : 0 < i),
        ⨅ (i_1 : ℕ → Set X),
          ⨅ (_ : s ⊆ ⋃ (n : ℕ), i_1 n),
            ⨅ (_ : ∀ (n : ℕ), ediam (i_1 n) ≤ i),
              ∑' (i : ℕ), ⨆ (_ : (i_1 i).Nonempty), (↑C : ℝ≥0∞) ^ d * ediam (i_1 i) ^ ((↑r : ℝ) * d))

Tactic:
refine le_iSup₂_of_le δ δ0 <| iInf₂_mono' fun t hst ↦
      ⟨fun n => f '' (t n ∩ s), ?_, iInf_mono' fun htδ ↦
        ⟨fun n => (h.ediam_image_inter_le (t n)).trans (H (htδ n)).le, ?_⟩⟩

Premises used: Inter.inter, iInf₂_mono', Exists.intro, Set.image, le_iSup₂_of_le
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : ℝ≥0∞) ^ d ≠ 0
hCd : (↑C : ℝ≥0∞) ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (β := ℝ≥0∞) (fun (d : ℝ≥0∞) ↦ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → (↑C : ℝ≥0∞) * x ^ (↑r : ℝ) < R
t : ℕ → Set X
hst : s ⊆ ⋃ (n : ℕ), t n
inr : f '' s ⊆ f '' ⋃ (i : ℕ), t i ∩ s
inr₁ : f '' s ⊆ f '' ((⋃ (i : ℕ), t i) ∩ s)
inr₂ : f '' s ⊆ f '' (s ∩ s)
inr₃ inr₄ : f '' s ⊆ f '' s
⊢ f '' s ⊆ ⋃ (n : ℕ), (fun (n : ℕ) ↦ f '' (t n ∩ s)) n

Tactic:
grw [← image_iUnion, ← iUnion_inter, ← hst, inter_self]

Premises used: Set.inter_self, Set.iUnion_inter, Set.image_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : ℝ≥0∞) ^ d ≠ 0
hCd : (↑C : ℝ≥0∞) ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (β := ℝ≥0∞) (fun (d : ℝ≥0∞) ↦ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → (↑C : ℝ≥0∞) * x ^ (↑r : ℝ) < R
t : ℕ → Set X
hst : s ⊆ ⋃ (n : ℕ), t n
htδ : ∀ (n : ℕ), ediam (t n) ≤ δ
⊢ LE.le (α := ℝ≥0∞)
    (∑' (n : ℕ),
      ⨆ (_ : Set.Nonempty.{u_3} (α := Y) ((fun (n : ℕ) ↦ f '' (t n ∩ s)) n)),
        ediam.{u_3} (X := Y) ((fun (n : ℕ) ↦ f '' (t n ∩ s)) n) ^ d)
    (∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), (↑C : ℝ≥0∞) ^ d * ediam (t i) ^ ((↑r : ℝ) * d))

Tactic:
ENNReal.tsum_le_tsum fun n => ?_

Premises used: ENNReal.tsum_le_tsum
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : ℝ≥0∞) ^ d ≠ 0
hCd : (↑C : ℝ≥0∞) ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (β := ℝ≥0∞) (fun (d : ℝ≥0∞) ↦ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → (↑C : ℝ≥0∞) * x ^ (↑r : ℝ) < R
t : ℕ → Set X
hst : s ⊆ ⋃ (n : ℕ), t n
htδ : ∀ (n : ℕ), ediam (t n) ≤ δ
inr :
  ∀ (n : ℕ),
    LE.le (α := ℝ≥0∞)
      (⨆ (_ : Set.Nonempty.{u_3} (α := Y) ((fun (n : ℕ) ↦ f '' (t n ∩ s)) n)),
        ediam.{u_3} (X := Y) ((fun (n : ℕ) ↦ f '' (t n ∩ s)) n) ^ d)
      (⨆ (_ : (t n).Nonempty), (↑C : ℝ≥0∞) ^ d * ediam (t n) ^ ((↑r : ℝ) * d))
⊢ LE.le (α := ℝ≥0∞)
    (∑' (n : ℕ),
      ⨆ (_ : Set.Nonempty.{u_3} (α := Y) ((fun (n : ℕ) ↦ f '' (t n ∩ s)) n)),
        ediam.{u_3} (X := Y) ((fun (n : ℕ) ↦ f '' (t n ∩ s)) n) ^ d)
    (∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), (↑C : ℝ≥0∞) ^ d * ediam (t i) ^ ((↑r : ℝ) * d))

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

Premises used: ENNReal.tsum_le_tsum
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : ℝ≥0∞) ^ d ≠ 0
hCd : (↑C : ℝ≥0∞) ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (β := ℝ≥0∞) (fun (d : ℝ≥0∞) ↦ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → (↑C : ℝ≥0∞) * x ^ (↑r : ℝ) < R
t : ℕ → Set X
hst : s ⊆ ⋃ (n : ℕ), t n
htδ : ∀ (n : ℕ), ediam (t n) ≤ δ
n : ℕ
inr :
  ∀ (i : (t n ∩ s).Nonempty),
    ediam (f '' (t n ∩ s)) ^ d ≤ ⨆ (_ : (t n).Nonempty), (↑C : ℝ≥0∞) ^ d * ediam (t n) ^ ((↑r : ℝ) * d)
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (_ : Set.Nonempty.{u_3} (α := Y) ((fun (n : ℕ) ↦ f '' (t n ∩ s)) n)),
      ediam.{u_3} (X := Y) ((fun (n : ℕ) ↦ f '' (t n ∩ s)) n) ^ d)
    (⨆ (_ : (t n).Nonempty), (↑C : ℝ≥0∞) ^ d * ediam (t n) ^ ((↑r : ℝ) * d))

Tactic:
simp only [iSup_le_iff, image_nonempty]

Premises used: Set.image_nonempty, iSup_le_iff
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : ℝ≥0∞) ^ d ≠ 0
hCd : (↑C : ℝ≥0∞) ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (β := ℝ≥0∞) (fun (d : ℝ≥0∞) ↦ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → (↑C : ℝ≥0∞) * x ^ (↑r : ℝ) < R
t : ℕ → Set X
hst : s ⊆ ⋃ (n : ℕ), t n
htδ : ∀ (n : ℕ), ediam (t n) ≤ δ
n : ℕ
hft : (t n ∩ s).Nonempty
inr : ediam (f '' (t n ∩ s)) ^ d ≤ (↑C : ℝ≥0∞) ^ d * ediam (t n) ^ ((↑r : ℝ) * d)
⊢ ediam (f '' (t n ∩ s)) ^ d ≤ ⨆ (_ : (t n).Nonempty), (↑C : ℝ≥0∞) ^ d * ediam (t n) ^ ((↑r : ℝ) * d)

Tactic:
simp only [Nonempty.mono ((t n).inter_subset_left) hft, ciSup_pos]

Premises used: Set.inter_subset_left, Set.Nonempty.mono, ciSup_pos
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : ℝ≥0∞) ^ d ≠ 0
hCd : (↑C : ℝ≥0∞) ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (β := ℝ≥0∞) (fun (d : ℝ≥0∞) ↦ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → (↑C : ℝ≥0∞) * x ^ (↑r : ℝ) < R
t : ℕ → Set X
hst : s ⊆ ⋃ (n : ℕ), t n
htδ : ∀ (n : ℕ), ediam (t n) ≤ δ
n : ℕ
hft : (t n ∩ s).Nonempty
inr : ediam (f '' (t n ∩ s)) ^ d ≤ ((↑C : ℝ≥0∞) * ediam (t n) ^ (↑r : ℝ)) ^ d
⊢ ediam (f '' (t n ∩ s)) ^ d ≤ (↑C : ℝ≥0∞) ^ d * ediam (t n) ^ ((↑r : ℝ) * d)

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

Premises used: ENNReal.rpow_mul, ENNReal.mul_rpow_of_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : 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 : ℝ≥0∞) ^ d ≠ 0
hCd : (↑C : ℝ≥0∞) ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (β := ℝ≥0∞) (fun (d : ℝ≥0∞) ↦ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → (↑C : ℝ≥0∞) * x ^ (↑r : ℝ) < R
t : ℕ → Set X
hst : s ⊆ ⋃ (n : ℕ), t n
htδ : ∀ (n : ℕ), ediam (t n) ≤ δ
n : ℕ
hft : (t n ∩ s).Nonempty
inr : ediam (f '' (t n ∩ s)) ≤ (↑C : ℝ≥0∞) * ediam (t n) ^ (↑r : ℝ)
⊢ ediam (f '' (t n ∩ s)) ^ d ≤ ((↑C : ℝ≥0∞) * ediam (t n) ^ (↑r : ℝ)) ^ d

Tactic:
gcongr