awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
ι : Type u_1
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 : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
a : (↑(Fintype.card (Fin (finrank ℝ E))) : ℝ)
| (↑(finrank ℝ E) : ℝ)

Tactic:
rw [← Fintype.card_fin (finrank ℝ E)]

Premises used: Real, Fintype.card_fin, Module.finrank
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
ι : Type u_1
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 : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
a : (↑(Fintype.card (Fin (finrank ℝ E))) : ℝ)
| ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' U) :
    ℝ≥0∞)

Tactic:
congr; congr; rw [← Fintype.card_fin (finrank ℝ E)]

Premises used: Real, Fintype.card_fin, Module.finrank
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
ι : Type u_1
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 : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
conv_rhs :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μH[(↑(Fintype.card (Fin (finrank ℝ E))) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞)
        ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' U) :
      ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞)
        ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' U) :
      ℝ≥0∞)

Tactic:
conv_rhs => congr; congr; rw [← Fintype.card_fin (finrank ℝ E)]

Premises used: Real, Fintype.card_fin, Module.finrank
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
ι : Type u_1
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 : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
rw :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((volume : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' U) : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μH[(↑(Fintype.card (Fin (finrank ℝ E))) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞)
        ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' U) :
      ℝ≥0∞)

Tactic:
rw [hausdorffMeasure_pi_real]

Premises used: MeasureTheory.hausdorffMeasure_pi_real
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
ι : Type u_1
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 : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
apply : Set.Nonempty (α := Fin (finrank ℝ E) → ℝ) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' U)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((volume : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' U) : ℝ≥0∞)

Tactic:
apply (e.isOpenMap U hU).measure_pos (μ := volume)

Premises used: ContinuousLinearEquiv.isOpenMap, IsOpen.measure_pos, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
ι : Type u_1
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 : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
⊢ Set.Nonempty (α := Fin (finrank ℝ E) → ℝ) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' U)

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : Unique ι
d : ℝ
⊢ MeasurePreserving (α := ι → X) (β := X) (⇑(MeasurableEquiv.funUnique ι X) : (a : ι → X) → X) μH[d] μH[d]

Tactic:
(IsometryEquiv.funUnique ι X).measurePreserving_hausdorffMeasure _

Premises used: IsometryEquiv.funUnique, IsometryEquiv.measurePreserving_hausdorffMeasure
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
α : Fin 2 → Type u_4
inst : (i : Fin 2) → MeasurableSpace (α i)
inst_1 : (i : Fin 2) → EMetricSpace (α i)
inst_2 : ∀ (i : Fin 2), BorelSpace.{u_4} (α i)
inst_3 : ∀ (i : Fin 2), SecondCountableTopology.{u_4} (α i)
d : ℝ
⊢ MeasurePreserving (α := (i : Fin 2) → α i) (β := α 0 × α 1)
    (⇑(MeasurableEquiv.piFinTwo α) : (a : (i : Fin 2) → α i) → α 0 × α 1) μH[d] μH[d]

Tactic:
(IsometryEquiv.piFinTwo α).measurePreserving_hausdorffMeasure _

Premises used: IsometryEquiv.piFinTwo, IsometryEquiv.measurePreserving_hausdorffMeasure
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
rw :
  Eq (α := Measure ℝ) μH[1]
    (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) volume)
rw₁ :
  Eq (α := Measure ℝ) (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) μH[1])
    (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) volume)
rw₂ :
  Eq (α := Measure ℝ) (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) μH[1])
    (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ)
      μH[(↑(Fintype.card Unit) : ℝ)])
rw₃ :
  Eq (α := Measure ℝ) (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) μH[1])
    (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) μH[(↑1 : ℝ)])
rw₄ rw₅ :
  Eq (α := Measure ℝ) (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) μH[1])
    (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) μH[1])
⊢ Eq (α := Measure ℝ) μH[1] volume

Tactic:
rw [← (volume_preserving_funUnique Unit ℝ).map_eq,
    ← (hausdorffMeasure_measurePreserving_funUnique Unit ℝ 1).map_eq,
    ← hausdorffMeasure_pi_real, Fintype.card_unit, Nat.cast_one]

Premises used: Real, MeasureTheory.hausdorffMeasure_pi_real, MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.hausdorffMeasure_measurePreserving_funUnique, Unit, Fintype.card_unit, OfNat.ofNat, Nat.cast_one, MeasureTheory.volume_preserving_funUnique
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
rw :
  Eq (α := Measure (ℝ × ℝ)) μH[2]
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) volume)
rw₁ :
  Eq (α := Measure (ℝ × ℝ))
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) μH[2])
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) volume)
rw₂ :
  Eq (α := Measure (ℝ × ℝ))
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) μH[2])
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ)
      μH[(↑(Fintype.card (Fin 2)) : ℝ)])
