-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem hausdorffMeasure_zero_singleton (x : X) : μH[0] ({x} : Set X) = 1

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
⊢ μH[0] {x} = 1

Tactic:
apply le_antisymm

Result:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
⊢ μH[0] {x} ≤ 1

case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
⊢ 1 ≤ μH[0] {x}

Proof state:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
r : ℕ → ℝ≥0∞ := fun x => 0
t : ℕ → Unit → Set X := fun x_1 x_2 => {x}
⊢ μH[0] {x} ≤ 1

Tactic:
have ht : ∀ᶠ n in atTop, ∀ i, diam (t n i) ≤ r n := by
  simp only [t, r, imp_true_iff, eq_self_iff_true, diam_singleton, eventually_atTop,
    nonpos_iff_eq_zero, exists_const]

Result:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
r : ℕ → ℝ≥0∞ := fun x => 0
t : ℕ → Unit → Set X := fun x_1 x_2 => {x}
ht : ∀ᶠ (n : ℕ) in atTop, ∀ (i : Unit), diam (t n i) ≤ r n
⊢ μH[0] {x} ≤ 1

Proof state:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
⊢ 1 ≤ μH[0] {x}

Tactic:
rw [hausdorffMeasure_apply]

Result:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
⊢ 1 ≤
    ⨆ r,
      ⨆ (_ : 0 < r),
        ⨅ t,
          ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ 0

Proof state:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
⊢ ∀ (i : ℕ → Set X), {x} ⊆ ⋃ n, i n → (∀ (n : ℕ), diam (i n) ≤ 1) → 1 ≤ ∑' (n : ℕ), ⨆ (_ : (i n).Nonempty), 1

Tactic:
intro t hst _

Result:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
t : ℕ → Set X
hst : {x} ⊆ ⋃ n, t n
i✝ : ∀ (n : ℕ), diam (t n) ≤ 1
⊢ 1 ≤ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), 1

Proof state:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
⊢ μH[0] {x} ≤ 1

Tactic:
let r : ℕ → ℝ≥0∞ := fun _ => 0

Result:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
r : ℕ → ℝ≥0∞ := fun x => 0
⊢ μH[0] {x} ≤ 1

Proof state:
case a.intro
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
t : ℕ → Set X
hst : {x} ⊆ ⋃ n, t n
i✝ : ∀ (n : ℕ), diam (t n) ≤ 1
m : ℕ
hm : x ∈ t m
A : (t m).Nonempty
⊢ 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 _

Result:
no goals

Proof state:
case a.intro
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
t : ℕ → Set X
hst : {x} ⊆ ⋃ n, t n
i✝ : ∀ (n : ℕ), diam (t n) ≤ 1
m : ℕ
hm : x ∈ t m
⊢ 1 ≤ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), 1

Tactic:
have A : (t m).Nonempty := ⟨x, hm⟩

Result:
case a.intro
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
t : ℕ → Set X
hst : {x} ⊆ ⋃ n, t n
i✝ : ∀ (n : ℕ), diam (t n) ≤ 1
m : ℕ
hm : x ∈ t m
A : (t m).Nonempty
⊢ 1 ≤ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), 1

Proof state:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
⊢ 1 ≤ ⨅ t, ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ 0

Tactic:
simp only [ENNReal.rpow_zero, le_iInf_iff]

Result:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
⊢ ∀ (i : ℕ → Set X), {x} ⊆ ⋃ n, i n → (∀ (n : ℕ), diam (i n) ≤ 1) → 1 ≤ ∑' (n : ℕ), ⨆ (_ : (i n).Nonempty), 1

Proof state:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
t : ℕ → Set X
hst : {x} ⊆ ⋃ n, t n
i✝ : ∀ (n : ℕ), diam (t n) ≤ 1
⊢ 1 ≤ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), 1

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

Result:
case a.intro
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
t : ℕ → Set X
hst : {x} ⊆ ⋃ n, t n
i✝ : ∀ (n : ℕ), diam (t n) ≤ 1
m : ℕ
hm : x ∈ t m
⊢ 1 ≤ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), 1

Proof state:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
⊢ 1 ≤
    ⨆ r,
      ⨆ (_ : 0 < r),
        ⨅ t,
          ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ 0

Tactic:
suffices
  (1 : ℝ≥0∞) ≤
    ⨅ (t : ℕ → Set X) (_ : {x} ⊆ ⋃ n, t n) (_ : ∀ n, diam (t n) ≤ 1),
      ∑' n, ⨆ _ : (t n).Nonempty, diam (t n) ^ (0 : ℝ) by
  apply le_trans this _
  convert le_iSup₂ (α := ℝ≥0∞) (1 : ℝ≥0∞) zero_lt_one
  rfl

Result:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
⊢ 1 ≤ ⨅ t, ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ 0

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
t : ℕ → Set X
hst : {x} ⊆ ⋃ n, t n
i✝ : ∀ (n : ℕ), diam (t n) ≤ 1
m : ℕ
hm : x ∈ t m
A : (t m).Nonempty
⊢ 1 = ⨆ (_ : (t m).Nonempty), 1

Tactic:
simp only [A, ciSup_pos]

Result:
no goals

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
r : ℕ → ℝ≥0∞ := fun x => 0
t : ℕ → Unit → Set X := fun x_1 x_2 => {x}
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : Unit), diam (t n i) ≤ r n

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

Result:
no goals

Proof state:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
r : ℕ → ℝ≥0∞ := fun x => 0
⊢ μH[0] {x} ≤ 1

Tactic:
let t : ℕ → Unit → Set X := fun _ _ => {x}

Result:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
r : ℕ → ℝ≥0∞ := fun x => 0
t : ℕ → Unit → Set X := fun x_1 x_2 => {x}
⊢ μH[0] {x} ≤ 1

Proof state:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
r : ℕ → ℝ≥0∞ := fun x => 0
t : ℕ → Unit → Set X := fun x_1 x_2 => {x}
ht : ∀ᶠ (n : ℕ) in atTop, ∀ (i : Unit), diam (t n i) ≤ r n
⊢ μH[0] {x} ≤ 1

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

Result:
no goals

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
this :
  1 ≤ ⨅ t, ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ 0
⊢ ⨅ t, ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ 0 ≤
    ⨆ r,
      ⨆ (_ : 0 < r),
        ⨅ t,
          ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ 0

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

Result:
case h.e'_3
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
this :
  1 ≤ ⨅ t, ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ 0
⊢ ⨅ t, ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ 0 =
    ⨅ t, ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ 0