-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem MeasureTheory.Measure.hausdorffMeasure_smul₀ {𝕜 E : Type*} [NormedAddCommGroup E]
    [NormedField 𝕜] [NormedSpace 𝕜 E] [MeasurableSpace E] [BorelSpace E] {d : ℝ} (hd : 0 ≤ d)
    {r : 𝕜} (hr : r ≠ 0) (s : Set E) : μH[d] (r • s) = ‖r‖₊ ^ d • μH[d] s

Proof state:
𝕜 : Type u_4
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this : ∀ {r : 𝕜} (s : Set E), μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
⊢ μH[d] (r • s) = ‖r‖₊ ^ d • μH[d] s

Tactic:
refine le_antisymm (this s) ?_

Result:
𝕜 : Type u_4
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this : ∀ {r : 𝕜} (s : Set E), μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
⊢ ‖r‖₊ ^ d • μH[d] s ≤ μH[d] (r • s)

Proof state:
𝕜 : Type u_4
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this : ∀ {r : 𝕜} (s : Set E), μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
⊢ ‖r‖₊ ^ d • μH[d] s ≤ μH[d] (r • s)

Tactic:
rw [← le_inv_smul_iff_of_pos]

Result:
𝕜 : Type u_4
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this : ∀ {r : 𝕜} (s : Set E), μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
⊢ μH[d] s ≤ (‖r‖₊ ^ d)⁻¹ • μH[d] (r • s)

𝕜 : Type u_4
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this : ∀ {r : 𝕜} (s : Set E), μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
⊢ 0 < ‖r‖₊ ^ d

Proof state:
𝕜 : Type u_4
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this : ∀ {r : 𝕜} (s : Set E), μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
⊢ 0 < ‖r‖₊ ^ d

Tactic:
simp [pos_iff_ne_zero, hr]

Result:
no goals

Proof state:
𝕜 : Type u_4
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this : ∀ {r : 𝕜} (s : Set E), μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
⊢ μH[d] s = μH[d] (r⁻¹ • r • s)

Tactic:
rw [inv_smul_smul₀ hr]

Result:
no goals

Proof state:
𝕜 : Type u_4
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this : ∀ {r : 𝕜} (s : Set E), μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
⊢ μH[d] s ≤ ↑(‖r⁻¹‖₊ ^ d) * μH[d] (r • s)

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

Result:
𝕜 : Type u_4
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this : ∀ {r : 𝕜} (s : Set E), μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
⊢ μH[d] s = μH[d] (r⁻¹ • r • s)

Proof state:
𝕜 : Type u_4
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this : ∀ {r : 𝕜} (s : Set E), μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
⊢ μH[d] s ≤ ↑(‖r‖₊ ^ d)⁻¹ * μH[d] (r • s)

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

Result:
𝕜 : Type u_4
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this : ∀ {r : 𝕜} (s : Set E), μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
⊢ μH[d] s ≤ ↑(‖r⁻¹‖₊ ^ d) * μH[d] (r • s)

Proof state:
𝕜 : Type u_4
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
⊢ μH[d] (r • s) = ‖r‖₊ ^ d • μH[d] s

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

Result:
𝕜 : Type u_4
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this : ∀ {r : 𝕜} (s : Set E), μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
⊢ μH[d] (r • s) = ‖r‖₊ ^ d • μH[d] s

Proof state:
𝕜 : Type u_4
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this : ∀ {r : 𝕜} (s : Set E), μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
⊢ μH[d] s ≤ (‖r‖₊ ^ d)⁻¹ • μH[d] (r • s)

Tactic:
dsimp

Result:
𝕜 : Type u_4
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this : ∀ {r : 𝕜} (s : Set E), μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
⊢ μH[d] s ≤ ↑(‖r‖₊ ^ d)⁻¹ * μH[d] (r • s)

Proof state:
𝕜 : Type u_4
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r✝ : 𝕜
hr : r✝ ≠ 0
s✝ : Set E
r : 𝕜
s : Set E
⊢ μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s

Tactic:
simpa [ENNReal.coe_rpow_of_nonneg, hd]
  using (lipschitzWith_smul r).hausdorffMeasure_image_le hd s

Result:
no goals