rw₃ :
  Eq (α := Measure (ℝ × ℝ))
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) μH[2])
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) μH[(↑2 : ℝ)])
rw₄ rw₅ :
  Eq (α := Measure (ℝ × ℝ))
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) μH[2])
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) μH[2])
⊢ Eq (α := Measure (ℝ × ℝ)) μH[2] volume

Tactic:
rw [← (volume_preserving_piFinTwo fun _ => ℝ).map_eq,
    ← (hausdorffMeasure_measurePreserving_piFinTwo (fun _ => ℝ) _).map_eq,
    ← hausdorffMeasure_pi_real, Fintype.card_fin, Nat.cast_two]

Premises used: Real, Fintype.card_fin, MeasureTheory.hausdorffMeasure_measurePreserving_piFinTwo, MeasureTheory.hausdorffMeasure_pi_real, MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.volume_preserving_piFinTwo, Nat.cast_two
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
v : E
s : Set ℝ
inl :
  ((μ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∞)
inr :
  ∀ (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∞)
⊢ ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((fun (r : ℝ) ↦ r • v) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
obtain rfl | hv := eq_or_ne v 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
s : Set ℝ
⊢ NoAtoms.{u_5} (α := E) (m0 := inst_2) μH[1]

Tactic:
haveI := noAtoms_hausdorff E one_pos
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
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∞)
⊢ ((μ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

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
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) '' ∅) =
    HSMul.hSMul (β := ℝ≥0∞) (nnnorm.{u_5} (E := E) 0) ((μH[1] : (a : Set ℝ) → ℝ≥0∞) ∅ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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]
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:
simp [hs]
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
⊢ ‖v‖ ≠ 0

Tactic:
have hn : ‖v‖ ≠ 0 := norm_ne_zero_iff.mpr hv
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
this :
  ((μ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∞)
⊢ ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((fun (r : ℝ) ↦ r • v) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)

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

Premises used: Norm.norm, Set.image_image, inv_smul_smul₀, LinearMap.toSpanSingleton_apply, SMulCommClass.smul_comm
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
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∞)
⊢ ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((fun (r : ℝ) ↦ r • v) '' 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
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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)

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

Premises used: LinearMap.id, Norm.norm, AddMonoidHomClass.isometry_of_norm, norm_smul, Inv.inv, HSMul.hSMul, DFunLike.coe, Eq.trans
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
refine : ∀ (x : ℝ), norm (E := ℝ) ((LinearMap.id : (a : ℝ) → ℝ) x : ℝ) * ‖‖v‖⁻¹ • v‖ = ‖x‖
⊢ Isometry (α := ℝ) (β := E) (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) : (a : ℝ) → E)

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

Premises used: AddMonoidHomClass.isometry_of_norm
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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‖
rw₅ rw₆ : ‖x‖ = ‖x‖
⊢ 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]

Premises used: norm_smul, LinearMap.id_apply, norm_norm, norm_inv, mul_one, inv_mul_cancel₀
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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)

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]
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
inr₄ inr₅ :
  HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) 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∞)

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' ℝ)]

Premises used: Set.image_smul, Real, Isometry.hausdorffMeasure_image, MeasureTheory.Measure.hausdorffMeasure_smul₀, zero_le_one', zero_le_one, nnnorm_norm, Or.inl, NNReal.rpow_one
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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 :
  ((μ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∞)
⊢ ((μ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∞)

Tactic:
simpa only [Set.image_image]

Premises used: Set.image_image
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
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∞)
⊢ ((μ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∞)

Tactic:
suffices
    μH[d] (IsometryEquiv.vaddConst x '' (c • ·) '' (IsometryEquiv.vaddConst x).symm '' s) =
      ‖c‖₊ ^ d • μH[d] s by
    simpa only [Set.image_image]
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
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∞)
rw₃ 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∞)
⊢ ((μ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:
rw [IsometryEquiv.hausdorffMeasure_image, Set.image_smul, Measure.hausdorffMeasure_smul₀ hd hc,
    IsometryEquiv.hausdorffMeasure_image]

Premises used: Set.image_smul, IsometryEquiv.hausdorffMeasure_image, MeasureTheory.Measure.hausdorffMeasure_smul₀