awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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₂
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:
simp [hs]
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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]

Tactic:
⟨fun x => ?_⟩

Premises used: MeasureTheory.NoAtoms.mk
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d : ℝ
hd : 0 < d
refine : ∀ (x : X), Eq (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NoAtoms.{u_2} (α := X) (m0 := inst_1) μH[d]

Tactic:
refine ⟨fun x => ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d : ℝ
hd : 0 < d
x : X
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
⊢ Eq (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← nonpos_iff_eq_zero, hausdorffMeasure_apply]

Premises used: MeasureTheory.Measure.hausdorffMeasure_apply, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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

Tactic:
iSup₂_le fun ε _ => iInf₂_le_of_le (fun _ => {x}) ?_ <| iInf_le_of_le (fun _ => ?_) ?_

Premises used: iSup₂_le, iInf₂_le_of_le, iInf_le_of_le, Singleton.singleton
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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) ≤ ε
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
⊢ 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:
refine iSup₂_le fun ε _ => iInf₂_le_of_le (fun _ => {x}) ?_ <| iInf_le_of_le (fun _ => ?_) ?_

Premises used: iSup₂_le, iInf₂_le_of_le
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d : ℝ
hd : 0 < d
x : X
ε : ℝ≥0∞
h : 0 < ε
⊢ Subset (α := Set X) {x} (⋃ (n : ℕ), (fun (x_1 : ℕ) ↦ ({x} : Set X)) n)

Tactic:
subset_iUnion (fun _ => {x} : ℕ → Set X) 0

Premises used: Set.subset_iUnion, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d : ℝ
hd : 0 < d
x : X
ε : ℝ≥0∞
h : 0 < ε
⊢ Subset (α := Set X) {x} (⋃ (n : ℕ), (fun (x_1 : ℕ) ↦ ({x} : Set X)) n)

Tactic:
exact subset_iUnion (fun _ => {x} : ℕ → Set X) 0

Premises used: Set.subset_iUnion, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d : ℝ
hd : 0 < d
x : X
ε : ℝ≥0∞
h : 0 < ε
x_1 : ℕ
⊢ ediam.{u_2} (X := X) ((fun (x_2 : ℕ) ↦ ({x} : Set X)) x_1) ≤ ε

Tactic:
simp only [ediam_singleton, zero_le]

Premises used: zero_le, Metric.ediam_singleton
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d : ℝ
hd : 0 < d
x : X
ε : ℝ≥0∞
h : 0 < ε
⊢ LE.le (α := ℝ≥0∞)
    (∑' (n : ℕ),
      ⨆ (_ : Set.Nonempty.{u_2} (α := X) ((fun (x_1 : ℕ) ↦ ({x} : Set X)) n)),
        ediam.{u_2} (X := X) ((fun (x_2 : ℕ) ↦ ({x} : Set X)) n) ^ d)
    0

Tactic:
simp [hd]
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
a₁ : LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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}
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : Unit), ediam (t n i) ≤ r n

Tactic:
simp only [t, r, imp_true_iff, ediam_singleton, eventually_atTop,
        nonpos_iff_eq_zero, exists_const]

Premises used: imp_true_iff, exists_const, Filter.eventually_atTop, Metric.ediam_singleton, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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}
⊢ ∀ᶠ (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]
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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}
ht : ∀ᶠ (n : ℕ) in atTop, ∀ (i : Unit), ediam (t n i) ≤ r n
⊢ LE.le (α := ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simpa [t, liminf_const] using hausdorffMeasure_le_liminf_sum 0 {x} r tendsto_const_nhds t ht

Premises used: MeasureTheory.Measure.hausdorffMeasure_le_liminf_sum, tendsto_const_nhds, Filter.liminf_const, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
x : X
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)
⊢ LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞)

Tactic:
rw [hausdorffMeasure_apply]

Premises used: MeasureTheory.Measure.hausdorffMeasure_apply
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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)
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)
⊢ 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:
apply le_trans this _

Premises used: le_trans
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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)
    (⨆ (i : ℝ≥0∞),
      ⨆ (_ : 0 < i),
        ⨅ (t : ℕ → Set X),
          ⨅ (_ : Subset (α := Set X) {x} (⋃ (n : ℕ), t n)),
            ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ i), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), HPow.hPow (β := ℝ) (ediam (t n)) 0)

Tactic:
le_iSup₂ (α := ℝ≥0∞) (1 : ℝ≥0∞) zero_lt_one

Premises used: le_iSup₂, zero_lt_one, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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)
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)
⊢ 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:
convert! le_iSup₂ (α := ℝ≥0∞) (1 : ℝ≥0∞) zero_lt_one

Premises used: le_iSup₂, zero_lt_one, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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)
⊢ 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:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
x : X
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)
⊢ 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:
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
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
x : X
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)
⊢ 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:
simp only [ENNReal.rpow_zero, le_iInf_iff]

