awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)) ≤ (↑C : ℝ≥0∞) * ediam (t n) ^ (↑r : ℝ)

Tactic:
h.ediam_image_inter_le _

Premises used: HolderOnWith.ediam_image_inter_le
-- 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
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)) ≤ (↑C : ℝ≥0∞) * ediam (t n) ^ (↑r : ℝ)

Tactic:
exact h.ediam_image_inter_le _

Premises used: HolderOnWith.ediam_image_inter_le
-- 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
K : ℝ≥0
f : X → Y
s : Set X
h : LipschitzOnWith K f s
d : ℝ
hd : 0 ≤ d
⊢ ((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' s) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑K : ℝ≥0∞) ^ d) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simpa only [NNReal.coe_one, one_mul] using h.holderOnWith.hausdorffMeasure_image_le zero_lt_one hd

Premises used: zero_lt_one, LipschitzOnWith.holderOnWith, NNReal.coe_one, HolderOnWith.hausdorffMeasure_image_le, one_mul
-- 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
K : ℝ≥0
f : X → Y
h : LipschitzWith K f
d : ℝ
hd : 0 ≤ d
s : Set X
⊢ ((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' s) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑K : ℝ≥0∞) ^ d) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
h.lipschitzOnWith.hausdorffMeasure_image_le hd

Premises used: LipschitzOnWith.hausdorffMeasure_image_le, LipschitzWith.lipschitzOnWith
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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_1 : 𝕜
hr : r_1 ≠ 0
s_1 : Set E
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:
simpa [ENNReal.coe_rpow_of_nonneg, hd]
      using (lipschitzWith_smul r).hausdorffMeasure_image_le hd s

Premises used: ENNReal.coe_rpow_of_nonneg, LipschitzWith.hausdorffMeasure_image_le
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
⊢ ∀ {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
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)

Tactic:
le_antisymm (this s) ?_

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
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)
⊢ ((μ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:
refine le_antisymm (this s) ?_

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
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∞)
rw₁ : 0 < ‖r‖₊ ^ d
⊢ 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:
rw [← le_inv_smul_iff_of_pos]

Premises used: le_inv_smul_iff_of_pos
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
rw :
  ((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (↑(‖r⁻¹‖₊ ^ d) : ℝ≥0∞) (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) (r • s) : ℝ≥0∞)
⊢ ((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (↑(‖r‖₊ ^ d)⁻¹ : ℝ≥0∞) (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) (r • s) : ℝ≥0∞)

Tactic:
rw [← NNReal.inv_rpow, ← nnnorm_inv]

Premises used: nnnorm_inv, NNReal.inv_rpow
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (↑(‖r⁻¹‖₊ ^ d) : ℝ≥0∞) (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) (r • s) : ℝ≥0∞)

Tactic:
Eq.trans_le ?_ (this (r • s))

Premises used: Eq.trans_le, HSMul.hSMul
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
refine :
  Eq (α := ℝ≥0∞) (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) (r⁻¹ • r • s) : ℝ≥0∞)
⊢ ((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (↑(‖r⁻¹‖₊ ^ d) : ℝ≥0∞) (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) (r • s) : ℝ≥0∞)

Tactic:
refine Eq.trans_le ?_ (this (r • s))

Premises used: Eq.trans_le, HSMul.hSMul
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
rw rw₁ :
  Eq (α := ℝ≥0∞) (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) (r⁻¹ • r • s) : ℝ≥0∞)

Tactic:
rw [inv_smul_smul₀ hr]

Premises used: inv_smul_smul₀
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
⊢ 0 < ‖r‖₊ ^ d

Tactic:
simp [pos_iff_ne_zero, hr]

Premises used: pos_iff_ne_zero
-- 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
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
inl :
  ∀ (hf : AntilipschitzWith 0 f),
    ((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) ≤
      HMul.hMul (β := ℝ≥0∞) ((↑0 : ℝ≥0∞) ^ d) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
inr :
  ∀ (h0 : K ≠ 0),
    ((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) ≤
      HMul.hMul (β := ℝ≥0∞) ((↑K : ℝ≥0∞) ^ d) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑K : ℝ≥0∞) ^ d) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rcases eq_or_ne K 0 with (rfl | h0)

Premises used: eq_or_ne, OfNat.ofNat, 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
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
inl :
  ∀ (hs : f ⁻¹' s = ∅),
    ((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) ≤
      HMul.hMul (β := ℝ≥0∞) ((↑0 : ℝ≥0∞) ^ d) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
inl₁ :
  ∀ (x : X) (hx : x ∈ f ⁻¹' s),
    ((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) ≤
      HMul.hMul (β := ℝ≥0∞) ((↑0 : ℝ≥0∞) ^ d) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑0 : ℝ≥0∞) ^ d) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rcases eq_empty_or_nonempty (f ⁻¹' s) with (hs | ⟨x, hx⟩)

Premises used: Set.eq_empty_or_nonempty, Set.preimage
-- 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
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
hs : f ⁻¹' s = ∅
⊢ ((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑0 : ℝ≥0∞) ^ d) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [hs, measure_empty, zero_le]

Premises used: zero_le, MeasureTheory.measure_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
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
⊢ Subsingleton X

Tactic:
haveI : Subsingleton X := hf.subsingleton
-- 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
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
this : Subsingleton X
⊢ (f ⁻¹' s).Subsingleton

Tactic:
have : (f ⁻¹' s).Subsingleton := subsingleton_univ.anti (subset_univ _)
-- 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
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
this_1 : Subsingleton X
this : (f ⁻¹' s).Subsingleton
⊢ f ⁻¹' s = {x}

Tactic:
(subsingleton_iff_singleton hx).1 this

Premises used: Set.subsingleton_iff_singleton, Iff.mp
-- 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
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
this_1 : Subsingleton X
this : (f ⁻¹' s).Subsingleton
⊢ f ⁻¹' s = {x}

Tactic:
exact (subsingleton_iff_singleton hx).1 this

Premises used: Set.subsingleton_iff_singleton, Iff.mp
-- 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
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
⊢ f ⁻¹' s = {x}

Tactic:
have : f ⁻¹' s = {x} := by
      haveI : Subsingleton X := hf.subsingleton
      have : (f ⁻¹' s).Subsingleton := subsingleton_univ.anti (subset_univ _)
      exact (subsingleton_iff_singleton hx).1 this
-- 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
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
this : f ⁻¹' s = {x}
inl :
  ((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) {x} ≤
    HMul.hMul (β := ℝ≥0∞) ((↑0 : ℝ≥0∞) ^ d) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑0 : ℝ≥0∞) ^ d) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [this]
-- 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
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
this : f ⁻¹' s = {x}
inl :
  ∀ (hd : LE.le (α := ℝ) 0 0),
    ((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} ≤
      HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℝ) (↑0 : ℝ≥0∞) 0) (((μH[0] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
inl₁ :
  ∀ (h'd : 0 < d),
    ((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) {x} ≤
      HMul.hMul (β := ℝ≥0∞) ((↑0 : ℝ≥0∞) ^ d) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) {x} ≤
    HMul.hMul (β := ℝ≥0∞) ((↑0 : ℝ≥0∞) ^ d) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rcases eq_or_lt_of_le hd with (rfl | h'd)

Premises used: eq_or_lt_of_le, 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
f : X → Y
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
this : f ⁻¹' s = {x}
hd : LE.le (α := ℝ) 0 0
inl :
  LE.le (α := ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞)
    (((μH[0] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} ≤
    HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℝ) (↑0 : ℝ≥0∞) 0) (((μH[0] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [ENNReal.rpow_zero, one_mul]

Premises used: ENNReal.rpow_zero, one_mul
-- 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
f : X → Y
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
this : f ⁻¹' s = {x}
hd : LE.le (α := ℝ) 0 0
inl : LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) (((μH[0] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞)
    (((μH[0] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [hausdorffMeasure_zero_singleton]

Premises used: MeasureTheory.Measure.hausdorffMeasure_zero_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
f : X → Y
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
this : f ⁻¹' s = {x}
hd : LE.le (α := ℝ) 0 0
⊢ LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) (((μH[0] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
one_le_hausdorffMeasure_zero_of_nonempty ⟨f x, hx⟩

Premises used: MeasureTheory.Measure.one_le_hausdorffMeasure_zero_of_nonempty, Exists.intro
-- 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
f : X → Y
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
this : f ⁻¹' s = {x}
hd : LE.le (α := ℝ) 0 0
⊢ LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) (((μH[0] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact one_le_hausdorffMeasure_zero_of_nonempty ⟨f x, hx⟩

Premises used: MeasureTheory.Measure.one_le_hausdorffMeasure_zero_of_nonempty, Exists.intro
-- 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
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
this : f ⁻¹' s = {x}
h'd : 0 < d
⊢ NoAtoms.{u_2} (α := X) (m0 := inst_2) μH[d]

Tactic:
haveI := noAtoms_hausdorff X h'd
-- 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
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
this_1 : f ⁻¹' s = {x}
h'd : 0 < d
this : NoAtoms.{u_2} (α := X) (m0 := inst_2) μH[d]
⊢ ((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) {x} ≤
    HMul.hMul (β := ℝ≥0∞) ((↑0 : ℝ≥0∞) ^ d) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥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
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
⊢ (↑K : ℝ≥0∞) ^ d ≠ 0

Tactic:
simp [h0]
-- 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
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
⊢ (↑K : ℝ≥0∞) ^ d ≠ 0

Tactic:
have hKd0 : (K : ℝ≥0∞) ^ d ≠ 0 := by simp [h0]
-- 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
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : (↑K : ℝ≥0∞) ^ d ≠ 0
⊢ (↑K : ℝ≥0∞) ^ d ≠ ∞

Tactic:
simp [hd]
-- 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
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : (↑K : ℝ≥0∞) ^ d ≠ 0
⊢ (↑K : ℝ≥0∞) ^ d ≠ ∞

Tactic:
have hKd : (K : ℝ≥0∞) ^ d ≠ ∞ := by simp [hd]
-- 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
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : (↑K : ℝ≥0∞) ^ d ≠ 0
hKd : (↑K : ℝ≥0∞) ^ d ≠ ∞
inr :
  LE.le (α := ℝ≥0∞)
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : 0 < r),
        ⨅ (t : ℕ → Set X),
          ⨅ (_ : 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 Y),
          ⨅ (_ : s ⊆ ⋃ (n : ℕ), i_1 n),
            ⨅ (_ : ∀ (n : ℕ), ediam (i_1 n) ≤ i),
              ∑' (i : ℕ), ⨆ (_ : (i_1 i).Nonempty), (↑K : ℝ≥0∞) ^ d * ediam (i_1 i) ^ d)
⊢ ((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑K : ℝ≥0∞) ^ d) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [hausdorffMeasure_apply, ENNReal.mul_iSup, ENNReal.mul_iInf_of_ne hKd0 hKd,
    ← ENNReal.tsum_mul_left]

Premises used: ENNReal.tsum_mul_left, ENNReal.mul_iInf_of_ne, MeasureTheory.Measure.hausdorffMeasure_apply, ENNReal.mul_iSup
-- 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
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : (↑K : ℝ≥0∞) ^ d ≠ 0
hKd : (↑K : ℝ≥0∞) ^ d ≠ ∞
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (r : ℝ≥0∞),
      ⨆ (_ : 0 < r),
        ⨅ (t : ℕ → Set X),
          ⨅ (_ : 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 Y),
          ⨅ (_ : s ⊆ ⋃ (n : ℕ), i_1 n),
            ⨅ (_ : ∀ (n : ℕ), ediam (i_1 n) ≤ i),
              ∑' (i : ℕ), ⨆ (_ : (i_1 i).Nonempty), (↑K : ℝ≥0∞) ^ d * ediam (i_1 i) ^ d)

Tactic:
iSup₂_le fun ε ε0 => ?_

Premises used: iSup₂_le