awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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] : 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∞)
have 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∞)
Tactic: rcases eq_or_lt_of_le hd with (rfl | h'd)
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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∞)
⊢ ((μ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∞)
have 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∞)
Tactic: rcases eq_or_lt_of_le hd with (rfl | h'd)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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
⊢ ((μ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∞)
have 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∞)
Tactic: simp only [ENNReal.rpow_zero, one_mul, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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∞) (((μH[0] : Measure Y) : (a : Set Y) → ℝ≥0∞) {f x} : ℝ≥0∞)
    (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have inl : LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [hausdorffMeasure_zero_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
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
⊢ ((μ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∞)
have this₁ : NoAtoms.{u_3} (α := Y) (m0 := inst_4) μH[d]
Tactic: haveI := noAtoms_hausdorff Y h'd
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
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
⊢ ((μ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∞)
have hCd0 : (↑C : ℝ≥0∞) ^ d ≠ 0
Tactic: have hCd0 : (C : ℝ≥0∞) ^ d ≠ 0 := by simp [hC0.ne']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
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
⊢ ((μ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∞)
have hCd : (↑C : ℝ≥0∞) ^ d ≠ ∞
Tactic: have hCd : (C : ℝ≥0∞) ^ d ≠ ∞ := by simp [hd]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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 ≠ ∞
⊢ ((μ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∞)
have 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))
Tactic: simp only [hausdorffMeasure_apply, ENNReal.mul_iSup, ENNReal.mul_iInf_of_ne hCd0 hCd,
      ← ENNReal.tsum_mul_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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))
have 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))
Tactic: refine iSup_le fun R => iSup_le fun hR => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
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
⊢ 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))
have this : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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)
⊢ 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))
have 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))
Tactic: rcases ENNReal.nhds_zero_basis_Iic.eventually_iff.1 (this.eventually (gt_mem_nhds hR)) with
      ⟨δ, δ0, H⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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))
have inr : ∀ (t : ℕ → Set X) (hst : s ⊆ ⋃ (n : ℕ), t n), f '' s ⊆ ⋃ (n : ℕ), (fun (n : ℕ) ↦ f '' (t n ∩ s)) n
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, ?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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
⊢ 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))
have 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))
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, ?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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
⊢ f '' s ⊆ ⋃ (n : ℕ), (fun (n : ℕ) ↦ f '' (t n ∩ s)) n
have inr : f '' s ⊆ f '' ⋃ (i : ℕ), t i ∩ s
Tactic: grw [← image_iUnion, ← iUnion_inter, ← hst, inter_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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
⊢ f '' s ⊆ ⋃ (n : ℕ), (fun (n : ℕ) ↦ f '' (t n ∩ s)) n
have inr₁ : f '' s ⊆ f '' ((⋃ (i : ℕ), t i) ∩ s)
Tactic: grw [← image_iUnion, ← iUnion_inter, ← hst, inter_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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)
⊢ f '' s ⊆ ⋃ (n : ℕ), (fun (n : ℕ) ↦ f '' (t n ∩ s)) n
have inr₂ : f '' s ⊆ f '' (s ∩ s)
Tactic: grw [← image_iUnion, ← iUnion_inter, ← hst, inter_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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)
⊢ f '' s ⊆ ⋃ (n : ℕ), (fun (n : ℕ) ↦ f '' (t n ∩ s)) n
have inr₃ : f '' s ⊆ f '' s
Tactic: grw [← image_iUnion, ← iUnion_inter, ← hst, inter_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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))
have 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))
Tactic: refine ENNReal.tsum_le_tsum fun n => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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 : ℕ
⊢ 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))
have inr : ∀ (i : (t n ∩ s).Nonempty),
  ediam (f '' (t n ∩ s)) ^ d ≤ ⨆ (_ : (t n).Nonempty), (↑C : ℝ≥0∞) ^ d * ediam (t n) ^ ((↑r : ℝ) * d)
Tactic: simp only [iSup_le_iff, image_nonempty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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
⊢ ediam (f '' (t n ∩ s)) ^ d ≤ ⨆ (_ : (t n).Nonempty), (↑C : ℝ≥0∞) ^ d * ediam (t n) ^ ((↑r : ℝ) * d)
have inr : ediam (f '' (t n ∩ s)) ^ d ≤ (↑C : ℝ≥0∞) ^ d * ediam (t n) ^ ((↑r : ℝ) * d)
Tactic: simp only [Nonempty.mono ((t n).inter_subset_left) hft, ciSup_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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
⊢ ediam (f '' (t n ∩ s)) ^ d ≤ (↑C : ℝ≥0∞) ^ d * ediam (t n) ^ ((↑r : ℝ) * d)
have inr : ediam (f '' (t n ∩ s)) ^ d ≤ ((↑C : ℝ≥0∞) * ediam (t n) ^ (↑r : ℝ)) ^ d
Tactic: rw [ENNReal.rpow_mul, ← ENNReal.mul_rpow_of_nonneg _ _ hd]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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
⊢ ediam (f '' (t n ∩ s)) ^ d ≤ ((↑C : ℝ≥0∞) * ediam (t n) ^ (↑r : ℝ)) ^ d
have inr : ediam (f '' (t n ∩ s)) ≤ (↑C : ℝ≥0∞) * ediam (t n) ^ (↑r : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
𝕜 : Type u_4
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
⊢ ((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) (r • s) =
    HSMul.hSMul (β := ℝ≥0∞) (‖r‖₊ ^ d) (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have this : ∀ {r : 𝕜} (s : Set E),
  ((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) (r • s) ≤
    HSMul.hSMul (β := ℝ≥0∞) (‖r‖₊ ^ d) (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: have {r : 𝕜} (s : Set E) : μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s := by
    simpa [ENNReal.coe_rpow_of_nonneg, hd]
      using (lipschitzWith_smul r).hausdorffMeasure_image_le hd s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this :
  ∀ {r : 𝕜} (s : Set E),
    ((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) (r • s) ≤
      HSMul.hSMul (β := ℝ≥0∞) (‖r‖₊ ^ d) (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) (r • s) =
    HSMul.hSMul (β := ℝ≥0∞) (‖r‖₊ ^ d) (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have refine : HSMul.hSMul (β := ℝ≥0∞) (‖r‖₊ ^ d) (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ≤
  ((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) (r • s)
Tactic: refine le_antisymm (this s) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this :
  ∀ {r : 𝕜} (s : Set E),
    ((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) (r • s) ≤
      HSMul.hSMul (β := ℝ≥0∞) (‖r‖₊ ^ d) (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ HSMul.hSMul (β := ℝ≥0∞) (‖r‖₊ ^ d) (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ≤
    ((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) (r • s)
have rw : ((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) s ≤
  HSMul.hSMul (β := ℝ≥0∞) (‖r‖₊ ^ d)⁻¹ (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) (r • s) : ℝ≥0∞)
Tactic: rw [← le_inv_smul_iff_of_pos]