awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ
⊢ μ.real (ball x r) = μ.real (ball 0 r)

Tactic:
simp [measureReal_def, addHaar_ball_center]

Premises used: MeasureTheory.Measure.addHaar_ball_center, MeasureTheory.measureReal_def
-- 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) (closedBall 0 r) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' closedBall x r)

Tactic:
simp [preimage_add_closedBall]

Premises used: preimage_add_closedBall
-- 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) (closedBall 0 r) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' closedBall x r)

Tactic:
have : closedBall (0 : E) r = (x + ·) ⁻¹' closedBall x r := by simp [preimage_add_closedBall]
-- 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) (closedBall 0 r) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' closedBall x r)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' closedBall x r) : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 r) : ℝ≥0∞)

Tactic:
rw [this, measure_preimage_add]

Premises used: MeasureTheory.measure_preimage_add
-- 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 : ℝ
⊢ μ.real (closedBall x r) = μ.real (closedBall 0 r)

Tactic:
simp [measureReal_def, addHaar_closedBall_center]

Premises used: MeasureTheory.measureReal_def, MeasureTheory.Measure.addHaar_closedBall_center
-- 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 : ℝ
hr : 0 < r
s : ℝ
⊢ ball 0 (r * s) = HSMul.hSMul (β := Set E) r (ball 0 s)

Tactic:
simp only [_root_.smul_ball hr.ne' (0 : E) s, Real.norm_eq_abs, abs_of_nonneg hr.le, smul_zero]

Premises used: smul_zero, LT.lt.le, LT.lt.ne', abs_of_nonneg, smul_ball, OfNat.ofNat, Real.norm_eq_abs
-- 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 : ℝ
hr : 0 < r
s : ℝ
⊢ ball 0 (r * s) = HSMul.hSMul (β := Set E) r (ball 0 s)

Tactic:
have : ball (0 : E) (r * s) = r • ball (0 : E) s := by
    simp only [_root_.smul_ball hr.ne' (0 : E) s, Real.norm_eq_abs, abs_of_nonneg hr.le, smul_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
x : E
r : ℝ
hr : 0 < r
s : ℝ
this : ball 0 (r * s) = HSMul.hSMul (β := Set E) r (ball 0 s)
⊢ (μ : (a : Set E) → ℝ≥0∞) (ball x (r * s)) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 s) : ℝ≥0∞)

Tactic:
simp only [this, addHaar_smul, abs_of_nonneg hr.le, addHaar_ball_center, abs_pow]

Premises used: MeasureTheory.Measure.addHaar_ball_center, LT.lt.le, 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
x : E
r : ℝ
hr : 0 < r
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x (r * 1)) : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (ball x r) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)

Tactic:
rw [← addHaar_ball_mul_of_pos μ x hr, mul_one]

Premises used: MeasureTheory.Measure.addHaar_ball_mul_of_pos, 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
inst_6 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
inl :
  ∀ (hr : LE.le (α := ℝ) 0 0),
    (μ : (a : Set E) → ℝ≥0∞) (ball x (0 * s)) =
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (HPow.hPow (α := ℝ) 0 (finrank ℝ E)))
        ((μ : (a : Set E) → ℝ≥0∞) (ball 0 s) : ℝ≥0∞)
inr :
  ∀ (h : 0 < r),
    (μ : (a : Set E) → ℝ≥0∞) (ball x (r * s)) =
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 s) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (ball x (r * s)) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 s) : ℝ≥0∞)

Tactic:
rcases hr.eq_or_lt with (rfl | h)

Premises used: LE.le.eq_or_lt, 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
inst_6 : Nontrivial E
x : E
s : ℝ
hr : LE.le (α := ℝ) 0 0
⊢ (μ : (a : Set E) → ℝ≥0∞) (ball x (0 * s)) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (HPow.hPow (α := ℝ) 0 (finrank ℝ E)))
      ((μ : (a : Set E) → ℝ≥0∞) (ball 0 s) : ℝ≥0∞)

Tactic:
simp only [zero_pow (finrank_pos (R := ℝ) (M := E)).ne', measure_empty, zero_mul,
      ENNReal.ofReal_zero, ball_zero]

Premises used: MulZeroClass.zero_mul, Metric.ball_zero, MeasureTheory.measure_empty, LT.lt.ne', ENNReal.ofReal_zero, zero_pow, Module.finrank_pos
-- 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
inst_6 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
h : 0 < r
⊢ (μ : (a : Set E) → ℝ≥0∞) (ball x (r * s)) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 s) : ℝ≥0∞)

Tactic:
addHaar_ball_mul_of_pos μ x h s

Premises used: MeasureTheory.Measure.addHaar_ball_mul_of_pos
-- 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
inst_6 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
h : 0 < r
⊢ (μ : (a : Set E) → ℝ≥0∞) (ball x (r * s)) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 s) : ℝ≥0∞)

Tactic:
exact addHaar_ball_mul_of_pos μ x h s

