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
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 :
  ∀ (ε : ℝ≥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)
⊢ 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:
refine iSup₂_le fun ε ε0 => ?_

Premises used: iSup₂_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
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 < ε
⊢ 0 < ε / (↑K : ℝ≥0∞)

Tactic:
simp [ε0.ne']

Premises used: LT.lt.ne'
-- 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 ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
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)
⊢ 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 le_iSup₂_of_le (ε / K) (by simp [ε0.ne']) ?_

Premises used: ENNReal.ofNNReal, HDiv.hDiv, le_iSup₂_of_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
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)

Tactic:
le_iInf₂ fun t hst => le_iInf fun htε => ?_

Premises used: le_iInf, le_iInf₂
-- 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 ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
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)
⊢ 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_iInf₂ fun t hst => le_iInf fun htε => ?_

Premises used: le_iInf, le_iInf₂
-- 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 ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
hst : s ⊆ ⋃ (n : ℕ), t n
htε : ∀ (n : ℕ), ediam (t n) ≤ ε / (↑K : ℝ≥0∞)
⊢ f ⁻¹' s ⊆ f ⁻¹' ⋃ (n : ℕ), t n

Tactic:
replace hst : f ⁻¹' s ⊆ _ := preimage_mono hst
-- 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 ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
htε : ∀ (n : ℕ), ediam (t n) ≤ ε / (↑K : ℝ≥0∞)
hst : f ⁻¹' s ⊆ f ⁻¹' ⋃ (n : ℕ), t n
⊢ f ⁻¹' s ⊆ ⋃ (i : ℕ), f ⁻¹' t i

Tactic:
rw [preimage_iUnion] at hst

Premises used: Set.preimage_iUnion
-- 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 ≠ ∞
ε : ℝ≥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)

Tactic:
iInf₂_le_of_le _ hst (iInf_le_of_le (fun n => ?_) ?_)

Premises used: iInf₂_le_of_le, iInf_le_of_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
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) ≤ ε
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)
⊢ 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 iInf₂_le_of_le _ hst (iInf_le_of_le (fun n => ?_) ?_)

