awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H :
  Ne (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0
hc : c ≠ 0
this_1 : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
r : ℝ≥0
hr₀_1 : 0 ≤ (↑r : ℝ≥0∞)
hrc : (↑r : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
hr₀ : r ≠ 0
this : (↑r : ℝ≥0∞) ≠ 0
⊢ ((↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹) ^ (d₂ - d₁) ≤ (↑c : ℝ≥0∞)
have h₁ : (↑c : ℝ≥0∞) ^ ((d₂ - d₁)⁻¹ * (d₂ - d₁)) ≤ (↑c : ℝ≥0∞)
Tactic: rw [← ENNReal.rpow_mul, inv_mul_cancel₀ (sub_pos.2 h).ne', ENNReal.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H :
  Ne (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0
hc : c ≠ 0
this_1 : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
r : ℝ≥0
hr₀_1 : 0 ≤ (↑r : ℝ≥0∞)
hrc : (↑r : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
hr₀ : r ≠ 0
this : (↑r : ℝ≥0∞) ≠ 0
h₁ : (↑c : ℝ≥0∞) ^ ((d₂ - d₁)⁻¹ * (d₂ - d₁)) ≤ (↑c : ℝ≥0∞)
⊢ ((↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹) ^ (d₂ - d₁) ≤ (↑c : ℝ≥0∞)
have h₂ : HPow.hPow (β := ℝ) (↑c : ℝ≥0∞) 1 ≤ (↑c : ℝ≥0∞)
Tactic: rw [← ENNReal.rpow_mul, inv_mul_cancel₀ (sub_pos.2 h).ne', ENNReal.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H :
  Ne (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0
hc : c ≠ 0
this_1 : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
r : ℝ≥0
hr₀_1 : 0 ≤ (↑r : ℝ≥0∞)
hrc : (↑r : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
hr₀ : r ≠ 0
this : (↑r : ℝ≥0∞) ≠ 0
h₁ : (↑c : ℝ≥0∞) ^ ((d₂ - d₁)⁻¹ * (d₂ - d₁)) ≤ (↑c : ℝ≥0∞)
h₂ : HPow.hPow (β := ℝ) (↑c : ℝ≥0∞) 1 ≤ (↑c : ℝ≥0∞)
⊢ ((↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹) ^ (d₂ - d₁) ≤ (↑c : ℝ≥0∞)
have h₃ : (↑c : ℝ≥0∞) ≤ (↑c : ℝ≥0∞)
Tactic: rw [← ENNReal.rpow_mul, inv_mul_cancel₀ (sub_pos.2 h).ne', ENNReal.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ ≤ d₂
s : Set X
⊢ LE.le (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have inl : ∀ (h : d₁ ≤ d₁),
  LE.le (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rcases h.eq_or_lt with (rfl | h)
Cleared hypotheses: d₂, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ ≤ d₂
s : Set X
inl :
  ∀ (h : d₁ ≤ d₁),
    LE.le (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
      (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have inr : ∀ (h : d₁ < d₂),
  LE.le (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rcases h.eq_or_lt with (rfl | h)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h_1 : d₁ ≤ d₂
s : Set X
h : d₁ < d₂
⊢ LE.le (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have inr : ∀ (hs : Eq (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  LE.le (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rcases hausdorffMeasure_zero_or_top h s with hs | hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h_1 : d₁ ≤ d₂
s : Set X
h : d₁ < d₂
inr :
  ∀ (hs : Eq (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
      (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have inr₁ : ∀ (hs : Eq (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  LE.le (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rcases hausdorffMeasure_zero_or_top h s with hs | hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d : ℝ
hd : 0 < d
⊢ NoAtoms.{u_2} (α := X) (m0 := inst_1) μH[d]
have refine : ∀ (x : X), Eq (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨fun x => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d : ℝ
hd : 0 < d
x : X
⊢ Eq (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞)
  (⨆ (r : ℝ≥0∞),
    ⨆ (_ : 0 < r),
      ⨅ (t : ℕ → Set X),
        ⨅ (_ : Subset (α := Set X) {x} (⋃ (n : ℕ), t n)),
          ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d)
  0
Tactic: rw [← nonpos_iff_eq_zero, hausdorffMeasure_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d : ℝ
hd : 0 < d
x : X
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : 0 < r),
        ⨅ (t : ℕ → Set X),
          ⨅ (_ : Subset (α := Set X) {x} (⋃ (n : ℕ), t n)),
            ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d)
    0
have refine_1 : ∀ (ε : ℝ≥0∞), 0 < ε → Subset (α := Set X) {x} (⋃ (n : ℕ), (fun (x_2 : ℕ) ↦ ({x} : Set X)) n)
Tactic: refine iSup₂_le fun ε _ => iInf₂_le_of_le (fun _ => {x}) ?_ <| iInf_le_of_le (fun _ => ?_) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d : ℝ
hd : 0 < d
x : X
refine_1 : ∀ (ε : ℝ≥0∞), 0 < ε → Subset (α := Set X) {x} (⋃ (n : ℕ), (fun (x_2 : ℕ) ↦ ({x} : Set X)) n)
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : 0 < r),
        ⨅ (t : ℕ → Set X),
          ⨅ (_ : Subset (α := Set X) {x} (⋃ (n : ℕ), t n)),
            ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d)
    0
have refine_2 : ∀ (ε : ℝ≥0∞), 0 < ε → ∀ (x_2 : ℕ), ediam.{u_2} (X := X) ((fun (x_3 : ℕ) ↦ ({x} : Set X)) x_2) ≤ ε
Tactic: refine iSup₂_le fun ε _ => iInf₂_le_of_le (fun _ => {x}) ?_ <| iInf_le_of_le (fun _ => ?_) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d : ℝ
hd : 0 < d
x : X
refine_1 : ∀ (ε : ℝ≥0∞), 0 < ε → Subset (α := Set X) {x} (⋃ (n : ℕ), (fun (x_2 : ℕ) ↦ ({x} : Set X)) n)
refine_2 : ∀ (ε : ℝ≥0∞), 0 < ε → ∀ (x_2 : ℕ), ediam.{u_2} (X := X) ((fun (x_3 : ℕ) ↦ ({x} : Set X)) x_2) ≤ ε
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : 0 < r),
        ⨅ (t : ℕ → Set X),
          ⨅ (_ : Subset (α := Set X) {x} (⋃ (n : ℕ), t n)),
            ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d)
    0
have refine_3 : ∀ (ε : ℝ≥0∞),
  0 < ε →
    LE.le (α := ℝ≥0∞)
      (∑' (n : ℕ),
        ⨆ (_ : Set.Nonempty.{u_2} (α := X) ((fun (x_2 : ℕ) ↦ ({x} : Set X)) n)),
          ediam.{u_2} (X := X) ((fun (x_3 : ℕ) ↦ ({x} : Set X)) n) ^ d)
      0
Tactic: refine iSup₂_le fun ε _ => iInf₂_le_of_le (fun _ => {x}) ?_ <| iInf_le_of_le (fun _ => ?_) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
x : X
⊢ Eq (α := ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (1 : ℝ≥0∞)
have a : LE.le (α := ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
x : X
a : LE.le (α := ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (1 : ℝ≥0∞)
have a₁ : LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
x : X
r : ℕ → ℝ≥0∞ := fun (x : ℕ) ↦ 0
t : ℕ → Unit → Set X := fun (x_1 : ℕ) (x_2 : Unit) ↦ {x}
⊢ LE.le (α := ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (1 : ℝ≥0∞)
have ht : ∀ᶠ (n : ℕ) in atTop, ∀ (i : Unit), ediam (t n i) ≤ r n
Tactic: have ht : ∀ᶠ n in atTop, ∀ i, ediam (t n i) ≤ r n := by
      simp only [t, r, imp_true_iff, ediam_singleton, eventually_atTop,
        nonpos_iff_eq_zero, exists_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
x : X
⊢ LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞)
have a : LE.le (α := ℝ≥0∞) 1
  (⨆ (r : ℝ≥0∞),
    ⨆ (_ : 0 < r),
      ⨅ (t : ℕ → Set X),
        ⨅ (_ : Subset (α := Set X) {x} (⋃ (n : ℕ), t n)),
          ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), HPow.hPow (β := ℝ) (ediam (t n)) 0)
Tactic: rw [hausdorffMeasure_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
x : X
this :
  LE.le (α := ℝ≥0∞) 1
    (⨅ (t : ℕ → Set X),
      ⨅ (_ : Subset (α := Set X) {x} (⋃ (n : ℕ), t n)),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), HPow.hPow (β := ℝ) (ediam (t n)) 0)
⊢ LE.le (α := ℝ≥0∞) 1
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : 0 < r),
        ⨅ (t : ℕ → Set X),
          ⨅ (_ : Subset (α := Set X) {x} (⋃ (n : ℕ), t n)),
            ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), HPow.hPow (β := ℝ) (ediam (t n)) 0)
have apply : LE.le (α := ℝ≥0∞)
  (⨅ (t : ℕ → Set X),
    ⨅ (_ : Subset (α := Set X) {x} (⋃ (n : ℕ), t n)),
      ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), HPow.hPow (β := ℝ) (ediam (t n)) 0)
  (⨆ (r : ℝ≥0∞),
    ⨆ (_ : 0 < r),
      ⨅ (t : ℕ → Set X),
        ⨅ (_ : Subset (α := Set X) {x} (⋃ (n : ℕ), t n)),
          ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), HPow.hPow (β := ℝ) (ediam (t n)) 0)
Tactic: apply le_trans this _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
x : X
this :
  LE.le (α := ℝ≥0∞) 1
    (⨅ (t : ℕ → Set X),
      ⨅ (_ : Subset (α := Set X) {x} (⋃ (n : ℕ), t n)),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), HPow.hPow (β := ℝ) (ediam (t n)) 0)
⊢ LE.le (α := ℝ≥0∞)
    (⨅ (t : ℕ → Set X),
      ⨅ (_ : Subset (α := Set X) {x} (⋃ (n : ℕ), t n)),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), HPow.hPow (β := ℝ) (ediam (t n)) 0)
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : 0 < r),
        ⨅ (t : ℕ → Set X),
          ⨅ (_ : Subset (α := Set X) {x} (⋃ (n : ℕ), t n)),
            ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), HPow.hPow (β := ℝ) (ediam (t n)) 0)
have h : Eq (α := ℝ≥0∞)
  (⨅ (t : ℕ → Set X),
    ⨅ (_ : Subset (α := Set X) {x} (⋃ (n : ℕ), t n)),
      ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), HPow.hPow (β := ℝ) (ediam (t n)) 0)
  (⨅ (t : ℕ → Set X),
    ⨅ (_ : Subset (α := Set X) {x} (⋃ (n : ℕ), t n)),
      ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), HPow.hPow (β := ℝ) (ediam (t n)) 0)
Tactic: convert! le_iSup₂ (α := ℝ≥0∞) (1 : ℝ≥0∞) zero_lt_one
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
x : X
⊢ LE.le (α := ℝ≥0∞) 1
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : 0 < r),
        ⨅ (t : ℕ → Set X),
          ⨅ (_ : Subset (α := Set X) {x} (⋃ (n : ℕ), t n)),
            ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), HPow.hPow (β := ℝ) (ediam (t n)) 0)
have a : LE.le (α := ℝ≥0∞) 1
  (⨅ (t : ℕ → Set X),
    ⨅ (_ : Subset (α := Set X) {x} (⋃ (n : ℕ), t n)),
      ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), HPow.hPow (β := ℝ) (ediam (t n)) 0)
Tactic: suffices
      (1 : ℝ≥0∞) ≤
        ⨅ (t : ℕ → Set X) (_ : {x} ⊆ ⋃ n, t n) (_ : ∀ n, ediam (t n) ≤ 1),
          ∑' n, ⨆ _ : (t n).Nonempty, ediam (t n) ^ (0 : ℝ) by
      apply le_trans this _
      convert! le_iSup₂ (α := ℝ≥0∞) (1 : ℝ≥0∞) zero_lt_one
      rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
x : X
⊢ LE.le (α := ℝ≥0∞) 1
    (⨅ (t : ℕ → Set X),
      ⨅ (_ : Subset (α := Set X) {x} (⋃ (n : ℕ), t n)),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), HPow.hPow (β := ℝ) (ediam (t n)) 0)
have a : ∀ (i : ℕ → Set X) (i_1 : Subset (α := Set X) {x} (⋃ (n : ℕ), i n)) (i_2 : ∀ (n : ℕ), ediam (i n) ≤ 1),
  LE.le (α := ℝ≥0∞) 1 (∑' (n : ℕ), ⨆ (_ : (i n).Nonempty), 1)
Tactic: simp only [ENNReal.rpow_zero, le_iInf_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
x : X
t : ℕ → Set X
hst : Subset (α := Set X) {x} (⋃ (n : ℕ), t n)
i : ∀ (n : ℕ), ediam (t n) ≤ 1
⊢ LE.le (α := ℝ≥0∞) 1 (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), 1)
have a : ∀ (m : ℕ) (hm : x ∈ t m), LE.le (α := ℝ≥0∞) 1 (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), 1)
Tactic: rcases mem_iUnion.1 (hst (mem_singleton x)) with ⟨m, hm⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
x : X
t : ℕ → Set X
hst : Subset (α := Set X) {x} (⋃ (n : ℕ), t n)
i : ∀ (n : ℕ), ediam (t n) ≤ 1
m : ℕ
hm : x ∈ t m
⊢ LE.le (α := ℝ≥0∞) 1 (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), 1)
have A : (t m).Nonempty
Tactic: have A : (t m).Nonempty := ⟨x, hm⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
x : X
t : ℕ → Set X
hst : Subset (α := Set X) {x} (⋃ (n : ℕ), t n)
i : ∀ (n : ℕ), ediam (t n) ≤ 1
m : ℕ
hm : x ∈ t m
A : (t m).Nonempty
⊢ LE.le (α := ℝ≥0∞) 1 (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), 1)
have h : Eq (α := ℝ≥0∞) 1 (⨆ (_ : (t m).Nonempty), 1)
Tactic: calc
      (1 : ℝ≥0∞) = ⨆ h : (t m).Nonempty, 1 := by simp only [A, ciSup_pos]
      _ ≤ ∑' n, ⨆ h : (t n).Nonempty, 1 := ENNReal.le_tsum _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
h : s.Nonempty
⊢ LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have rcases : ∀ (x : X) (hx : x ∈ s), LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rcases h with ⟨x, hx⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
⊢ LE.le (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)
have inl : ∀ (hs : Set.Subsingleton.{u_2} (α := X) ∅), LE.le (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) ∅) 1
Tactic: rcases eq_empty_or_nonempty s with (rfl | ⟨x, hx⟩)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
inl : ∀ (hs : Set.Subsingleton.{u_2} (α := X) ∅), LE.le (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) ∅) 1
⊢ LE.le (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)
have inr : ∀ (x : X) (hx : x ∈ s), LE.le (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rcases eq_empty_or_nonempty s with (rfl | ⟨x, hx⟩)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
x : X
hx : x ∈ s
⊢ LE.le (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)
have inr : LE.le (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rw [(subsingleton_iff_singleton hx).1 hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
x : X
hx : x ∈ s
⊢ LE.le (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (1 : ℝ≥0∞)
have inr : ∀ (hd : LE.le (α := ℝ) 0 0), LE.le (α := ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rcases eq_or_lt_of_le hd with (rfl | dpos)
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
x : X
hx : x ∈ s
inr : ∀ (hd : LE.le (α := ℝ) 0 0), LE.le (α := ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (1 : ℝ≥0∞)
have inr₁ : ∀ (dpos : 0 < d), LE.le (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rcases eq_or_lt_of_le hd with (rfl | dpos)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
x : X
hx : x ∈ s
dpos : 0 < d
⊢ LE.le (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (1 : ℝ≥0∞)
have this : NoAtoms.{u_2} (α := X) (m0 := inst_1) μH[d]
Tactic: haveI := noAtoms_hausdorff X dpos
-- 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
⊢ ((μ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 inl : ∀ (h : HolderOnWith 0 r f s),
  ((μ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: rcases eq_zero_or_pos C with (rfl | hC0)
Cleared hypotheses: C, 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
inl :
  ∀ (h : HolderOnWith 0 r f s),
    ((μ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∞)
⊢ ((μ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 : ∀ (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∞)
Tactic: rcases eq_zero_or_pos C with (rfl | hC0)
-- 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
⊢ ((μ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∞)
have inl : ∀ (h : HolderOnWith 0 r f ∅),
  ((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' ∅) ≤
    (↑0 : ℝ≥0∞) ^ d * ((μH[(↑r : ℝ) * d] : Measure X) : (a : Set X) → ℝ≥0∞) ∅
Tactic: rcases eq_empty_or_nonempty s with (rfl | ⟨x, hx⟩)
Cleared hypotheses: s, 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
r : ℝ≥0
f : X → Y
s : Set X
hr : 0 < r
d : ℝ
hd : 0 ≤ d
h : HolderOnWith 0 r f s
inl :
  ∀ (h : HolderOnWith 0 r f ∅),
    ((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' ∅) ≤
      (↑0 : ℝ≥0∞) ^ d * ((μH[(↑r : ℝ) * d] : Measure X) : (a : Set X) → ℝ≥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∞)
have inl₁ : ∀ (x : X) (hx : x ∈ s),
  ((μ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: rcases eq_empty_or_nonempty s with (rfl | ⟨x, hx⟩)
-- 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
⊢ ((μ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∞)
have this : 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
-- 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 '' s) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑0 : ℝ≥0∞) ^ d) (((μH[(↑r : ℝ) * d] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
Tactic: rw [this]