awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
s : Set ℝ
this : NoAtoms.{u_5} (α := E) (m0 := inst_2) μH[1]
⊢ ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((fun (r : ℝ) ↦ HSMul.hSMul (β := E) r 0) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) (nnnorm.{u_5} (E := E) 0) ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
have inl : ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((fun (r : ℝ) ↦ HSMul.hSMul (β := E) r 0) '' ∅) =
  HSMul.hSMul (β := ℝ≥0∞) (nnnorm.{u_5} (E := E) 0) ((μH[1] : (a : Set ℝ) → ℝ≥0∞) ∅ : ℝ≥0∞)
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
s : Set ℝ
this : NoAtoms.{u_5} (α := E) (m0 := inst_2) μH[1]
inl :
  ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((fun (r : ℝ) ↦ HSMul.hSMul (β := E) r 0) '' ∅) =
    HSMul.hSMul (β := ℝ≥0∞) (nnnorm.{u_5} (E := E) 0) ((μH[1] : (a : Set ℝ) → ℝ≥0∞) ∅ : ℝ≥0∞)
⊢ ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((fun (r : ℝ) ↦ HSMul.hSMul (β := E) r 0) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) (nnnorm.{u_5} (E := E) 0) ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
have inl₁ : ∀ (hs : s.Nonempty),
  ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((fun (r : ℝ) ↦ HSMul.hSMul (β := E) r 0) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) (nnnorm.{u_5} (E := E) 0) ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
⊢ ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((fun (r : ℝ) ↦ r • v) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
have hn : ‖v‖ ≠ 0
Tactic: have hn : ‖v‖ ≠ 0 := norm_ne_zero_iff.mpr hv
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
⊢ ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((fun (r : ℝ) ↦ r • v) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
have inr : ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞)
    ((fun (x : E) ↦ ‖v‖ • x) '' (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E) '' s) =
  HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: suffices
      μH[1] ((‖v‖ • ·) '' LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v) '' s) = ‖v‖₊ • μH[1] s by
    simpa only [Set.image_image, smul_comm (norm _), inv_smul_smul₀ hn,
      LinearMap.toSpanSingleton_apply] using this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
