-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem hausdorffMeasure_preimage_le (hf : AntilipschitzWith K f) (hd : 0 ≤ d) (s : Set Y) :
    μH[d] (f ⁻¹' s) ≤ (K : ℝ≥0∞) ^ d * μH[d] s

Proof state:
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : 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}

Tactic:
have : (f ⁻¹' s).Subsingleton := subsingleton_univ.anti (subset_univ _)

Result:
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : 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
this : (f ⁻¹' s).Subsingleton
⊢ f ⁻¹' s = {x}

Proof state:
case inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : ↑K ^ d ≠ 0
hKd : ↑K ^ d ≠ ⊤
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
htε : ∀ (n : ℕ), diam (t n) ≤ ε / ↑K
hst : f ⁻¹' s ⊆ f ⁻¹' ⋃ n, t n
⊢ ⨅ t,
      ⨅ (_ : f ⁻¹' s ⊆ ⋃ n, t n),
        ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ d ≤
    ∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), ↑K ^ d * diam (t i) ^ d

Tactic:
rw [preimage_iUnion] at hst

Result:
case inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : ↑K ^ d ≠ 0
hKd : ↑K ^ d ≠ ⊤
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
htε : ∀ (n : ℕ), diam (t n) ≤ ε / ↑K
hst : f ⁻¹' s ⊆ ⋃ i, f ⁻¹' t i
⊢ ⨅ t,
      ⨅ (_ : f ⁻¹' s ⊆ ⋃ n, t n),
        ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ d ≤
    ∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), ↑K ^ d * diam (t i) ^ d

Proof state:
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : ↑K ^ d ≠ 0
⊢ ↑K ^ d ≠ ⊤

Tactic:
simp [hd]

Result:
no goals

Proof state:
case inl
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
⊢ μH[d] (f ⁻¹' s) ≤ ↑0 ^ d * μH[d] s

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

Result:
case inl.inl
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
hs : f ⁻¹' s = ∅
⊢ μH[d] (f ⁻¹' s) ≤ ↑0 ^ d * μH[d] s

case inl.inr.intro
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
⊢ μH[d] (f ⁻¹' s) ≤ ↑0 ^ d * μH[d] s

Proof state:
case inl.inr.intro.inl
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
this : f ⁻¹' s = {x}
hd : 0 ≤ 0
⊢ μH[0] {x} ≤ ↑0 ^ 0 * μH[0] s

Tactic:
simp only [ENNReal.rpow_zero, one_mul, mul_zero]

Result:
case inl.inr.intro.inl
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
this : f ⁻¹' s = {x}
hd : 0 ≤ 0
⊢ μH[0] {x} ≤ μH[0] s

Proof state:
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
⊢ μH[d] (f ⁻¹' s) ≤ ↑K ^ d * μH[d] s

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

Result:
case inl
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
⊢ μH[d] (f ⁻¹' s) ≤ ↑0 ^ d * μH[d] s

case inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
⊢ μH[d] (f ⁻¹' s) ≤ ↑K ^ d * μH[d] s

Proof state:
case inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : ↑K ^ d ≠ 0
hKd : ↑K ^ d ≠ ⊤
ε : ℝ≥0∞
ε0 : 0 < ε
⊢ ⨅ t,
      ⨅ (_ : f ⁻¹' s ⊆ ⋃ n, t n),
        ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ d ≤
    ⨅ i,
      ⨅ (_ : s ⊆ ⋃ n, i n),
        ⨅ (_ : ∀ (n : ℕ), diam (i n) ≤ ε / ↑K), ∑' (i_1 : ℕ), ⨆ (_ : (i i_1).Nonempty), ↑K ^ d * diam (i i_1) ^ d

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

Result:
case inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : ↑K ^ d ≠ 0
hKd : ↑K ^ d ≠ ⊤
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
hst : s ⊆ ⋃ n, t n
htε : ∀ (n : ℕ), diam (t n) ≤ ε / ↑K
⊢ ⨅ t,
      ⨅ (_ : f ⁻¹' s ⊆ ⋃ n, t n),
        ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ d ≤
    ∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), ↑K ^ d * diam (t i) ^ d

Proof state:
case inr.refine_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : ↑K ^ d ≠ 0
hKd : ↑K ^ d ≠ ⊤
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
htε : ∀ (n : ℕ), diam (t n) ≤ ε / ↑K
hst : f ⁻¹' s ⊆ ⋃ i, f ⁻¹' t i
n : ℕ
⊢ diam ((fun n => f ⁻¹' t n) n) ≤ ε

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

Result:
no goals