-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
E : Type u_1
p : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hp : 0 < p
hE : Subsingleton E
inl :
  (μ : (a : Set E) → ℝ≥0∞) {0} =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
inl₁ :
  (μ : (a : Set E) → ℝ≥0∞) {0} =
    ENNReal.ofReal ((∫ (x : E) in Set.univ, Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
inl₂ :
  (μ : (a : Set E) → ℝ≥0∞) {0} =
    ENNReal.ofReal ((∫ (x : E) in {0}, Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
inl₃ :
  (μ : (a : Set E) → ℝ≥0∞) {0} =
    ENNReal.ofReal (μ.real {0} • Real.exp (-norm.{u_1} (E := E) 0 ^ p) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
inl₄ :
  (μ : (a : Set E) → ℝ≥0∞) {0} =
    ENNReal.ofReal (μ.real {0} • Real.exp (-norm.{u_1} (E := E) 0 ^ p) / Real.Gamma ((↑0 : ℝ) / p + 1))
inl₅ :
  (μ : (a : Set E) → ℝ≥0∞) {0} =
    ENNReal.ofReal (μ.real {0} • Real.exp (-norm.{u_1} (E := E) 0 ^ p) / Real.Gamma (0 / p + 1))
inl₆ :
  (μ : (a : Set E) → ℝ≥0∞) {0} =
    ENNReal.ofReal (μ.real {0} • Real.exp (-norm.{u_1} (E := E) 0 ^ p) / Real.Gamma (HAdd.hAdd (α := ℝ) 0 1))
inl₇ : (μ : (a : Set E) → ℝ≥0∞) {0} = ENNReal.ofReal (μ.real {0} • Real.exp (-norm.{u_1} (E := E) 0 ^ p) / Real.Gamma 1)
inl₈ : (μ : (a : Set E) → ℝ≥0∞) {0} = ENNReal.ofReal (μ.real {0} • Real.exp (-norm.{u_1} (E := E) 0 ^ p) / 1)
inl₉ : (μ : (a : Set E) → ℝ≥0∞) {0} = ENNReal.ofReal (μ.real {0} • Real.exp (-norm.{u_1} (E := E) 0 ^ p))
inl₁₀ : (μ : (a : Set E) → ℝ≥0∞) {0} = ENNReal.ofReal (μ.real {0} • Real.exp (-HPow.hPow (α := ℝ) 0 p))
inl₁₁ : (μ : (a : Set E) → ℝ≥0∞) {0} = ENNReal.ofReal (μ.real {0} • Real.exp (-0))
inl₁₂ : (μ : (a : Set E) → ℝ≥0∞) {0} = ENNReal.ofReal (μ.real {0} • Real.exp 0)
inl₁₃ : (μ : (a : Set E) → ℝ≥0∞) {0} = ENNReal.ofReal (HSMul.hSMul (β := ℝ) (μ.real {0}) 1)
inl₁₄ : (μ : (a : Set E) → ℝ≥0∞) {0} = ENNReal.ofReal (μ.real {0} * 1)
inl₁₅ : (μ : (a : Set E) → ℝ≥0∞) {0} = ENNReal.ofReal (μ.real {0})
inl₁₆ : (μ : (a : Set E) → ℝ≥0∞) {0} = ENNReal.ofReal (ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) {0}))
inl₁₇ inl₁₈ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {0} : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {0} : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))

Tactic:
rw [(Metric.nonempty_ball.mpr zero_lt_one).eq_zero, ← setIntegral_univ,
      Set.univ_nonempty.eq_zero, integral_singleton, finrank_zero_of_subsingleton, Nat.cast_zero,
      zero_div, zero_add, Real.Gamma_one, div_one, norm_zero, Real.zero_rpow hp.ne', neg_zero,
      Real.exp_zero, smul_eq_mul, mul_one, measureReal_def, ofReal_toReal (measure_ne_top μ {0})]

Premises used: Iff.mpr, Set.Nonempty.eq_zero, Real.Gamma_one, norm_zero, zero_div, MeasureTheory.measure_ne_top, Set.univ_nonempty, ENNReal.ofReal_toReal, Metric.nonempty_ball, zero_add, Real.zero_rpow, LT.lt.ne', zero_lt_one, MeasureTheory.measureReal_def, Real.exp_zero, MeasureTheory.integral_singleton, Nat.cast_zero, smul_eq_mul, mul_one, Singleton.singleton, OfNat.ofNat, neg_zero, div_one, MeasureTheory.setIntegral_univ, Module.finrank_zero_of_subsingleton