awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
f : E →ₗ[ℝ] E := HSMul.hSMul (β := E →ₗ[ℝ] E) r 1
change : map (⇑f : (a : E) → E) μ = ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ
⊢ map (fun (x : E) ↦ r • x) μ = ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ

Tactic:
change Measure.map f μ = _

Premises used: MeasureTheory.Measure.map, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
f : E →ₗ[ℝ] E := HSMul.hSMul (β := E →ₗ[ℝ] E) r 1
simp : ¬r ^ finrank ℝ E = 0
⊢ Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)

Tactic:
simp only [f, mul_one, LinearMap.det_smul, Ne, map_one]

Premises used: Ne, map_one, LinearMap.det_smul, mul_one
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
f : E →ₗ[ℝ] E := HSMul.hSMul (β := E →ₗ[ℝ] E) r 1
⊢ ¬r ^ finrank ℝ E = 0

Tactic:
pow_ne_zero _ hr

Premises used: pow_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
f : E →ₗ[ℝ] E := HSMul.hSMul (β := E →ₗ[ℝ] E) r 1
⊢ ¬r ^ finrank ℝ E = 0

Tactic:
exact pow_ne_zero _ hr

Premises used: pow_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
f : E →ₗ[ℝ] E := HSMul.hSMul (β := E →ₗ[ℝ] E) r 1
⊢ Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)

Tactic:
have hf : LinearMap.det f ≠ 0 := by
    simp only [f, mul_one, LinearMap.det_smul, Ne, map_one]
    exact pow_ne_zero _ hr
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
f : E →ₗ[ℝ] E := HSMul.hSMul (β := E →ₗ[ℝ] E) r 1
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
⊢ map (⇑f : (a : E) → E) μ = ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ

Tactic:
simp only [f, map_linearMap_addHaar_eq_smul_addHaar μ hf, mul_one, LinearMap.det_smul, map_one]

Premises used: MeasureTheory.Measure.map_linearMap_addHaar_eq_smul_addHaar, map_one, LinearMap.det_smul, mul_one
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
⊢ QuasiMeasurePreserving (fun (x : E) ↦ r • x) μ μ

Tactic:
⟨measurable_const_smul r, ?_⟩

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.mk, MeasurableConstSMul.measurable_const_smul
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
refine : map (fun (x : E) ↦ r • x) μ ≪ μ
⊢ QuasiMeasurePreserving (fun (x : E) ↦ r • x) μ μ

Tactic:
refine ⟨measurable_const_smul r, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
rw : ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ ≪ μ
⊢ map (fun (x : E) ↦ r • x) μ ≪ μ

Tactic:
rw [map_addHaar_smul μ hr]

Premises used: MeasureTheory.Measure.map_addHaar_smul
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
⊢ ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ ≪ μ

Tactic:
smul_absolutelyContinuous

Premises used: MeasureTheory.Measure.smul_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
⊢ ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ ≪ μ

Tactic:
exact smul_absolutelyContinuous

Premises used: MeasureTheory.Measure.smul_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
s : Set E
rw :
  (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ : (a : Set E) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  HSMul.hSMul (β := (a : Set E) → ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) (⇑μ : (a : Set E) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
rw₂ :
  HSMul.hSMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
rw₃ rw₄ :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((map (fun (x : E) ↦ r • x) μ : Measure E) : (a : Set E) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [map_addHaar_smul μ hr, coe_smul, Pi.smul_apply, smul_eq_mul]

Premises used: MeasureTheory.Measure.coe_smul, MeasureTheory.Measure.map_addHaar_smul, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
s : Set E
inl :
  ∀ (h : r ≠ 0),
    (μ : (a : Set E) → ℝ≥0∞) (r • s) =
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
inr :
  (μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := ℝ) 0 s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (r • s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rcases ne_or_eq r 0 with (h | rfl)

Premises used: ne_or_eq, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
s : Set E
h : r ≠ 0
inl :
  (μ : (a : Set E) → ℝ≥0∞) ((fun (x : E) ↦ r⁻¹ • x) ⁻¹' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
inl₁ :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r⁻¹ ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
inl₂ :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
inl₃ inl₄ :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (r • s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← preimage_smul_inv₀ h, addHaar_preimage_smul μ (inv_ne_zero h), inv_pow, inv_inv]

Premises used: Set.preimage_smul_inv₀, MeasureTheory.Measure.addHaar_preimage_smul, inv_pow, inv_inv, inv_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
inr :
  (μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := ℝ) (β := Set E) 0 ∅) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) ∅ : ℝ≥0∞)
inr₁ :
  ∀ (hs : s.Nonempty),
    (μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := ℝ) 0 s) =
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := ℝ) 0 s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hs)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
⊢ (μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := ℝ) (β := Set E) 0 ∅) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) ∅ : ℝ≥0∞)

