awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (goal)
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℕ
h : d₁ < d₂
s : Set X
inl :
  ∀ (h : Eq (α := ENNReal) (((μH[(↑d₂ : ℝ)] : Measure X) : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)),
    Eq (α := ENNReal)
        ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₂)) volume μH[(↑d₂ : ℝ)])
                μH[(↑d₂ : ℝ)] :
              (a : Set X) → ENNReal)
            s :
          ENNReal)
        (0 : ENNReal) ∨
      Eq (α := ENNReal)
        ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₁)) volume μH[(↑d₁ : ℝ)])
                μH[(↑d₁ : ℝ)] :
              (a : Set X) → ENNReal)
            s :
          ENNReal)
        (⊤ : ENNReal)
⊢ Eq (α := ENNReal)
      ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₂)) volume μH[(↑d₂ : ℝ)])
              μH[(↑d₂ : ℝ)] :
            (a : Set X) → ENNReal)
          s :
        ENNReal)
      (0 : ENNReal) ∨
    Eq (α := ENNReal)
      ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₁)) volume μH[(↑d₁ : ℝ)])
              μH[(↑d₁ : ℝ)] :
            (a : Set X) → ENNReal)
          s :
        ENNReal)
      (⊤ : ENNReal)
have inr : ∀ (h : Eq (α := ENNReal) (((μH[(↑d₁ : ℝ)] : Measure X) : (a : Set X) → ENNReal) s : ENNReal) (⊤ : ENNReal)),
  Eq (α := ENNReal)
      ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₂)) volume μH[(↑d₂ : ℝ)])
              μH[(↑d₂ : ℝ)] :
            (a : Set X) → ENNReal)
          s :
        ENNReal)
      (0 : ENNReal) ∨
    Eq (α := ENNReal)
      ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₁)) volume μH[(↑d₁ : ℝ)])
              μH[(↑d₁ : ℝ)] :
            (a : Set X) → ENNReal)
          s :
        ENNReal)
      (⊤ : ENNReal)
Tactic: obtain h | h := hausdorffMeasure_zero_or_top (show (d₁ : ℝ) < d₂ by simpa using h) s
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (goal)
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℕ
h_1 : d₁ < d₂
s : Set X
h : Eq (α := ENNReal) (((μH[(↑d₁ : ℝ)] : Measure X) : (a : Set X) → ENNReal) s : ENNReal) (⊤ : ENNReal)
⊢ Eq (α := ENNReal)
      ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₂)) volume μH[(↑d₂ : ℝ)])
              μH[(↑d₂ : ℝ)] :
            (a : Set X) → ENNReal)
          s :
        ENNReal)
      (0 : ENNReal) ∨
    Eq (α := ENNReal)
      ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₁)) volume μH[(↑d₁ : ℝ)])
              μH[(↑d₁ : ℝ)] :
            (a : Set X) → ENNReal)
          s :
        ENNReal)
      (⊤ : ENNReal)
have inr : Eq (α := ENNReal)
  ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₁)) volume μH[(↑d₁ : ℝ)])
          μH[(↑d₁ : ℝ)] :
        (a : Set X) → ENNReal)
      s :
    ENNReal)
  (⊤ : ENNReal)
Tactic: right
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (goal)
Goal:
X : Type u_1
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
d₁ d₂ : ℕ
h_1 : d₁ < d₂
s : Set X
h : Eq (α := ENNReal) (((μH[(↑d₁ : ℝ)] : Measure X) : (a : Set X) → ENNReal) s : ENNReal) (⊤ : ENNReal)
⊢ Eq (α := ENNReal)
    ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₁)) volume μH[(↑d₁ : ℝ)])
            μH[(↑d₁ : ℝ)] :
          (a : Set X) → ENNReal)
        s :
      ENNReal)
    (⊤ : ENNReal)
have inr : Eq (α := ENNReal) (if addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₁)) volume μH[(↑d₁ : ℝ)] = 0 then 0 else ⊤) ⊤
Tactic: rw [smul_apply, h, ENNReal.smul_top]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : EMetricSpace Y
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
f : X → Y
d : ℕ
hf : Isometry f
s : Set X
⊢ HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ENNReal) (f '' s) : ENNReal) =
    HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ENNReal) s : ENNReal)
have rw : HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
    (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ENNReal) s : ENNReal) =
  HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
    (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ENNReal) s : ENNReal)
