awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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)
inr :
  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)

Tactic:
right
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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)
inr :
  Eq (α := ENNReal) (if addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₁)) volume μH[(↑d₁ : ℝ)] = 0 then 0 else ⊤) ⊤
⊢ Eq (α := ENNReal)
    ((HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₁)) volume μH[(↑d₁ : ℝ)])
            μH[(↑d₁ : ℝ)] :
          (a : Set X) → ENNReal)
        s :
      ENNReal)
    (⊤ : ENNReal)

Tactic:
rw [smul_apply, h, ENNReal.smul_top]

Premises used: ENNReal.smul_top, MeasureTheory.Measure.smul_apply
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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) (if addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d₁)) volume μH[(↑d₁ : ℝ)] = 0 then 0 else ⊤) ⊤

Tactic:
simp [addHaarScalarFactor_volume_hausdorffMeasure_ne_zero]

Premises used: MeasureTheory.Measure.addHaarScalarFactor_volume_hausdorffMeasure_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
e : X ≃ᵢ Y
d : ℕ
⊢ MeasurePreserving.{u_1, u_2} (α := X) (β := Y) (⇑e : (a : X) → Y) μHE[d] μHE[d]

Tactic:
(IsometryEquiv.measurePreserving_hausdorffMeasure e d).smul_measure _

Premises used: MeasureTheory.MeasurePreserving.smul_measure, MeasureTheory.Measure.euclideanHausdorffMeasure, Nat.cast, IsometryEquiv.measurePreserving_hausdorffMeasure
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
⊢ LE.le (α := ℝ) 0 (↑d : ℝ) ∨ Function.Surjective f

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
rw 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)
⊢ 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)

Tactic:
rw [Isometry.hausdorffMeasure_image hf (by simp)]

Premises used: Isometry.hausdorffMeasure_image
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
⊢ LE.le (α := ℝ) 0 (↑d : ℝ) ∨ Function.Surjective f

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
rw 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)
⊢ 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)

Tactic:
rw [Isometry.hausdorffMeasure_preimage hf (by simp)]

Premises used: Isometry.hausdorffMeasure_preimage
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
⊢ LE.le (α := ℝ) 0 (↑d : ℝ) ∨ Function.Surjective f

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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)
rw₂ 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))
⊢ 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)

Tactic:
rw [Measure.map_smul, map_hausdorffMeasure hf (by simp), Measure.restrict_smul]

Premises used: MeasureTheory.Measure.restrict_smul, Isometry.map_hausdorffMeasure, MeasureTheory.Measure.map_smul
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
⊢ LE.le (α := ℝ) 0 (↑d : ℝ)

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
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)
⊢ ((μ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)

Tactic:
rw [euclideanHausdorffMeasure_def, Measure.smul_apply, hausdorffMeasure_smul₀ (by simp) hr,
    Measure.smul_apply, smul_comm]

Premises used: MeasureTheory.Measure.hausdorffMeasure_smul₀, MeasureTheory.Measure.smul_apply, SMulCommClass.smul_comm, MeasureTheory.Measure.euclideanHausdorffMeasure_def
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
⊢ 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:
simp
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
⊢ LE.le (α := ℝ) 0 (↑d : ℝ)

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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)
rw₂ 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)
⊢ 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)

Tactic:
rw [hausdorffMeasure_homothety_image (by simp) x hc, smul_comm, NNReal.rpow_natCast]

Premises used: NNReal.rpow_natCast, MeasureTheory.hausdorffMeasure_homothety_image, SMulCommClass.smul_comm
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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)
rw₂ 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)
⊢ 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)

Tactic:
rw [hausdorffMeasure_homothety_preimage (by simp) x hc, smul_comm, NNReal.rpow_natCast]

Premises used: NNReal.rpow_natCast, SMulCommClass.smul_comm, MeasureTheory.hausdorffMeasure_homothety_preimage
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
d : ℕ
rw :
  HSMul.hSMul (β := Measure (EuclideanSpace ℝ (Fin d)))
      (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)]) μH[(↑d : ℝ)] =
    volume
rw₁ rw₂ : Eq (α := Measure (EuclideanSpace ℝ (Fin d))) volume volume
⊢ Eq (α := Measure (EuclideanSpace ℝ (Fin d))) μHE[d] volume

Tactic:
rw [euclideanHausdorffMeasure_def, ← isAddLeftInvariant_eq_smul]

Premises used: MeasureTheory.Measure.isAddLeftInvariant_eq_smul, MeasureTheory.Measure.euclideanHausdorffMeasure_def
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
V : Type u_3
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
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)
⊢ Eq.{u_3 + 1} (α := Measure V) (μHE[finrank ℝ V] : Measure V) (volume : Measure V)

Tactic:
rw [← (stdOrthonormalBasis ℝ V).measurePreserving_repr_symm.map_eq,
    ← (stdOrthonormalBasis ℝ V).repr.toIsometryEquiv
      |>.symm.measurePreserving_euclideanHausdorffMeasure _ |>.map_eq,
    EuclideanSpace.euclideanHausdorffMeasure_eq_volume]