Tactic:
simp only [measure_empty, mul_zero, smul_set_empty]

Premises used: Set.smul_set_empty, MeasureTheory.measure_empty, MulZeroClass.mul_zero
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : s.Nonempty
inr :
  (μ : (a : Set E) → ℝ≥0∞) {0} =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := ℝ) 0 s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [zero_smul_set hs, ← singleton_zero]

Premises used: Set.zero_smul_set, Set.singleton_zero
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : s.Nonempty
pos :
  ∀ (h : finrank ℝ E = 0),
    (μ : (a : Set E) → ℝ≥0∞) {0} =
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
neg :
  ∀ (h : ¬finrank ℝ E = 0),
    (μ : (a : Set E) → ℝ≥0∞) {0} =
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) {0} =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
by_cases h : finrank ℝ E = 0

Premises used: Real, Module.finrank
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : s.Nonempty
h : finrank ℝ E = 0
⊢ Subsingleton E

Tactic:
haveI : Subsingleton E := finrank_zero_iff.1 h
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : s.Nonempty
h : finrank ℝ E = 0
this : Subsingleton E
⊢ (μ : (a : Set E) → ℝ≥0∞) {0} =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [h, one_mul, ENNReal.ofReal_one, abs_one, Subsingleton.eq_univ_of_nonempty hs,
      pow_zero, Subsingleton.eq_univ_of_nonempty (singleton_nonempty (0 : E))]

Premises used: Set.singleton_nonempty, ENNReal.ofReal_one, pow_zero, Subsingleton.eq_univ_of_nonempty, abs_one, OfNat.ofNat, one_mul
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : s.Nonempty
h : ¬finrank ℝ E = 0
⊢ Nontrivial E

Tactic:
haveI : Nontrivial E := nontrivial_of_finrank_pos (bot_lt_iff_ne_bot.2 h)
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : s.Nonempty
h : ¬finrank ℝ E = 0
this : Nontrivial E
⊢ (μ : (a : Set E) → ℝ≥0∞) {0} =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [h, zero_mul, ENNReal.ofReal_zero, abs_zero, Ne, not_false_iff,
      zero_pow, measure_singleton]