Tactic: rw [Isometry.hausdorffMeasure_image hf (by simp)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : EMetricSpace Y
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
f : X → Y
d : ℕ
hf : Isometry f
s : Set Y
⊢ HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal) =
    HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ENNReal) (s ∩ Set.range f) : ENNReal)
have rw : HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
    (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ENNReal) (s ∩ Set.range f) : ENNReal) =
  HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
    (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ENNReal) (s ∩ Set.range f) : ENNReal)
Tactic: rw [Isometry.hausdorffMeasure_preimage hf (by simp)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : EMetricSpace Y
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
f : X → Y
d : ℕ
hf : Isometry f
⊢ map f
      (HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
        μH[(↑d : ℝ)]) =
    (HSMul.hSMul (β := Measure Y) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
          μH[(↑d : ℝ)]).restrict
      (Set.range f)
have rw : HSMul.hSMul (β := Measure Y) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
    (map f μH[(↑d : ℝ)]) =
  (HSMul.hSMul (β := Measure Y) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
        μH[(↑d : ℝ)]).restrict
    (Set.range f)
Tactic: rw [Measure.map_smul, map_hausdorffMeasure hf (by simp), Measure.restrict_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : EMetricSpace Y
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
f : X → Y
d : ℕ
hf : Isometry f
rw :
  HSMul.hSMul (β := Measure Y) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (map f μH[(↑d : ℝ)]) =
    (HSMul.hSMul (β := Measure Y) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
          μH[(↑d : ℝ)]).restrict
      (Set.range f)
⊢ map f
      (HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
        μH[(↑d : ℝ)]) =
    (HSMul.hSMul (β := Measure Y) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
          μH[(↑d : ℝ)]).restrict
      (Set.range f)
have rw₁ : HSMul.hSMul (β := Measure Y) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
    (restrict μH[(↑d : ℝ)] (Set.range f)) =
  (HSMul.hSMul (β := Measure Y) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
        μH[(↑d : ℝ)]).restrict
    (Set.range f)
Tactic: rw [Measure.map_smul, map_hausdorffMeasure hf (by simp), Measure.restrict_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : EMetricSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : EMetricSpace Y
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
f : X → Y
d : ℕ
hf : Isometry f
rw :
  HSMul.hSMul (β := Measure Y) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (map f μH[(↑d : ℝ)]) =
    (HSMul.hSMul (β := Measure Y) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
          μH[(↑d : ℝ)]).restrict
      (Set.range f)
rw₁ :
  HSMul.hSMul (β := Measure Y) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (restrict μH[(↑d : ℝ)] (Set.range f)) =
    (HSMul.hSMul (β := Measure Y) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
          μH[(↑d : ℝ)]).restrict
      (Set.range f)
⊢ map f
      (HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
        μH[(↑d : ℝ)]) =
    (HSMul.hSMul (β := Measure Y) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
          μH[(↑d : ℝ)]).restrict
      (Set.range f)
have rw₂ : HSMul.hSMul (β := Measure Y) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
    (restrict μH[(↑d : ℝ)] (Set.range f)) =
  HSMul.hSMul (β := Measure Y) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
    (restrict μH[(↑d : ℝ)] (Set.range f))
Tactic: rw [Measure.map_smul, map_hausdorffMeasure hf (by simp), Measure.restrict_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (goal)
Goal:
𝕜 : Type u_3
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
d : ℕ
r : 𝕜
hr : r ≠ 0
s : Set E
⊢ ((μHE[d] : Measure E) : (a : Set E) → ENNReal) (r • s) =
    HSMul.hSMul (β := ENNReal) (‖r‖₊ ^ d) (((μHE[d] : Measure E) : (a : Set E) → ENNReal) s : ENNReal)
have rw : HPow.hPow (β := ℝ) ‖r‖₊ (↑d : ℝ) •
    HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure E) : (a : Set E) → ENNReal) s : ENNReal) =
  ‖r‖₊ ^ d •
    HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure E) : (a : Set E) → ENNReal) s : ENNReal)
Tactic: rw [euclideanHausdorffMeasure_def, Measure.smul_apply, hausdorffMeasure_smul₀ (by simp) hr,
    Measure.smul_apply, smul_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (goal)
Goal:
𝕜 : Type u_3
V : Type u_4
P : Type u_5
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : MeasurableSpace P
inst_4 : MetricSpace P
inst_5 : NormedAddTorsor V P
inst_6 : BorelSpace P
d : ℕ
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) ((⇑(AffineMap.homothety x c) : (a : P) → P) '' s) :
        ENNReal) =
    ‖c‖₊ ^ d •
      HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
        (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal)