Premises used: MeasureTheory.Measure.addHaar_ball_mul_of_pos
-- 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
inst_6 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x (r * 1)) : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (ball x r) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)

Tactic:
rw [← addHaar_ball_mul μ x hr, mul_one]

Premises used: MeasureTheory.Measure.addHaar_ball_mul, 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
x : E
r : ℝ
hr : 0 < r
s : ℝ
⊢ closedBall 0 (r * s) = HSMul.hSMul (β := Set E) r (closedBall 0 s)

Tactic:
simp [smul_closedBall' hr.ne' (0 : E), abs_of_nonneg hr.le]

Premises used: smul_closedBall', LT.lt.le, LT.lt.ne', abs_of_nonneg, OfNat.ofNat
-- 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 : ℝ
hr : 0 < r
s : ℝ
⊢ closedBall 0 (r * s) = HSMul.hSMul (β := Set E) r (closedBall 0 s)

Tactic:
have : closedBall (0 : E) (r * s) = r • closedBall (0 : E) s := by
    simp [smul_closedBall' hr.ne' (0 : E), abs_of_nonneg hr.le]
-- 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 : ℝ
hr : 0 < r
s : ℝ
this : closedBall 0 (r * s) = HSMul.hSMul (β := Set E) r (closedBall 0 s)
⊢ (μ : (a : Set E) → ℝ≥0∞) (closedBall x (r * s)) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 s) : ℝ≥0∞)

Tactic:
simp only [this, addHaar_smul, abs_of_nonneg hr.le, addHaar_closedBall_center, abs_pow]

Premises used: LT.lt.le, abs_of_nonneg, MeasureTheory.Measure.addHaar_closedBall_center, 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
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
hs : 0 ≤ s
⊢ closedBall 0 (r * s) = HSMul.hSMul (β := Set E) r (closedBall 0 s)

Tactic:
simp [smul_closedBall r (0 : E) hs, abs_of_nonneg hr]

Premises used: abs_of_nonneg, OfNat.ofNat, smul_closedBall
-- 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 : ℝ
hr : 0 ≤ r
s : ℝ
hs : 0 ≤ s
⊢ closedBall 0 (r * s) = HSMul.hSMul (β := Set E) r (closedBall 0 s)

Tactic:
have : closedBall (0 : E) (r * s) = r • closedBall (0 : E) s := by
    simp [smul_closedBall r (0 : E) hs, abs_of_nonneg 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
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
hs : 0 ≤ s
this : closedBall 0 (r * s) = HSMul.hSMul (β := Set E) r (closedBall 0 s)
⊢ (μ : (a : Set E) → ℝ≥0∞) (closedBall x (r * s)) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 s) : ℝ≥0∞)

Tactic:
simp only [this, addHaar_smul, abs_of_nonneg hr, addHaar_closedBall_center, abs_pow]

Premises used: abs_of_nonneg, MeasureTheory.Measure.addHaar_closedBall_center, 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
x : E
r : ℝ
hr : 0 ≤ r
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (closedBall x (r * 1)) : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (closedBall x r) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)

Tactic:
rw [← addHaar_closedBall_mul μ x hr zero_le_one, mul_one]

Premises used: zero_le_one, MeasureTheory.Measure.addHaar_closedBall_mul, 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
x : E
r : ℝ
hr : 0 ≤ r
simp : 0 ≤ r ^ finrank ℝ E ∨ ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1)) = 0
⊢ μ.real (closedBall x r) = r ^ finrank ℝ E * μ.real (closedBall 0 1)

Tactic:
simp only [measureReal_def, addHaar_closedBall' μ x hr, ENNReal.toReal_mul, mul_eq_mul_right_iff,
    ENNReal.toReal_ofReal_eq_iff]

Premises used: mul_eq_mul_right_iff, ENNReal.toReal_mul, MeasureTheory.measureReal_def, ENNReal.toReal_ofReal_eq_iff, MeasureTheory.Measure.addHaar_closedBall'
-- 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 : ℝ
hr : 0 ≤ r
h : 0 ≤ r ^ finrank ℝ E
⊢ 0 ≤ r ^ finrank ℝ E ∨ ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1)) = 0

Tactic:
left
-- 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 : ℝ
hr : 0 ≤ r
⊢ 0 ≤ r ^ finrank ℝ E

Tactic:
positivity
-- 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
apply :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)

Tactic:
apply le_antisymm _ (measure_mono ball_subset_closedBall)

Premises used: Metric.ball_subset_closedBall, le_antisymm, MeasureTheory.measure_mono
-- 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
⊢ ENNReal.ofReal (HPow.hPow (α := ℝ) 1 (finrank ℝ E)) ≠ 0 ∨
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) (∞ : ℝ≥0∞)

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
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    ENNReal.ofReal (HPow.hPow (α := ℝ) 1 (finrank ℝ E)) ≠ ∞

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
refine :
  Tendsto (fun (r : ℝ) ↦ ENNReal.ofReal (r ^ finrank ℝ E)) (𝓝[<] 1)
    (𝓝 (ENNReal.ofReal (HPow.hPow (α := ℝ) 1 (finrank ℝ E))))
