-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem hausdorffMeasure_smul_right_image [NormedAddCommGroup E] [NormedSpace ℝ E]
    [MeasurableSpace E] [BorelSpace E] (v : E) (s : Set ℝ) :
    μH[1] ((fun r => r • v) '' s) = ‖v‖₊ • μH[1] s

Proof state:
case inr
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
⊢ μH[1] ((fun x => ‖v‖ • x) '' (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) '' s)) = ‖v‖₊ • μH[1] s

Tactic:
have iso_smul : Isometry (LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) := by
  refine AddMonoidHomClass.isometry_of_norm _ fun x => (norm_smul _ _).trans ?_
  rw [norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hn, mul_one, LinearMap.id_apply]

Result:
case inr
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
iso_smul : Isometry ⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v))
⊢ μH[1] ((fun x => ‖v‖ • x) '' (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) '' s)) = ‖v‖₊ • μH[1] s

Proof state:
case inr
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
iso_smul : Isometry ⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v))
⊢ μH[1] ((fun x => ‖v‖ • x) '' (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) '' s)) = ‖v‖₊ • μH[1] s

Tactic:
rw [Set.image_smul, Measure.hausdorffMeasure_smul₀ zero_le_one hn, nnnorm_norm,
    NNReal.rpow_one, iso_smul.hausdorffMeasure_image (Or.inl <| zero_le_one' ℝ)]

Result:
no goals

Proof state:
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
this : μH[1] ((fun x => ‖v‖ • x) '' (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) '' s)) = ‖v‖₊ • μH[1] s
⊢ μH[1] ((fun r => r • v) '' s) = ‖v‖₊ • μH[1] s

Tactic:
simpa only [Set.image_image, smul_comm (norm _), inv_smul_smul₀ hn,
  LinearMap.toSpanSingleton_apply] using this

Result:
no goals

Proof state:
case inl
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set ℝ
this : NoAtoms μH[1]
⊢ μH[1] ((fun r => r • 0) '' s) = ‖0‖₊ • μH[1] s

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Result:
case inl.inl
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
this : NoAtoms μH[1]
⊢ μH[1] ((fun r => r • 0) '' ∅) = ‖0‖₊ • μH[1] ∅

case inl.inr
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set ℝ
this : NoAtoms μH[1]
hs : s.Nonempty
⊢ μH[1] ((fun r => r • 0) '' s) = ‖0‖₊ • μH[1] s

Proof state:
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
x : ℝ
⊢ ‖LinearMap.id x‖ * ‖‖v‖⁻¹ • v‖ = ‖x‖

Tactic:
rw [norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hn, mul_one, LinearMap.id_apply]

Result:
no goals

Proof state:
case inr
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
⊢ μH[1] ((fun r => r • v) '' s) = ‖v‖₊ • μH[1] s

Tactic:
have hn : ‖v‖ ≠ 0 := norm_ne_zero_iff.mpr hv

Result:
case inr
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
⊢ μH[1] ((fun r => r • v) '' s) = ‖v‖₊ • μH[1] s

Proof state:
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
⊢ μH[1] ((fun r => r • v) '' s) = ‖v‖₊ • μH[1] s

Tactic:
obtain rfl | hv := eq_or_ne v 0

Result:
case inl
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set ℝ
⊢ μH[1] ((fun r => r • 0) '' s) = ‖0‖₊ • μH[1] s

case inr
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
⊢ μH[1] ((fun r => r • v) '' s) = ‖v‖₊ • μH[1] s

Proof state:
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
⊢ Isometry ⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v))

Tactic:
refine AddMonoidHomClass.isometry_of_norm _ fun x => (norm_smul _ _).trans ?_

Result:
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
x : ℝ
⊢ ‖LinearMap.id x‖ * ‖‖v‖⁻¹ • v‖ = ‖x‖

Proof state:
case inl.inl
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
this : NoAtoms μH[1]
⊢ μH[1] ((fun r => r • 0) '' ∅) = ‖0‖₊ • μH[1] ∅

Tactic:
simp

Result:
no goals

Proof state:
case inl.inr
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set ℝ
this : NoAtoms μH[1]
hs : s.Nonempty
⊢ μH[1] ((fun r => r • 0) '' s) = ‖0‖₊ • μH[1] s

Tactic:
simp [hs]

Result:
no goals

Proof state:
case inl
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set ℝ
⊢ μH[1] ((fun r => r • 0) '' s) = ‖0‖₊ • μH[1] s

Tactic:
haveI := noAtoms_hausdorff E one_pos

Result:
case inl
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set ℝ
this : NoAtoms μH[1]
⊢ μH[1] ((fun r => r • 0) '' s) = ‖0‖₊ • μH[1] s