have rw : addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)] •
    HSMul.hSMul (β := ENNReal) (HPow.hPow (β := ℝ) ‖c‖₊ (↑d : ℝ))
      (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal) =
  ‖c‖₊ ^ d •
    HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal)
Tactic: rw [hausdorffMeasure_homothety_image (by simp) x hc, smul_comm, NNReal.rpow_natCast]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (goal)
Goal:
𝕜 : Type u_3
V : Type u_4
P : Type u_5
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : MeasurableSpace P
inst_4 : MetricSpace P
inst_5 : NormedAddTorsor V P
inst_6 : BorelSpace P
d : ℕ
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
rw :
  addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)] •
      HSMul.hSMul (β := ENNReal) (HPow.hPow (β := ℝ) ‖c‖₊ (↑d : ℝ))
        (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal) =
    ‖c‖₊ ^ d •
      HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
        (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal)
⊢ HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) ((⇑(AffineMap.homothety x c) : (a : P) → P) '' s) :
        ENNReal) =
    ‖c‖₊ ^ d •
      HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
        (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal)
have rw₁ : HPow.hPow (β := ℝ) ‖c‖₊ (↑d : ℝ) •
    HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal) =
  ‖c‖₊ ^ d •
    HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal)
Tactic: rw [hausdorffMeasure_homothety_image (by simp) x hc, smul_comm, NNReal.rpow_natCast]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (goal)
Goal:
𝕜 : Type u_3
V : Type u_4
P : Type u_5
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : MeasurableSpace P
inst_4 : MetricSpace P
inst_5 : NormedAddTorsor V P
inst_6 : BorelSpace P
d : ℕ
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
rw :
  addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)] •
      HSMul.hSMul (β := ENNReal) (HPow.hPow (β := ℝ) ‖c‖₊ (↑d : ℝ))
        (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal) =
    ‖c‖₊ ^ d •
      HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
        (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal)
rw₁ :
  HPow.hPow (β := ℝ) ‖c‖₊ (↑d : ℝ) •
      HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
        (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal) =
    ‖c‖₊ ^ d •
      HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
        (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal)
⊢ HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) ((⇑(AffineMap.homothety x c) : (a : P) → P) '' s) :
        ENNReal) =
    ‖c‖₊ ^ d •
      HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
        (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal)
have rw₂ : ‖c‖₊ ^ d •
    HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal) =
  ‖c‖₊ ^ d •
    HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal)
Tactic: rw [hausdorffMeasure_homothety_image (by simp) x hc, smul_comm, NNReal.rpow_natCast]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (goal)
Goal:
𝕜 : Type u_3
V : Type u_4
P : Type u_5
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : MeasurableSpace P
inst_4 : MetricSpace P
inst_5 : NormedAddTorsor V P
inst_6 : BorelSpace P
d : ℕ
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) ((⇑(AffineMap.homothety x c) : (a : P) → P) ⁻¹' s) :
        ENNReal) =
    ‖c‖₊⁻¹ ^ d •
      HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
        (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal)
have rw : addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)] •
    HSMul.hSMul (β := ENNReal) (HPow.hPow (β := ℝ) ‖c‖₊⁻¹ (↑d : ℝ))
      (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal) =
  ‖c‖₊⁻¹ ^ d •
    HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal)
Tactic: rw [hausdorffMeasure_homothety_preimage (by simp) x hc, smul_comm, NNReal.rpow_natCast]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (goal)
Goal:
𝕜 : Type u_3
V : Type u_4
P : Type u_5
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : MeasurableSpace P
inst_4 : MetricSpace P
inst_5 : NormedAddTorsor V P
inst_6 : BorelSpace P
d : ℕ
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
rw :
  addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)] •
      HSMul.hSMul (β := ENNReal) (HPow.hPow (β := ℝ) ‖c‖₊⁻¹ (↑d : ℝ))
        (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal) =
    ‖c‖₊⁻¹ ^ d •
      HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
        (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal)
⊢ HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) ((⇑(AffineMap.homothety x c) : (a : P) → P) ⁻¹' s) :
        ENNReal) =
    ‖c‖₊⁻¹ ^ d •
      HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
        (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal)
have rw₁ : HPow.hPow (β := ℝ) ‖c‖₊⁻¹ (↑d : ℝ) •
    HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal) =
  ‖c‖₊⁻¹ ^ d •
    HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal)