Premises used: MulZeroClass.zero_mul, Ne, MeasureTheory.NoAtoms.measure_singleton, abs_zero, ENNReal.ofReal_zero, not_false_iff, zero_pow
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : 0 ≤ r
s : Set E
rw :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (|r| ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
rw₂ rw₃ :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (r • s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [addHaar_smul, abs_pow, abs_of_nonneg hr]

Premises used: abs_of_nonneg, abs_pow, MeasureTheory.Measure.addHaar_smul
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ≥0
s : Set E
⊢ (μ : (a : Set E) → ℝ≥0∞) (r • s) =
    HMul.hMul (β := ℝ≥0∞) ((↑r : ℝ≥0∞) ^ finrank ℝ E) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [NNReal.smul_def]

Premises used: NNReal.smul_def
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : NullMeasurableSet s μ
r : ℝ
inl : ∀ (hs : NullMeasurableSet ∅ μ), NullMeasurableSet (HSMul.hSMul (β := Set E) r ∅) μ
inr : ∀ (hs' : s.Nonempty), NullMeasurableSet (r • s) μ
⊢ NullMeasurableSet (r • s) μ

Tactic:
obtain rfl | hs' := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hs : NullMeasurableSet ∅ μ
⊢ NullMeasurableSet (HSMul.hSMul (β := Set E) r ∅) μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : NullMeasurableSet s μ
r : ℝ
hs' : s.Nonempty
inr : NullMeasurableSet (HSMul.hSMul (α := ℝ) 0 s) μ
inr₁ : ∀ (hr : r ≠ 0), NullMeasurableSet (r • s) μ
⊢ NullMeasurableSet (r • s) μ

Tactic:
obtain rfl | hr := eq_or_ne r 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : NullMeasurableSet s μ
hs' : s.Nonempty
⊢ NullMeasurableSet (HSMul.hSMul (α := ℝ) 0 s) μ

Tactic:
simpa [zero_smul_set hs'] using nullMeasurableSet_singleton _

Premises used: MeasureTheory.nullMeasurableSet_singleton, Set.zero_smul_set
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : NullMeasurableSet s μ
r : ℝ
hs' : s.Nonempty
hr : r ≠ 0
inr : ∀ (t : Set E) (ht : MeasurableSet t) (hst : s =ᶠ[ae μ] t), NullMeasurableSet (r • s) μ
⊢ NullMeasurableSet (r • s) μ

Tactic:
obtain ⟨t, ht, hst⟩ := hs
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
r : ℝ
hs' : s.Nonempty
hr : r ≠ 0
t : Set E
ht : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ NullMeasurableSet (r • s) μ

Tactic:
⟨_, ht.const_smul_of_ne_zero hr, ?_⟩

Premises used: MeasurableSet, MeasureTheory.NullMeasurableSet, MeasurableSet.const_smul_of_ne_zero, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
r : ℝ
hs' : s.Nonempty
hr : r ≠ 0
t : Set E
ht : MeasurableSet t
hst : s =ᶠ[ae μ] t
inr : r • s =ᶠ[ae μ] r • t
⊢ NullMeasurableSet (r • s) μ

Tactic:
refine ⟨_, ht.const_smul_of_ne_zero hr, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
r : ℝ
hs' : s.Nonempty
hr : r ≠ 0
t : Set E
ht : MeasurableSet t
hst : s =ᶠ[ae μ] t
inr :
  ∀ (hst : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (symmDiff s t) : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (symmDiff (r • s) (r • t)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ r • s =ᶠ[ae μ] r • t

Tactic:
rw [← measure_symmDiff_eq_zero_iff] at hst ⊢

Premises used: MeasureTheory.measure_symmDiff_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
r : ℝ
hs' : s.Nonempty
hr : r ≠ 0
t : Set E
ht : MeasurableSet t
hst : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (symmDiff s t) : ℝ≥0∞) (0 : ℝ≥0∞)
inr : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (r • symmDiff s t) : ℝ≥0∞) (0 : ℝ≥0∞)
inr₁ : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) (symmDiff s t) : ℝ≥0∞) = 0
inr₂ : ENNReal.ofReal |r ^ finrank ℝ E| * 0 = 0
inr₃ inr₄ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (symmDiff (r • s) (r • t)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← smul_set_symmDiff₀ hr, addHaar_smul μ, hst, mul_zero]

Premises used: MulZeroClass.mul_zero, Set.smul_set_symmDiff₀, MeasureTheory.Measure.addHaar_smul
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
x : E
r : ℝ
s : Set E
simp :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ((⇑(AffineMap.homothety x r) : (a : E) → E) '' s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) ((fun (x_1 : E) ↦ r • (x_1 - x) + x) '' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ((⇑(AffineMap.homothety x r) : (a : E) → E) '' s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) ((fun (y : E) ↦ y + x) '' HSMul.hSMul (β := Set E) r ((fun (y : E) ↦ y + -x) '' s)) :
      ℝ≥0∞)

Tactic:
simp only [← image_smul, image_image, ← sub_eq_add_neg]

Premises used: Set.image_image, Set.image_smul, sub_eq_add_neg
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
x : E
r : ℝ
s : Set E
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ((⇑(AffineMap.homothety x r) : (a : E) → E) '' s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) ((fun (x_1 : E) ↦ r • (x_1 - x) + x) '' s) : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
x : E
r : ℝ
s : Set E
⊢ (μ : (a : Set E) → ℝ≥0∞) ((fun (y : E) ↦ y + x) '' HSMul.hSMul (β := Set E) r ((fun (y : E) ↦ y + -x) '' s)) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [image_add_right, measure_preimage_add_right, addHaar_smul]

Premises used: Set.image_add_right, MeasureTheory.measure_preimage_add_right, MeasureTheory.Measure.addHaar_smul
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
μ : Measure E
inst_3 : μ.IsAddHaarMeasure
x : E
r : ℝ
⊢ Eq (α := Set E) (ball 0 r) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' ball x r)

Tactic:
simp [preimage_add_ball]

Premises used: preimage_add_ball
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
μ : Measure E
inst_3 : μ.IsAddHaarMeasure
x : E
r : ℝ
⊢ Eq (α := Set E) (ball 0 r) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' ball x r)

Tactic:
have : ball (0 : E) r = (x + ·) ⁻¹' ball x r := by simp [preimage_add_ball]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
μ : Measure E
inst_3 : μ.IsAddHaarMeasure
x : E
r : ℝ
this : Eq (α := Set E) (ball 0 r) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' ball x r)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' ball x r) : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 r) : ℝ≥0∞)

Tactic:
rw [this, measure_preimage_add]

Premises used: MeasureTheory.measure_preimage_add