awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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∞)
⊢ 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)
have rw₁ : 0 < ‖r‖₊ ^ d
Tactic: rw [← le_inv_smul_iff_of_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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∞)
have 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∞)
Tactic: rw [← NNReal.inv_rpow, ← nnnorm_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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∞)
have 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∞)
Tactic: refine Eq.trans_le ?_ (this (r • s))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) (r⁻¹ • r • s) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
  (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [inv_smul_smul₀ hr]
-- 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
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
⊢ ((μ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∞)
have 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∞)
Tactic: rcases eq_or_ne K 0 with (rfl | h0)
Cleared hypotheses: K, hf
-- 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
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∞)
⊢ ((μ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∞)
have 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∞)
Tactic: rcases eq_or_ne K 0 with (rfl | h0)
-- 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
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
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∞)
have 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∞)
Tactic: rcases eq_empty_or_nonempty (f ⁻¹' s) with (hs | ⟨x, hx⟩)
-- 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
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∞)
⊢ ((μ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∞)
have 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∞)
Tactic: rcases eq_empty_or_nonempty (f ⁻¹' s) with (hs | ⟨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
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
⊢ f ⁻¹' s = {x}
have this : Subsingleton X
Tactic: haveI : Subsingleton X := hf.subsingleton
-- 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
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 = {x}
have this₁ : (f ⁻¹' s).Subsingleton
Tactic: have : (f ⁻¹' s).Subsingleton := subsingleton_univ.anti (subset_univ _)
-- 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
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
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∞)
have this : 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
-- 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
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] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑0 : ℝ≥0∞) ^ d) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
Tactic: rw [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
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] : Measure X) : (a : Set X) → ℝ≥0∞) {x} ≤
    HMul.hMul (β := ℝ≥0∞) ((↑0 : ℝ≥0∞) ^ d) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