Tactic: rw [hausdorffMeasure_homothety_preimage (by simp) x hc, smul_comm, NNReal.rpow_natCast]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (goal)
Goal:
𝕜 : Type u_3
V : Type u_4
P : Type u_5
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : MeasurableSpace P
inst_4 : MetricSpace P
inst_5 : NormedAddTorsor V P
inst_6 : BorelSpace P
d : ℕ
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
rw :
  addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)] •
      HSMul.hSMul (β := ENNReal) (HPow.hPow (β := ℝ) ‖c‖₊⁻¹ (↑d : ℝ))
        (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal) =
    ‖c‖₊⁻¹ ^ d •
      HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
        (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal)
rw₁ :
  HPow.hPow (β := ℝ) ‖c‖₊⁻¹ (↑d : ℝ) •
      HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
        (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal) =
    ‖c‖₊⁻¹ ^ d •
      HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
        (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal)
⊢ HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) ((⇑(AffineMap.homothety x c) : (a : P) → P) ⁻¹' s) :
        ENNReal) =
    ‖c‖₊⁻¹ ^ d •
      HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
        (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal)
have rw₂ : ‖c‖₊⁻¹ ^ d •
    HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal) =
  ‖c‖₊⁻¹ ^ d •
    HSMul.hSMul (β := ENNReal) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      (((μH[(↑d : ℝ)] : Measure P) : (a : Set P) → ENNReal) s : ENNReal)
Tactic: rw [hausdorffMeasure_homothety_preimage (by simp) x hc, smul_comm, NNReal.rpow_natCast]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (goal)
Goal:
d : ℕ
⊢ Eq (α := Measure (EuclideanSpace ℝ (Fin d))) μHE[d] volume
have rw : HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin d)))
    (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)]) μH[(↑d : ℝ)] =
  volume
Tactic: rw [euclideanHausdorffMeasure_def, ← isAddLeftInvariant_eq_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (goal)
Goal:
d : ℕ
rw :
  HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin d)))
      (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)]) μH[(↑d : ℝ)] =
    volume
⊢ Eq (α := Measure (EuclideanSpace ℝ (Fin d))) μHE[d] volume
have rw₁ : Eq (α := Measure (EuclideanSpace ℝ (Fin d))) volume volume
Tactic: rw [euclideanHausdorffMeasure_def, ← isAddLeftInvariant_eq_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (goal)
Goal:
V : Type u_3
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
⊢ Eq.{u_3 + 1} (α := Measure V) (μHE[finrank ℝ V] : Measure V) (volume : Measure V)
have rw : Eq (α := Measure V)
  (map (α := EuclideanSpace ℝ (Fin (finrank ℝ V)))
    (⇑(IsometryEquiv.symm (LinearIsometryEquiv.toIsometryEquiv (OrthonormalBasis.repr (stdOrthonormalBasis ℝ V)))) :
      (a : EuclideanSpace ℝ (Fin (finrank ℝ V))) → V)
    volume)
  (map (α := EuclideanSpace ℝ (Fin (finrank ℝ V)))
    (⇑(LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ V))) :
      (a : EuclideanSpace ℝ (Fin (finrank ℝ V))) → V)
    volume)
Tactic: rw [← (stdOrthonormalBasis ℝ V).measurePreserving_repr_symm.map_eq,
    ← (stdOrthonormalBasis ℝ V).repr.toIsometryEquiv
      |>.symm.measurePreserving_euclideanHausdorffMeasure _ |>.map_eq,
    EuclideanSpace.euclideanHausdorffMeasure_eq_volume]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (hypothesis)
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : MetricSpace P
inst_6 : MeasurableSpace P
inst_7 : BorelSpace P
inst_8 : NormedAddTorsor V P
p : P
⊢ Eq.{u_4 + 1} (α := Measure P) μHE[finrank ℝ V]
    (map.{u_3, u_4} (α := V) (⇑(IsometryEquiv.vaddConst p) : (a : V) → P) volume)
have h : Eq.{u_4 + 1} (α := Measure P)
  (map.{u_3, u_4} (α := V) (⇑(IsometryEquiv.vaddConst p : V ≃ᵢ P) : (a : V) → P) μHE[finrank ℝ V]) μHE[finrank ℝ V]
Tactic: have h := (IsometryEquiv.vaddConst p)
    |>.measurePreserving_euclideanHausdorffMeasure (finrank ℝ V) |>.map_eq