⊢ Tendsto
    (fun (r : ℝ) ↦
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞))
    (𝓝[<] 1)
    (𝓝
      (HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (HPow.hPow (α := ℝ) 1 (finrank ℝ E)))
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)))

Tactic:
refine ENNReal.Tendsto.mul ?_ (by simp) tendsto_const_nhds (by simp)

Premises used: ENNReal.Tendsto.mul, tendsto_const_nhds
-- 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
⊢ Tendsto (fun (r : ℝ) ↦ ENNReal.ofReal (r ^ finrank ℝ E)) (𝓝[<] 1)
    (𝓝 (ENNReal.ofReal (HPow.hPow (α := ℝ) 1 (finrank ℝ E))))

Tactic:
ENNReal.tendsto_ofReal ((tendsto_id'.2 nhdsWithin_le_nhds).pow _)

Premises used: Iff.mpr, Filter.tendsto_id', Filter.Tendsto.pow, nhdsWithin_le_nhds, ENNReal.tendsto_ofReal
-- 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
⊢ Tendsto (fun (r : ℝ) ↦ ENNReal.ofReal (r ^ finrank ℝ E)) (𝓝[<] 1)
    (𝓝 (ENNReal.ofReal (HPow.hPow (α := ℝ) 1 (finrank ℝ E))))

Tactic:
exact ENNReal.tendsto_ofReal ((tendsto_id'.2 nhdsWithin_le_nhds).pow _)

Premises used: Iff.mpr, Filter.tendsto_id', Filter.Tendsto.pow, nhdsWithin_le_nhds, ENNReal.tendsto_ofReal
-- 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
⊢ Tendsto
    (fun (r : ℝ) ↦
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞))
    (𝓝[<] 1)
    (𝓝
      (HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (HPow.hPow (α := ℝ) 1 (finrank ℝ E)))
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)))

Tactic:
have A : Tendsto
      (fun r : ℝ => ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall (0 : E) 1)) (𝓝[<] 1)
        (𝓝 (ENNReal.ofReal ((1 : ℝ) ^ finrank ℝ E) * μ (closedBall (0 : E) 1))) := by
    refine ENNReal.Tendsto.mul ?_ (by simp) tendsto_const_nhds (by simp)
    exact ENNReal.tendsto_ofReal ((tendsto_id'.2 nhdsWithin_le_nhds).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
A :
  Tendsto
    (fun (r : ℝ) ↦
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞))
    (𝓝[<] 1)
    (𝓝
      (HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (HPow.hPow (α := ℝ) 1 (finrank ℝ E)))
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞))
    (𝓝[<] 1) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1)) : Filter ℝ≥0∞)

Tactic:
simp only [one_pow, one_mul, ENNReal.ofReal_one] at A

Premises used: one_pow, ENNReal.ofReal_one, 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
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞))
    (𝓝[<] 1) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1)) : Filter ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)

Tactic:
le_of_tendsto A ?_

Premises used: le_of_tendsto
-- 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 :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞))
    (𝓝[<] 1) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1)) : Filter ℝ≥0∞)
refine :
  ∀ᶠ (c : ℝ) in 𝓝[<] 1,
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (c ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) ≤
      (μ : (a : Set E) → ℝ≥0∞) (ball 0 1)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)

Tactic:
refine le_of_tendsto A ?_

Premises used: le_of_tendsto
-- 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 :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞))
    (𝓝[<] 1) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1)) : Filter ℝ≥0∞)
h :
  ∀ (r : ℝ) (hr : Membership.mem (γ := Set ℝ) (Ioo 0 1) r),
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) ≤
      (μ : (a : Set E) → ℝ≥0∞) (ball 0 1)
⊢ ∀ᶠ (c : ℝ) in 𝓝[<] 1,
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (c ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) ≤
      (μ : (a : Set E) → ℝ≥0∞) (ball 0 1)

Tactic:
filter_upwards [Ioo_mem_nhdsLT zero_lt_one] with r hr

Premises used: Ioo_mem_nhdsLT, zero_lt_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
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞))
    (𝓝[<] 1) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1)) : Filter ℝ≥0∞)
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioo 0 1) r
h : LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) ≤
    (μ : (a : Set E) → ℝ≥0∞) (ball 0 1)

Tactic:
rw [← addHaar_closedBall' μ (0 : E) hr.1.le]

Premises used: LT.lt.le, And.left, OfNat.ofNat, MeasureTheory.Measure.addHaar_closedBall'
-- 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 :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞))
    (𝓝[<] 1) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1)) : Filter ℝ≥0∞)
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioo 0 1) r
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)

Tactic:
measure_mono (closedBall_subset_ball hr.2)

Premises used: Metric.closedBall_subset_ball, And.right, MeasureTheory.measure_mono