Tactic: rcases eq_or_lt_of_le hd with (rfl | h'd)
Cleared hypotheses: d, hd
-- 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
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∞)
⊢ ((μ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∞)
have 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∞)
Tactic: rcases eq_or_lt_of_le hd with (rfl | h'd)
-- 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
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
⊢ ((μ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∞)
have inl : LE.le (α := ℝ≥0∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞)
  (((μH[0] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp only [ENNReal.rpow_zero, one_mul]
-- 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
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∞) (((μH[0] : Measure X) : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞)
    (((μH[0] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
have inl : LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) (((μH[0] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [hausdorffMeasure_zero_singleton]
-- 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
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
⊢ ((μ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∞)
have this₁ : NoAtoms.{u_2} (α := X) (m0 := inst_2) μH[d]
Tactic: haveI := noAtoms_hausdorff X h'd
-- 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
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
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∞)
have hKd0 : (↑K : ℝ≥0∞) ^ d ≠ 0
Tactic: have hKd0 : (K : ℝ≥0∞) ^ d ≠ 0 := by simp [h0]
-- 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
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : (↑K : ℝ≥0∞) ^ d ≠ 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∞)
have hKd : (↑K : ℝ≥0∞) ^ d ≠ ∞
Tactic: have hKd : (K : ℝ≥0∞) ^ d ≠ ∞ := by simp [hd]
-- 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
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 ≠ ∞
⊢ ((μ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∞)
have 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)
Tactic: simp only [hausdorffMeasure_apply, ENNReal.mul_iSup, ENNReal.mul_iInf_of_ne hKd0 hKd,
    ← ENNReal.tsum_mul_left]
-- 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
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)
have inr : ∀ (ε : ℝ≥0∞) (ε0 : 0 < ε),
  LE.le (α := ℝ≥0∞)
    (⨅ (t : ℕ → Set X),
      ⨅ (_ : f ⁻¹' s ⊆ ⋃ (n : ℕ), t n),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (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: refine iSup₂_le fun ε ε0 => ?_
-- 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
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 ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
⊢ LE.le (α := ℝ≥0∞)
    (⨅ (t : ℕ → Set X),
      ⨅ (_ : f ⁻¹' s ⊆ ⋃ (n : ℕ), t n),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (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)
have inr : LE.le (α := ℝ≥0∞)
  (⨅ (t : ℕ → Set X),
    ⨅ (_ : f ⁻¹' s ⊆ ⋃ (n : ℕ), t n),
      ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d)
  (⨅ (i : ℕ → Set Y),
    ⨅ (_ : s ⊆ ⋃ (n : ℕ), i n),
      ⨅ (_ : ∀ (n : ℕ), ediam (i n) ≤ ε / (↑K : ℝ≥0∞)),
        ∑' (i_1 : ℕ), ⨆ (_ : (i i_1).Nonempty), (↑K : ℝ≥0∞) ^ d * ediam (i i_1) ^ d)
Tactic: refine le_iSup₂_of_le (ε / K) (by simp [ε0.ne']) ?_
-- 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
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 ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
⊢ LE.le (α := ℝ≥0∞)
    (⨅ (t : ℕ → Set X),
      ⨅ (_ : f ⁻¹' s ⊆ ⋃ (n : ℕ), t n),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d)
    (⨅ (i : ℕ → Set Y),
      ⨅ (_ : s ⊆ ⋃ (n : ℕ), i n),
        ⨅ (_ : ∀ (n : ℕ), ediam (i n) ≤ ε / (↑K : ℝ≥0∞)),
          ∑' (i_1 : ℕ), ⨆ (_ : (i i_1).Nonempty), (↑K : ℝ≥0∞) ^ d * ediam (i i_1) ^ d)
have inr : ∀ (t : ℕ → Set Y) (hst : s ⊆ ⋃ (n : ℕ), t n) (htε : ∀ (n : ℕ), ediam (t n) ≤ ε / (↑K : ℝ≥0∞)),
  LE.le (α := ℝ≥0∞)
    (⨅ (t : ℕ → Set X),
      ⨅ (_ : f ⁻¹' s ⊆ ⋃ (n : ℕ), t n),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d)
    (∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), (↑K : ℝ≥0∞) ^ d * ediam (t i) ^ d)
Tactic: refine le_iInf₂ fun t hst => le_iInf fun htε => ?_
-- 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
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 ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
hst : s ⊆ ⋃ (n : ℕ), t n
htε : ∀ (n : ℕ), ediam (t n) ≤ ε / (↑K : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    (⨅ (t : ℕ → Set X),
      ⨅ (_ : f ⁻¹' s ⊆ ⋃ (n : ℕ), t n),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d)
    (∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), (↑K : ℝ≥0∞) ^ d * ediam (t i) ^ d)
have hst₁ : f ⁻¹' s ⊆ f ⁻¹' ⋃ (n : ℕ), t n
Tactic: replace hst : f ⁻¹' s ⊆ _ := preimage_mono hst
Cleared hypotheses: hst
-- 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
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 ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
htε : ∀ (n : ℕ), ediam (t n) ≤ ε / (↑K : ℝ≥0∞)
hst : f ⁻¹' s ⊆ f ⁻¹' ⋃ (n : ℕ), t n
⊢ LE.le (α := ℝ≥0∞)
    (⨅ (t : ℕ → Set X),
      ⨅ (_ : f ⁻¹' s ⊆ ⋃ (n : ℕ), t n),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d)
    (∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), (↑K : ℝ≥0∞) ^ d * ediam (t i) ^ d)
have hst₁ : f ⁻¹' s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
Tactic: rw [preimage_iUnion] at hst
Cleared hypotheses: hst
-- 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
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 ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
htε : ∀ (n : ℕ), ediam (t n) ≤ ε / (↑K : ℝ≥0∞)
hst : f ⁻¹' s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
⊢ LE.le (α := ℝ≥0∞)
    (⨅ (t : ℕ → Set X),
      ⨅ (_ : f ⁻¹' s ⊆ ⋃ (n : ℕ), t n),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d)
    (∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), (↑K : ℝ≥0∞) ^ d * ediam (t i) ^ d)
have inr : ∀ (n : ℕ), ediam.{u_2} (X := X) ((fun (n : ℕ) ↦ f ⁻¹' t n) n) ≤ ε
Tactic: refine iInf₂_le_of_le _ hst (iInf_le_of_le (fun n => ?_) ?_)
-- 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
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 ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
htε : ∀ (n : ℕ), ediam (t n) ≤ ε / (↑K : ℝ≥0∞)
hst : f ⁻¹' s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
inr : ∀ (n : ℕ), ediam.{u_2} (X := X) ((fun (n : ℕ) ↦ f ⁻¹' t n) n) ≤ ε
⊢ LE.le (α := ℝ≥0∞)
    (⨅ (t : ℕ → Set X),
      ⨅ (_ : f ⁻¹' s ⊆ ⋃ (n : ℕ), t n),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d)
    (∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), (↑K : ℝ≥0∞) ^ d * ediam (t i) ^ d)
have inr₁ : LE.le (α := ℝ≥0∞)
  (∑' (n : ℕ),
    ⨆ (_ : Set.Nonempty.{u_2} (α := X) ((fun (n : ℕ) ↦ f ⁻¹' t n) n)),
      ediam.{u_2} (X := X) ((fun (n : ℕ) ↦ f ⁻¹' t n) n) ^ d)
  (∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), (↑K : ℝ≥0∞) ^ d * ediam (t i) ^ d)
Tactic: refine iInf₂_le_of_le _ hst (iInf_le_of_le (fun n => ?_) ?_)
-- 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
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 ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
htε : ∀ (n : ℕ), ediam (t n) ≤ ε / (↑K : ℝ≥0∞)
hst : f ⁻¹' s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
⊢ LE.le (α := ℝ≥0∞)
    (∑' (n : ℕ),
      ⨆ (_ : Set.Nonempty.{u_2} (α := X) ((fun (n : ℕ) ↦ f ⁻¹' t n) n)),
        ediam.{u_2} (X := X) ((fun (n : ℕ) ↦ f ⁻¹' t n) n) ^ d)
    (∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), (↑K : ℝ≥0∞) ^ d * ediam (t i) ^ d)
have inr : ∀ (n : ℕ) (hft : Set.Nonempty.{u_2} (α := X) ((fun (n : ℕ) ↦ f ⁻¹' t n) n)),
  ediam.{u_2} (X := X) ((fun (n : ℕ) ↦ f ⁻¹' t n) n) ^ d ≤ ⨆ (_ : (t n).Nonempty), (↑K : ℝ≥0∞) ^ d * ediam (t n) ^ d
Tactic: refine ENNReal.tsum_le_tsum fun n => iSup_le_iff.2 fun hft => ?_