Premises used: le_iInf_iff, ENNReal.rpow_zero
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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)
a : (∀ (n : ℕ), ediam (t n) ≤ 1) → LE.le (α := ℝ≥0∞) 1 (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), 1)
⊢ ∀ (i : ∀ (n : ℕ), ediam (t n) ≤ 1), LE.le (α := ℝ≥0∞) 1 (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), 1)

Tactic:
_
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
a : ∀ (m : ℕ) (hm : x ∈ t m), LE.le (α := ℝ≥0∞) 1 (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), 1)
⊢ LE.le (α := ℝ≥0∞) 1 (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), 1)

Tactic:
rcases mem_iUnion.1 (hst (mem_singleton x)) with ⟨m, hm⟩

Premises used: Set.mem_singleton, Set.mem_iUnion, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
⊢ (t m).Nonempty

Tactic:
have A : (t m).Nonempty := ⟨x, hm⟩
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
⊢ Eq (α := ℝ≥0∞) 1 (⨆ (_ : (t m).Nonempty), 1)

Tactic:
simp only [A, ciSup_pos]

Premises used: ciSup_pos
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞) (⨆ (_ : (t m).Nonempty), 1) (∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), 1)

Tactic:
ENNReal.le_tsum _

Premises used: ENNReal.le_tsum
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
h : Eq (α := ℝ≥0∞) 1 (⨆ (_ : (t m).Nonempty), 1)
⊢ LE.le (α := ℝ≥0∞) 1 (∑' (n : ℕ), ⨆ (_ : (t n).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 _

Premises used: ENNReal.le_tsum, Set.Nonempty, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
h : s.Nonempty
rcases : ∀ (x : X) (hx : x ∈ s), LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rcases h with ⟨x, hx⟩
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
x : X
hx : x ∈ s
⊢ Eq (α := ℝ≥0∞) (1 : ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞)

Tactic:
(hausdorffMeasure_zero_singleton x).symm

Premises used: MeasureTheory.Measure.hausdorffMeasure_zero_singleton, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
x : X
hx : x ∈ s
⊢ LE.le (α := ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞)
    (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
measure_mono (singleton_subset_iff.2 hx)

Premises used: Iff.mpr, Set.singleton_subset_iff, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
x : X
hx : x ∈ s
⊢ LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
calc
    (1 : ℝ≥0∞) = μH[0] ({x} : Set X) := (hausdorffMeasure_zero_singleton x).symm
    _ ≤ μH[0] s := measure_mono (singleton_subset_iff.2 hx)

Premises used: Iff.mpr, Set.singleton_subset_iff, MeasureTheory.Measure.hausdorffMeasure_zero_singleton, MeasureTheory.Measure.hausdorffMeasure, MeasureTheory.measure_mono, Singleton.singleton, OfNat.ofNat, Eq.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
inr : ∀ (x : X) (hx : x ∈ s), LE.le (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ 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⟩)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d : ℝ
hd : 0 ≤ d
hs : Set.Subsingleton.{u_2} (α := X) ∅
⊢ LE.le (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) ∅) 1

Tactic:
simp only [measure_empty, zero_le]

Premises used: zero_le, MeasureTheory.measure_empty
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 : LE.le (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rw [(subsingleton_iff_singleton hx).1 hs]

Premises used: Set.subsingleton_iff_singleton, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
inr₁ : ∀ (dpos : 0 < d), LE.le (α := ℝ≥0∞) (((μH[d] : 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∞)

Tactic:
rcases eq_or_lt_of_le hd with (rfl | dpos)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
s : Set X
hs : s.Subsingleton
x : X
hx : x ∈ s
hd : LE.le (α := ℝ) 0 0
⊢ LE.le (α := ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp only [le_refl, hausdorffMeasure_zero_singleton]

Premises used: MeasureTheory.Measure.hausdorffMeasure_zero_singleton, le_refl
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
⊢ NoAtoms.{u_2} (α := X) (m0 := inst_1) μH[d]

Tactic:
haveI := noAtoms_hausdorff X dpos
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
this : NoAtoms.{u_2} (α := X) (m0 := inst_1) μH[d]
⊢ LE.le (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (1 : ℝ≥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
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∞)
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∞)
⊢ ((μ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)

Premises used: eq_zero_or_pos, 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
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∞) ∅
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∞)
⊢ ((μ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⟩)

Premises used: Set.eq_empty_or_nonempty, 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
hr : 0 < r
d : ℝ
hd : 0 ≤ d
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:
simp only [measure_empty, nonpos_iff_eq_zero, mul_zero, image_empty]

Premises used: MeasureTheory.measure_empty, MulZeroClass.mul_zero, nonpos_iff_eq_zero, Set.image_empty
-- 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).Subsingleton

Tactic:
simpa [ediam_eq_zero_iff] using h.ediam_image_le

Premises used: Metric.ediam_eq_zero_iff, HolderOnWith.ediam_image_le