Premises used: iInf₂_le_of_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
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
n : ℕ
⊢ ediam.{u_2} (X := X) ((fun (n : ℕ) ↦ f ⁻¹' t n) n) ≤ ε

Tactic:
(hf.ediam_preimage_le _).trans (ENNReal.mul_le_of_le_div' <| htε n)

Premises used: ENNReal.mul_le_of_le_div', LE.le.trans, AntilipschitzWith.ediam_preimage_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
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
n : ℕ
⊢ ediam.{u_2} (X := X) ((fun (n : ℕ) ↦ f ⁻¹' t n) n) ≤ ε

Tactic:
exact (hf.ediam_preimage_le _).trans (ENNReal.mul_le_of_le_div' <| htε n)

Premises used: ENNReal.mul_le_of_le_div', LE.le.trans, AntilipschitzWith.ediam_preimage_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
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)

Tactic:
ENNReal.tsum_le_tsum fun n => iSup_le_iff.2 fun hft => ?_

Premises used: Iff.mpr, ENNReal.tsum_le_tsum, iSup_le_iff
-- 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 ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
htε : ∀ (n : ℕ), ediam (t n) ≤ ε / (↑K : ℝ≥0∞)
hst : f ⁻¹' s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
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
⊢ 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 ENNReal.tsum_le_tsum fun n => iSup_le_iff.2 fun hft => ?_

Premises used: Iff.mpr, ENNReal.tsum_le_tsum, iSup_le_iff
-- 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 ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
htε : ∀ (n : ℕ), ediam (t n) ≤ ε / (↑K : ℝ≥0∞)
hst : f ⁻¹' s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
n : ℕ
hft : Set.Nonempty.{u_2} (α := X) ((fun (n : ℕ) ↦ f ⁻¹' t n) n)
inr : ediam (f ⁻¹' t n) ^ d ≤ (↑K : ℝ≥0∞) ^ d * ediam (t n) ^ d
⊢ ediam.{u_2} (X := X) ((fun (n : ℕ) ↦ f ⁻¹' t n) n) ^ d ≤ ⨆ (_ : (t n).Nonempty), (↑K : ℝ≥0∞) ^ d * ediam (t n) ^ d

Tactic:
simp only [nonempty_of_nonempty_preimage hft, ciSup_pos]

Premises used: Set.nonempty_of_nonempty_preimage, ciSup_pos
-- 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 ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
htε : ∀ (n : ℕ), ediam (t n) ≤ ε / (↑K : ℝ≥0∞)
hst : f ⁻¹' s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
n : ℕ
hft : Set.Nonempty.{u_2} (α := X) ((fun (n : ℕ) ↦ f ⁻¹' t n) n)
inr : ediam (f ⁻¹' t n) ^ d ≤ ((↑K : ℝ≥0∞) * ediam (t n)) ^ d
⊢ ediam (f ⁻¹' t n) ^ d ≤ (↑K : ℝ≥0∞) ^ d * ediam (t n) ^ d

Tactic:
rw [← ENNReal.mul_rpow_of_nonneg _ _ hd]

Premises used: ENNReal.mul_rpow_of_nonneg
-- 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 ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
htε : ∀ (n : ℕ), ediam (t n) ≤ ε / (↑K : ℝ≥0∞)
hst : f ⁻¹' s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
n : ℕ
hft : Set.Nonempty.{u_2} (α := X) ((fun (n : ℕ) ↦ f ⁻¹' t n) n)
⊢ ediam (f ⁻¹' t n) ^ d ≤ ((↑K : ℝ≥0∞) * ediam (t n)) ^ d

Tactic:
ENNReal.rpow_le_rpow (hf.ediam_preimage_le _) hd

Premises used: ENNReal.rpow_le_rpow, AntilipschitzWith.ediam_preimage_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
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
n : ℕ
hft : Set.Nonempty.{u_2} (α := X) ((fun (n : ℕ) ↦ f ⁻¹' t n) n)
⊢ ediam (f ⁻¹' t n) ^ d ≤ ((↑K : ℝ≥0∞) * ediam (t n)) ^ d

Tactic:
exact ENNReal.rpow_le_rpow (hf.ediam_preimage_le _) hd

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

Tactic:
calc
    μH[d] s ≤ μH[d] (f ⁻¹' f '' s) := measure_mono (subset_preimage_image _ _)
    _ ≤ (K : ℝ≥0∞) ^ d * μH[d] (f '' s) := hf.hausdorffMeasure_preimage_le hd (f '' s)

Premises used: AntilipschitzWith.hausdorffMeasure_preimage_le, Trans.trans, MeasureTheory.measure_mono, Set.image, Set.subset_preimage_image
-- 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 : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set X
simp :
  Eq (α := ℝ≥0∞)
    ((((OuterMeasure.comap f : (a : OuterMeasure Y) → OuterMeasure X) (OuterMeasure.mkMetric fun (r : ℝ≥0∞) ↦ r ^ d) :
            OuterMeasure X) :
          (a : Set X) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((OuterMeasure.mkMetric fun (r : ℝ≥0∞) ↦ r ^ d : OuterMeasure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [hausdorffMeasure, ← OuterMeasure.coe_mkMetric, ← OuterMeasure.comap_apply]

Premises used: MeasureTheory.OuterMeasure.comap_apply, MeasureTheory.Measure.hausdorffMeasure, MeasureTheory.OuterMeasure.coe_mkMetric
-- 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 : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set X
rw : 0 ≤ d → Monotone (β := ℝ≥0∞) fun (r : ℝ≥0∞) ↦ r ^ d
⊢ Eq (α := ℝ≥0∞)
    ((((OuterMeasure.comap f : (a : OuterMeasure Y) → OuterMeasure X) (OuterMeasure.mkMetric fun (r : ℝ≥0∞) ↦ r ^ d) :
            OuterMeasure X) :
          (a : Set X) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((OuterMeasure.mkMetric fun (r : ℝ≥0∞) ↦ r ^ d : OuterMeasure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [OuterMeasure.isometry_comap_mkMetric _ hf (hd.imp_left _)]

Premises used: Or.imp_left, MeasureTheory.OuterMeasure.isometry_comap_mkMetric
-- 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 : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set X
⊢ 0 ≤ d → Monotone (β := ℝ≥0∞) fun (r : ℝ≥0∞) ↦ r ^ d

Tactic:
ENNReal.monotone_rpow_of_nonneg

Premises used: ENNReal.monotone_rpow_of_nonneg
-- 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 : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set X
⊢ 0 ≤ d → Monotone (β := ℝ≥0∞) fun (r : ℝ≥0∞) ↦ r ^ d

Tactic:
exact ENNReal.monotone_rpow_of_nonneg

Premises used: ENNReal.monotone_rpow_of_nonneg
-- 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 : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set Y
rw :
  Eq (α := ℝ≥0∞) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' f ⁻¹' s) : ℝ≥0∞)
    (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
    (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)

Tactic:
rw [← hf.hausdorffMeasure_image hd, image_preimage_eq_inter_range]

Premises used: Isometry.hausdorffMeasure_image, Set.image_preimage_eq_inter_range
-- 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 : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
h :
  ∀ (s : Set Y) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((Measure.map f μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
      (((Measure.restrict μH[d] (range f) : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Measure Y) (Measure.map f μH[d]) (Measure.restrict μH[d] (range f))

Tactic:
ext1 s hs
-- 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 : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set Y
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((Measure.restrict μH[d] (range f) : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
h₂ h₃ :
  Eq (α := ℝ≥0∞) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
    (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map f μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.restrict μH[d] (range f) : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [map_apply hf.continuous.measurable hs, Measure.restrict_apply hs,
    hf.hausdorffMeasure_preimage hd]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.Measure.restrict_apply, Isometry.continuous, Isometry.hausdorffMeasure_preimage, Continuous.measurable
-- 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
e : X ≃ᵢ Y
d : ℝ
s : Set X
⊢ Eq (α := ℝ≥0∞) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) ((⇑e : (a : X) → Y) '' s) : ℝ≥0∞)
    (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
e.isometry.hausdorffMeasure_image (Or.inr e.surjective) s

Premises used: Isometry.hausdorffMeasure_image, Or.inr, IsometryEquiv.isometry, IsometryEquiv.surjective
-- 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
e : X ≃ᵢ Y
d : ℝ
s : Set Y
rw :
  Eq (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) ((⇑e.symm : (a : Y) → X) '' s) : ℝ≥0∞)
    (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
    (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μH[d] : Measure X) : (a : Set X) → ℝ≥0∞) ((⇑e : (a : X) → Y) ⁻¹' s) : ℝ≥0∞)
    (((μH[d] : Measure Y) : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← e.image_symm, e.symm.hausdorffMeasure_image]

Premises used: IsometryEquiv.hausdorffMeasure_image, IsometryEquiv.symm, IsometryEquiv.image_symm
-- 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
e : X ≃ᵢ Y
d : ℝ
rw : Eq.{u_3 + 1} (α := Measure Y) (Measure.restrict μH[d] (range.{u_3, u_2 + 1} (ι := X) (⇑e : (a : X) → Y))) μH[d]
rw₁ : Eq.{u_3 + 1} (α := Measure Y) (Measure.restrict μH[d] univ) μH[d]
rw₂ rw₃ : Eq.{u_3 + 1} (α := Measure Y) μH[d] μH[d]
⊢ Eq.{u_3 + 1} (α := Measure Y) (Measure.map.{u_2, u_3} (α := X) (⇑e : (a : X) → Y) μH[d]) μH[d]

Tactic:
rw [e.isometry.map_hausdorffMeasure (Or.inr e.surjective), e.surjective.range_eq, restrict_univ]

Premises used: Function.Surjective.range_eq, Isometry.map_hausdorffMeasure, Or.inr, IsometryEquiv.isometry, IsometryEquiv.surjective, MeasureTheory.Measure.restrict_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
e : X ≃ᵢ Y
d : ℝ
⊢ MeasurePreserving.{u_2, u_3} (α := X) (β := Y) (⇑e : (a : X) → Y) μH[d] μH[d]

Tactic:
⟨e.continuous.measurable, map_hausdorffMeasure _ _⟩

Premises used: MeasureTheory.MeasurePreserving.mk, IsometryEquiv.map_hausdorffMeasure, Continuous.measurable, IsometryEquiv.continuous