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
β : Type u_4
ι : β → Type u_5
inst_3 : ∀ (n : β), Countable.{u_5 + 1} (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ (i : ι n), t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
c : ℝ≥0∞
hc : liminf (fun (n : β) ↦ ∑' (i : ι n), m (ediam (t n i))) l < c
n : β
hn : ∑' (i : ι n), m (ediam (t n i)) < c
hrn : r n < ε
htn : ∀ (i : ι n), ediam (t n i) ≤ r n
hstn : s ⊆ ⋃ (i : ι n), t n i
u : ℕ → Set X := fun (j : ℕ) ↦ ⋃ (b : ι n), ⋃ (_ : Membership.mem (γ := Option (ι n)) (decode₂ (ι n) j) b), t n b
⊢ ∑' (n : ℕ), ⨆ (_ : (u n).Nonempty), m (ediam (u n)) ≤ c

Tactic:
calc
      (∑' j : ℕ, ⨆ _ : (u j).Nonempty, m (ediam (u j))) = _ :=
        tsum_iUnion_decode₂ (fun t : Set X => ⨆ _ : t.Nonempty, m (ediam t)) (by simp) _
      _ ≤ ∑' i : ι n, m (ediam (t n i)) := ENNReal.tsum_le_tsum fun b => iSup_le fun _ => le_rfl
      _ ≤ c := hn.le

Premises used: ENNReal.tsum_le_tsum, le_rfl, iSup, LT.lt.le, Metric.ediam, tsum_iUnion_decode₂, tsum, iSup_le, SummationFilter.unconditional
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
β : Type u_4
ι : β → Type u_5
hι : (n : β) → Fintype (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ (i : ι n), t n i
m : ℝ≥0∞ → ℝ≥0∞
⊢ LE.le (α := ℝ≥0∞) (((mkMetric m : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (liminf (fun (n : β) ↦ ∑ i : ι n, m (ediam (t n i))) l : ℝ≥0∞)

Tactic:
simpa only [tsum_fintype] using mkMetric_le_liminf_tsum s r hr t ht hst m

Premises used: MeasureTheory.Measure.mkMetric_le_liminf_tsum, tsum_fintype
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d : ℝ
μ : Measure X
ε : ℝ≥0∞
h₀ : 0 < ε
h : ∀ (s : Set X), ediam s ≤ ε → (μ : (a : Set X) → ℝ≥0∞) s ≤ ediam s ^ d
⊢ μ ≤ μH[d]

Tactic:
le_mkMetric _ μ ε h₀ h

Premises used: MeasureTheory.Measure.le_mkMetric
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d : ℝ
s : Set X
⊢ Eq (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (⨆ (r : ℝ≥0∞),
        ⨆ (_ : 0 < r),
          ⨅ (t : ℕ → Set X),
            ⨅ (_ : s ⊆ ⋃ (n : ℕ), t n),
              ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d :
      ℝ≥0∞)

Tactic:
mkMetric_apply _ _

Premises used: MeasureTheory.Measure.mkMetric_apply
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst_3 : ∀ (n : β), Countable.{u_5 + 1} (ι n)
d : ℝ
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ (i : ι n), t n i
⊢ LE.le (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (liminf (fun (n : β) ↦ ∑' (i : ι n), ediam (t n i) ^ d) l : ℝ≥0∞)

Tactic:
mkMetric_le_liminf_tsum s r hr t ht hst _

Premises used: MeasureTheory.Measure.mkMetric_le_liminf_tsum
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst_3 : (n : β) → Fintype (ι n)
d : ℝ
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ (i : ι n), t n i
⊢ LE.le (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    (liminf (fun (n : β) ↦ ∑ i : ι n, ediam (t n i) ^ d) l : ℝ≥0∞)

Tactic:
mkMetric_le_liminf_sum s r hr t ht hst _

Premises used: MeasureTheory.Measure.mkMetric_le_liminf_sum
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
by_contra! :
  ∀
    (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∞)),
    False
⊢ Eq (α := ℝ≥0∞) (((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
by_contra! H
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
this :
  ∀ (c : ℝ≥0),
    c ≠ 0 →
      ((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s ≤
        HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
rcases :
  ∀ (c : ℝ≥0) (hc0 : c > 0)
    (hc :
      HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) <
        ((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s),
    False
⊢ False

Tactic:
rcases ENNReal.exists_nnreal_pos_mul_lt H.2 H.1 with ⟨c, hc0, hc⟩

Premises used: ENNReal.exists_nnreal_pos_mul_lt, And.right, And.left
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
this :
  ∀ (c : ℝ≥0),
    c ≠ 0 →
      ((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s ≤
        HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
c : ℝ≥0
hc0 : c > 0
hc :
  HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) <
    ((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s
⊢ False

Tactic:
hc.not_ge (this c (pos_iff_ne_zero.1 hc0))

Premises used: Iff.mp, LT.lt.not_ge, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
this :
  ∀ (c : ℝ≥0),
    c ≠ 0 →
      ((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s ≤
        HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
c : ℝ≥0
hc0 : c > 0
hc :
  HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) <
    ((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s
⊢ False

Tactic:
exact hc.not_ge (this c (pos_iff_ne_zero.1 hc0))

Premises used: Iff.mp, LT.lt.not_ge, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
suffices :
  ∀ (c : ℝ≥0),
    c ≠ 0 →
      ((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s ≤
        HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ False

Tactic:
suffices ∀ c : ℝ≥0, c ≠ 0 → μH[d₂] s ≤ c * μH[d₁] s by
    rcases ENNReal.exists_nnreal_pos_mul_lt H.2 H.1 with ⟨c, hc0, hc⟩
    exact hc.not_ge (this c (pos_iff_ne_zero.1 hc0))
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
refine : (fun (r : ℝ≥0∞) ↦ r ^ d₂) ≤ᶠ[𝓝[≥] 0] HSMul.hSMul (β := ℝ≥0∞ → ℝ≥0∞) (↑c : ℝ≥0∞) fun (r : ℝ≥0∞) ↦ r ^ d₁
⊢ ((μH[d₂] : Measure X) : (a : Set X) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) (((μH[d₁] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
refine le_iff'.1 (mkMetric_mono_smul ENNReal.coe_ne_top (mod_cast hc) ?_) s

Premises used: MeasureTheory.Measure.le_iff', Iff.mp, MeasureTheory.Measure.mkMetric_mono_smul, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
rw : ¬(c = 0 ∧ (d₂ - d₁)⁻¹ ≠ 0)
⊢ 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹

Tactic:
rw [← ENNReal.coe_rpow_of_ne_zero hc, pos_iff_ne_zero, Ne, ENNReal.coe_eq_zero,
      NNReal.rpow_eq_zero_iff]

Premises used: Ne, ENNReal.coe_eq_zero, ENNReal.coe_rpow_of_ne_zero, NNReal.rpow_eq_zero_iff, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
⊢ ¬(c = 0 ∧ (d₂ - d₁)⁻¹ ≠ 0)

Tactic:
mt And.left hc

Premises used: mt, And.left
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
⊢ ¬(c = 0 ∧ (d₂ - d₁)⁻¹ ≠ 0)

Tactic:
exact mt And.left hc

Premises used: mt, And.left
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
⊢ 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹

Tactic:
have : 0 < ((c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹) := by
    rw [← ENNReal.coe_rpow_of_ne_zero hc, pos_iff_ne_zero, Ne, ENNReal.coe_eq_zero,
      NNReal.rpow_eq_zero_iff]
    exact mt And.left hc
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
h₁ :
  ∀ a ∈ Ico 0 ((↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹),
    a ^ d₂ ≤ HSMul.hSMul (β := ℝ≥0∞ → ℝ≥0∞) (↑c : ℝ≥0∞) (fun (r : ℝ≥0∞) ↦ r ^ d₁) a
⊢ (fun (r : ℝ≥0∞) ↦ r ^ d₂) ≤ᶠ[𝓝[≥] 0] HSMul.hSMul (β := ℝ≥0∞ → ℝ≥0∞) (↑c : ℝ≥0∞) fun (r : ℝ≥0∞) ↦ r ^ d₁

Tactic:
filter_upwards [Ico_mem_nhdsGE this]

Premises used: Ico_mem_nhdsGE
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
r : ℝ≥0∞
hr₀ : 0 ≤ r
hrc : r < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
⊢ r ≠ ∞

Tactic:
ne_top_of_lt hrc

Premises used: ne_top_of_lt
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
r : ℝ≥0∞
hr₀ : 0 ≤ r
hrc : r < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
h₁ :
  ∀ (r : ℝ≥0) (hr₀ : 0 ≤ (↑r : ℝ≥0∞)) (hrc : (↑r : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹),
    (↑r : ℝ≥0∞) ^ d₂ ≤ HSMul.hSMul (β := ℝ≥0∞ → ℝ≥0∞) (↑c : ℝ≥0∞) (fun (r : ℝ≥0∞) ↦ r ^ d₁) (↑r : ℝ≥0∞)
⊢ r ^ d₂ ≤ HSMul.hSMul (β := ℝ≥0∞ → ℝ≥0∞) (↑c : ℝ≥0∞) (fun (r : ℝ≥0∞) ↦ r ^ d₁) r

Tactic:
lift r to ℝ≥0 using ne_top_of_lt hrc

Premises used: ne_top_of_lt
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
r : ℝ≥0
hr₀ : 0 ≤ (↑r : ℝ≥0∞)
hrc : (↑r : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
h₁ : (↑r : ℝ≥0∞) ^ d₂ / (↑r : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)
⊢ (↑r : ℝ≥0∞) ^ d₂ ≤ HSMul.hSMul (β := ℝ≥0∞ → ℝ≥0∞) (↑c : ℝ≥0∞) (fun (r : ℝ≥0∞) ↦ r ^ d₁) (↑r : ℝ≥0∞)

Tactic:
rw [Pi.smul_apply, smul_eq_mul,
    ← ENNReal.div_le_iff_le_mul (Or.inr ENNReal.coe_ne_top) (Or.inr <| mt ENNReal.coe_eq_zero.1 hc)]

Premises used: ENNReal.div_le_iff_le_mul, mt, ENNReal.coe_eq_zero, Iff.mp, smul_eq_mul, Or.inr, ENNReal.coe_ne_top, Pi.smul_apply
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
r : ℝ≥0
hr₀ : 0 ≤ (↑r : ℝ≥0∞)
hrc : (↑r : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
h₁ :
  ∀ (hr₀ : 0 ≤ (↑0 : ℝ≥0∞)) (hrc : (↑0 : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹),
    (↑0 : ℝ≥0∞) ^ d₂ / (↑0 : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)
h₂ : ∀ (hr₀ : r ≠ 0), (↑r : ℝ≥0∞) ^ d₂ / (↑r : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)
⊢ (↑r : ℝ≥0∞) ^ d₂ / (↑r : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)

Tactic:
rcases eq_or_ne r 0 with (rfl | hr₀)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
hr₀ : 0 ≤ (↑0 : ℝ≥0∞)
hrc : (↑0 : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
h₁ : ∀ (h₂ : 0 < d₂), (↑0 : ℝ≥0∞) ^ d₂ / (↑0 : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)
h₂ : ∀ (h₂ : d₂ ≤ 0), (↑0 : ℝ≥0∞) ^ d₂ / (↑0 : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)
⊢ (↑0 : ℝ≥0∞) ^ d₂ / (↑0 : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)

Tactic:
rcases lt_or_ge 0 d₂ with (h₂ | h₂)

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
hr₀ : 0 ≤ (↑0 : ℝ≥0∞)
hrc : (↑0 : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
h₂ : 0 < d₂
⊢ (↑0 : ℝ≥0∞) ^ d₂ / (↑0 : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)

Tactic:
simp only [h₂, ENNReal.zero_rpow_of_pos, zero_le, ENNReal.zero_div, ENNReal.coe_zero]

Premises used: zero_le, ENNReal.zero_rpow_of_pos, ENNReal.zero_div, ENNReal.coe_zero
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
hr₀ : 0 ≤ (↑0 : ℝ≥0∞)
hrc : (↑0 : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
h₂ : d₂ ≤ 0
⊢ (↑0 : ℝ≥0∞) ^ d₂ / (↑0 : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)

Tactic:
simp only [h.trans_le h₂, ENNReal.div_top, zero_le, ENNReal.zero_rpow_of_neg,
        ENNReal.coe_zero]

Premises used: ENNReal.div_top, zero_le, ENNReal.coe_zero, ENNReal.zero_rpow_of_neg, LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
r : ℝ≥0
hr₀_1 : 0 ≤ (↑r : ℝ≥0∞)
hrc : (↑r : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
hr₀ : r ≠ 0
⊢ (↑r : ℝ≥0∞) ≠ 0

Tactic:
simpa only [ENNReal.coe_eq_zero, Ne] using hr₀

Premises used: Ne, ENNReal.coe_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 : 0 < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
r : ℝ≥0
hr₀_1 : 0 ≤ (↑r : ℝ≥0∞)
hrc : (↑r : ℝ≥0∞) < (↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹
hr₀ : r ≠ 0
⊢ (↑r : ℝ≥0∞) ≠ 0

Tactic:
have : (r : ℝ≥0∞) ≠ 0 := by simpa only [ENNReal.coe_eq_zero, Ne] using hr₀
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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₁ : (↑r : ℝ≥0∞) ^ (d₂ - d₁) ≤ (↑c : ℝ≥0∞)
⊢ (↑r : ℝ≥0∞) ^ d₂ / (↑r : ℝ≥0∞) ^ d₁ ≤ (↑c : ℝ≥0∞)

Tactic:
rw [← ENNReal.rpow_sub _ _ this ENNReal.coe_ne_top]

Premises used: ENNReal.rpow_sub, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
⊢ (↑r : ℝ≥0∞) ^ (d₂ - d₁) ≤ (↑c : ℝ≥0∞)

Tactic:
(ENNReal.rpow_lt_rpow hrc (sub_pos.2 h)).le.trans ?_

Premises used: Iff.mpr, sub_pos, LT.lt.le, ENNReal.rpow_lt_rpow, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
⊢ (↑r : ℝ≥0∞) ^ (d₂ - d₁) ≤ (↑c : ℝ≥0∞)

Tactic:
refine (ENNReal.rpow_lt_rpow hrc (sub_pos.2 h)).le.trans ?_

Premises used: Iff.mpr, sub_pos, LT.lt.le, ENNReal.rpow_lt_rpow, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
h₃ h₄ : (↑c : ℝ≥0∞) ≤ (↑c : ℝ≥0∞)
⊢ ((↑c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹) ^ (d₂ - d₁) ≤ (↑c : ℝ≥0∞)

Tactic:
rw [← ENNReal.rpow_mul, inv_mul_cancel₀ (sub_pos.2 h).ne', ENNReal.rpow_one]

Premises used: Iff.mpr, sub_pos, ENNReal.rpow_mul, ENNReal.rpow_one, LT.lt.ne', inv_mul_cancel₀
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
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∞)
⊢ 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)

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
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∞)

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
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∞)

Tactic:
exact le_rfl

Premises used: le_rfl
-- 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₂
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∞)
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∞)
⊢ 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

Premises used: MeasureTheory.Measure.hausdorffMeasure_zero_or_top
-- 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 : ℝ≥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]