⊢ Isometry (α := ℝ) (β := E) (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E)
have refine : ∀ (x : ℝ), norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * ‖‖v‖⁻¹ • v‖ = ‖x‖
Tactic: refine AddMonoidHomClass.isometry_of_norm _ fun x => (norm_smul _ _).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
x : ℝ
⊢ norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * ‖‖v‖⁻¹ • v‖ = ‖x‖
have rw : norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * (‖‖v‖⁻¹‖ * ‖v‖) = ‖x‖
Tactic: rw [norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hn, mul_one, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
x : ℝ
rw : norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * (‖‖v‖⁻¹‖ * ‖v‖) = ‖x‖
⊢ norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * ‖‖v‖⁻¹ • v‖ = ‖x‖
have rw₁ : norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * (‖‖v‖‖⁻¹ * ‖v‖) = ‖x‖
Tactic: rw [norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hn, mul_one, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
x : ℝ
rw : norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * (‖‖v‖⁻¹‖ * ‖v‖) = ‖x‖
rw₁ : norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * (‖‖v‖‖⁻¹ * ‖v‖) = ‖x‖
⊢ norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * ‖‖v‖⁻¹ • v‖ = ‖x‖
have rw₂ : norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * (‖v‖⁻¹ * ‖v‖) = ‖x‖
Tactic: rw [norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hn, mul_one, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
x : ℝ
rw : norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * (‖‖v‖⁻¹‖ * ‖v‖) = ‖x‖
rw₁ : norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * (‖‖v‖‖⁻¹ * ‖v‖) = ‖x‖
rw₂ : norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * (‖v‖⁻¹ * ‖v‖) = ‖x‖
⊢ norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * ‖‖v‖⁻¹ • v‖ = ‖x‖
have rw₃ : norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * 1 = ‖x‖
Tactic: rw [norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hn, mul_one, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
x : ℝ
rw : norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * (‖‖v‖⁻¹‖ * ‖v‖) = ‖x‖
rw₁ : norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * (‖‖v‖‖⁻¹ * ‖v‖) = ‖x‖
rw₂ : norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * (‖v‖⁻¹ * ‖v‖) = ‖x‖
rw₃ : norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * 1 = ‖x‖
⊢ norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * ‖‖v‖⁻¹ • v‖ = ‖x‖
have rw₄ : norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) = ‖x‖
Tactic: rw [norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hn, mul_one, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
x : ℝ
rw : norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * (‖‖v‖⁻¹‖ * ‖v‖) = ‖x‖
rw₁ : norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * (‖‖v‖‖⁻¹ * ‖v‖) = ‖x‖
rw₂ : norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * (‖v‖⁻¹ * ‖v‖) = ‖x‖
rw₃ : norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * 1 = ‖x‖
rw₄ : norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) = ‖x‖
⊢ norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * ‖‖v‖⁻¹ • v‖ = ‖x‖
have rw₅ : ‖x‖ = ‖x‖
Tactic: rw [norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hn, mul_one, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
⊢ ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞)
      ((fun (x : E) ↦ ‖v‖ • x) '' (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
have iso_smul : Isometry (α := ℝ) (β := E) (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
iso_smul : Isometry (α := ℝ) (β := E) (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E)
⊢ ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞)
      ((fun (x : E) ↦ ‖v‖ • x) '' (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
have inr : ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞)
    (HSMul.hSMul (β := Set E) ‖v‖ ((⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E) '' s)) =
  HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
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' ℝ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
iso_smul : Isometry (α := ℝ) (β := E) (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E)
inr :
  ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞)
      (HSMul.hSMul (β := Set E) ‖v‖ ((⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E) '' s)) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞)
      ((fun (x : E) ↦ ‖v‖ • x) '' (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
have inr₁ : HSMul.hSMul (β := ℝ≥0∞) (HPow.hPow (β := ℝ) ‖‖v‖‖₊ 1)
    (((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E) '' s) :
      ℝ≥0∞) =
  HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
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' ℝ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
iso_smul : Isometry (α := ℝ) (β := E) (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E)
inr :
  ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞)
      (HSMul.hSMul (β := Set E) ‖v‖ ((⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E) '' s)) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
inr₁ :
  HSMul.hSMul (β := ℝ≥0∞) (HPow.hPow (β := ℝ) ‖‖v‖‖₊ 1)
      (((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E) '' s) :
        ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞)
      ((fun (x : E) ↦ ‖v‖ • x) '' (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
have inr₂ : HSMul.hSMul (β := ℝ≥0∞) (HPow.hPow (β := ℝ) ‖v‖₊ 1)
    (((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E) '' s) :
      ℝ≥0∞) =
  HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
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' ℝ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
iso_smul : Isometry (α := ℝ) (β := E) (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E)
inr :
  ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞)
      (HSMul.hSMul (β := Set E) ‖v‖ ((⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E) '' s)) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
inr₁ :
  HSMul.hSMul (β := ℝ≥0∞) (HPow.hPow (β := ℝ) ‖‖v‖‖₊ 1)
      (((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E) '' s) :
        ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
inr₂ :
  HSMul.hSMul (β := ℝ≥0∞) (HPow.hPow (β := ℝ) ‖v‖₊ 1)
      (((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E) '' s) :
        ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞)
      ((fun (x : E) ↦ ‖v‖ • x) '' (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
have inr₃ : HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊
    (((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E) '' s) :
      ℝ≥0∞) =
  HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
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' ℝ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
iso_smul : Isometry (α := ℝ) (β := E) (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E)
inr :
  ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞)
      (HSMul.hSMul (β := Set E) ‖v‖ ((⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E) '' s)) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
inr₁ :
  HSMul.hSMul (β := ℝ≥0∞) (HPow.hPow (β := ℝ) ‖‖v‖‖₊ 1)
      (((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E) '' s) :
        ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
inr₂ :
  HSMul.hSMul (β := ℝ≥0∞) (HPow.hPow (β := ℝ) ‖v‖₊ 1)
      (((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E) '' s) :
        ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
inr₃ :
  HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊
      (((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E) '' s) :
        ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞)
      ((fun (x : E) ↦ ‖v‖ • x) '' (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
have inr₄ : HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) =
  HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
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' ℝ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : MeasurableSpace P
inst_4 : MetricSpace P
inst_5 : NormedAddTorsor E P
inst_6 : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ ((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) ((⇑(AffineMap.homothety x c) : (a : P) → P) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
have x₁ : ((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞)
    (image.{u_5, u_6} (α := E) (⇑(IsometryEquiv.vaddConst x) : (a : E) → P)
      ((fun (x : E) ↦ c • x) '' (⇑(IsometryEquiv.symm (IsometryEquiv.vaddConst x)) : (a : P) → E) '' s)) =
  HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: suffices
    μH[d] (IsometryEquiv.vaddConst x '' (c • ·) '' (IsometryEquiv.vaddConst x).symm '' s) =
      ‖c‖₊ ^ d • μH[d] s by
    simpa only [Set.image_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : MeasurableSpace P
inst_4 : MetricSpace P
inst_5 : NormedAddTorsor E P
inst_6 : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ ((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞)
      (image.{u_5, u_6} (α := E) (⇑(IsometryEquiv.vaddConst x) : (a : E) → P)
        ((fun (x : E) ↦ c • x) '' (⇑(IsometryEquiv.symm (IsometryEquiv.vaddConst x)) : (a : P) → E) '' s)) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : MeasurableSpace P
inst_4 : MetricSpace P
inst_5 : NormedAddTorsor E P
inst_6 : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ ((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞)
      (image.{u_5, u_6} (α := E) (⇑(IsometryEquiv.vaddConst x) : (a : E) → P)
        ((fun (x : E) ↦ c • x) '' (⇑(IsometryEquiv.symm (IsometryEquiv.vaddConst x)) : (a : P) → E) '' s)) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞)
    ((fun (x : E) ↦ c • x) '' (⇑(IsometryEquiv.symm (IsometryEquiv.vaddConst x)) : (a : P) → E) '' s) =
  HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [IsometryEquiv.hausdorffMeasure_image, Set.image_smul, Measure.hausdorffMeasure_smul₀ hd hc,
    IsometryEquiv.hausdorffMeasure_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : MeasurableSpace P
inst_4 : MetricSpace P
inst_5 : NormedAddTorsor E P
inst_6 : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
rw :
  ((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞)
      ((fun (x : E) ↦ c • x) '' (⇑(IsometryEquiv.symm (IsometryEquiv.vaddConst x)) : (a : P) → E) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞)
      (image.{u_5, u_6} (α := E) (⇑(IsometryEquiv.vaddConst x) : (a : E) → P)
        ((fun (x : E) ↦ c • x) '' (⇑(IsometryEquiv.symm (IsometryEquiv.vaddConst x)) : (a : P) → E) '' s)) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : ((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞)
    (HSMul.hSMul (β := Set E) c ((⇑(IsometryEquiv.symm (IsometryEquiv.vaddConst x)) : (a : P) → E) '' s)) =
  HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [IsometryEquiv.hausdorffMeasure_image, Set.image_smul, Measure.hausdorffMeasure_smul₀ hd hc,
    IsometryEquiv.hausdorffMeasure_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : MeasurableSpace P
inst_4 : MetricSpace P
inst_5 : NormedAddTorsor E P
inst_6 : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
rw :
  ((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞)
      ((fun (x : E) ↦ c • x) '' (⇑(IsometryEquiv.symm (IsometryEquiv.vaddConst x)) : (a : P) → E) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  ((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞)
      (HSMul.hSMul (β := Set E) c ((⇑(IsometryEquiv.symm (IsometryEquiv.vaddConst x)) : (a : P) → E) '' s)) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞)
      (image.{u_5, u_6} (α := E) (⇑(IsometryEquiv.vaddConst x) : (a : E) → P)
        ((fun (x : E) ↦ c • x) '' (⇑(IsometryEquiv.symm (IsometryEquiv.vaddConst x)) : (a : P) → E) '' s)) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
have rw₂ : HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊ ^ d)
    (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞)
        ((⇑(IsometryEquiv.symm (IsometryEquiv.vaddConst x)) : (a : P) → E) '' s) :
      ℝ≥0∞) =
  HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [IsometryEquiv.hausdorffMeasure_image, Set.image_smul, Measure.hausdorffMeasure_smul₀ hd hc,
    IsometryEquiv.hausdorffMeasure_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : MeasurableSpace P
inst_4 : MetricSpace P
inst_5 : NormedAddTorsor E P
inst_6 : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
rw :
  ((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞)
      ((fun (x : E) ↦ c • x) '' (⇑(IsometryEquiv.symm (IsometryEquiv.vaddConst x)) : (a : P) → E) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  ((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞)
      (HSMul.hSMul (β := Set E) c ((⇑(IsometryEquiv.symm (IsometryEquiv.vaddConst x)) : (a : P) → E) '' s)) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
rw₂ :
  HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊ ^ d)
      (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞)
          ((⇑(IsometryEquiv.symm (IsometryEquiv.vaddConst x)) : (a : P) → E) '' s) :
        ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞)
      (image.{u_5, u_6} (α := E) (⇑(IsometryEquiv.vaddConst x) : (a : E) → P)
        ((fun (x : E) ↦ c • x) '' (⇑(IsometryEquiv.symm (IsometryEquiv.vaddConst x)) : (a : P) → E) '' s)) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
have rw₃ : HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞) =
  HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [IsometryEquiv.hausdorffMeasure_image, Set.image_smul, Measure.hausdorffMeasure_smul₀ hd hc,
    IsometryEquiv.hausdorffMeasure_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : MeasurableSpace P
inst_4 : MetricSpace P
inst_5 : NormedAddTorsor E P
inst_6 : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ ((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) ((⇑(AffineMap.homothety x c) : (a : P) → P) ⁻¹' s) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊⁻¹ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
have change : ((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞)
    ((⇑((AffineEquiv.homothetyUnitsMulHom x : (a : 𝕜ˣ) → P ≃ᵃ[𝕜] P) (Units.mk0 c hc) : P ≃ᵃ[𝕜] P) : (a : P) → P) ⁻¹'
      s) =
  HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊⁻¹ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: change μH[d] (AffineEquiv.homothetyUnitsMulHom x (Units.mk0 c hc) ⁻¹' s) = _