Premises used: Real, OrthonormalBasis.repr, IsometryEquiv.symm, MeasureTheory.MeasurePreserving.map_eq, LinearIsometryEquiv.toIsometryEquiv, OrthonormalBasis.measurePreserving_repr_symm, EuclideanSpace.euclideanHausdorffMeasure_eq_volume, IsometryEquiv.measurePreserving_euclideanHausdorffMeasure, stdOrthonormalBasis
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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 (α := 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:
simp
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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)
    (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
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
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]
⊢ Eq.{u_4 + 1} (α := Measure P)
    (map.{u_3, u_4} (α := V) (⇑(IsometryEquiv.vaddConst p : V ≃ᵢ P) : (a : V) → P) (volume : Measure V))
    μHE[finrank ℝ V]

Tactic:
rw [InnerProductSpace.euclideanHausdorffMeasure_eq_volume] at h

Premises used: InnerProductSpace.euclideanHausdorffMeasure_eq_volume
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
h :
  Eq.{u_4 + 1} (α := Measure P)
    (map.{u_3, u_4} (α := V) (⇑(IsometryEquiv.vaddConst p : V ≃ᵢ P) : (a : V) → P) (volume : Measure V))
    μHE[finrank ℝ V]
⊢ Eq.{u_4 + 1} (α := Measure P) μHE[finrank ℝ V]
    (map.{u_3, u_4} (α := V) (⇑(IsometryEquiv.vaddConst p) : (a : V) → P) volume)

Tactic:
h.symm

Premises used: Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
h :
  Eq.{u_4 + 1} (α := Measure P)
    (map.{u_3, u_4} (α := V) (⇑(IsometryEquiv.vaddConst p : V ≃ᵢ P) : (a : V) → P) (volume : Measure V))
    μHE[finrank ℝ V]
⊢ Eq.{u_4 + 1} (α := Measure P) μHE[finrank ℝ V]
    (map.{u_3, u_4} (α := V) (⇑(IsometryEquiv.vaddConst p) : (a : V) → P) volume)

Tactic:
exact h.symm

Premises used: Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : MeasurableSpace P
inst_4 : BorelSpace P
inst_5 : NormedAddTorsor V P
d : ℕ
s : AffineSubspace ℝ P
t : Set ↥s
⊢ Eq (α := ENNReal)
    (((μHE[d] : Measure P) : (a : Set P) → ENNReal) (Subtype.val (p := fun (x : P) ↦ x ∈ s) '' t) : ENNReal)
    (((μHE[d] : Measure ↥s) : (a : Set ↥s) → ENNReal) t : ENNReal)

Tactic:
isometry_subtype_coe.euclideanHausdorffMeasure_image _

Premises used: Isometry.euclideanHausdorffMeasure_image
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
V : Type u_3
P : Type u_4
inst_6 : NormedAddCommGroup V
inst_7 : InnerProductSpace ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
inst_10 : FiniteDimensional ℝ V
inst_11 : MetricSpace P
inst_12 : MeasurableSpace P
inst_13 : BorelSpace P
inst_14 : NormedAddTorsor V P
α : Type u_5
inst_15 : AddGroup α
inst_16 : AddAction α X
inst_17 : IsIsometricVAdd α X
d : ℕ
⊢ VAddInvariantMeasure α X
    (HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      μH[(↑d : ℝ)])

Tactic:
infer_instance
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
V : Type u_3
P : Type u_4
inst_6 : NormedAddCommGroup V
inst_7 : InnerProductSpace ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
inst_10 : FiniteDimensional ℝ V
inst_11 : MetricSpace P
inst_12 : MeasurableSpace P
inst_13 : BorelSpace P
inst_14 : NormedAddTorsor V P
inst_15 : AddGroup X
inst_16 : IsIsometricVAdd X X
d : ℕ
⊢ (HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      μH[(↑d : ℝ)]).IsAddLeftInvariant

Tactic:
infer_instance
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
V : Type u_3
P : Type u_4
inst_6 : NormedAddCommGroup V
inst_7 : InnerProductSpace ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
inst_10 : FiniteDimensional ℝ V
inst_11 : MetricSpace P
inst_12 : MeasurableSpace P
inst_13 : BorelSpace P
inst_14 : NormedAddTorsor V P
inst_15 : AddGroup X
inst_16 : IsIsometricVAdd Xᵃᵒᵖ X
d : ℕ
⊢ (HSMul.hSMul (β := Measure X) (addHaarScalarFactor (G := EuclideanSpace ℝ (Fin d)) volume μH[(↑d : ℝ)])
      μH[(↑d : ℝ)]).IsAddRightInvariant

Tactic:
infer_instance
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
s : Submodule ℝ V
p q : P
⊢ Eq.{u_3 + 1} (α := ↥s × ↥sᗮ)
    (((s.measurableEquivProd p : MeasurableEquiv.{u_4, u_3} P (↥s × ↥sᗮ)) : (a : P) → ↥s × ↥sᗮ) q : ↥s × ↥sᗮ)
    (((s.orthogonalProjection : (a : V) → ↥s) (q -ᵥ p), (sᗮ.orthogonalProjection : (a : V) → ↥sᗮ) (q -ᵥ p)) : ↥s × ↥sᗮ)

Tactic:
simp [measurableEquivProd]

Premises used: Submodule.measurableEquivProd
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
s : Submodule ℝ V
p : P
q : ↥s × ↥sᗮ
⊢ (MeasurableEquiv.symm (s.measurableEquivProd p) : (a : ↥s × ↥sᗮ) → P) q = ((↑q.1 : V) + (↑q.2 : V)) +ᵥ p

Tactic:
simp [measurableEquivProd]

Premises used: Submodule.measurableEquivProd