awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
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
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
have inl : (μ : (a : Set E) → ℝ≥0∞) {0} =
  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})]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
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))
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
have inl₁ : (μ : (a : Set E) → ℝ≥0∞) {0} =
  ENNReal.ofReal ((∫ (x : E) in Set.univ, 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})]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
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))
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
have inl₂ : (μ : (a : Set E) → ℝ≥0∞) {0} =
  ENNReal.ofReal ((∫ (x : E) in {0}, 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})]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
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))
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
have 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))
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})]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
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))
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
have inl₄ : (μ : (a : Set E) → ℝ≥0∞) {0} =
  ENNReal.ofReal (μ.real {0} • Real.exp (-norm.{u_1} (E := E) 0 ^ p) / Real.Gamma ((↑0 : ℝ) / 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})]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
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))
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
have inl₅ : (μ : (a : Set E) → ℝ≥0∞) {0} =
  ENNReal.ofReal (μ.real {0} • Real.exp (-norm.{u_1} (E := E) 0 ^ p) / Real.Gamma (0 / 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})]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
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))
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
have 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))
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})]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
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))
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
have inl₇ : (μ : (a : Set E) → ℝ≥0∞) {0} = ENNReal.ofReal (μ.real {0} • Real.exp (-norm.{u_1} (E := E) 0 ^ p) / Real.Gamma 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})]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
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)
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
have inl₈ : (μ : (a : Set E) → ℝ≥0∞) {0} = ENNReal.ofReal (μ.real {0} • Real.exp (-norm.{u_1} (E := E) 0 ^ 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})]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
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)
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
have inl₉ : (μ : (a : Set E) → ℝ≥0∞) {0} = ENNReal.ofReal (μ.real {0} • Real.exp (-norm.{u_1} (E := E) 0 ^ p))
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})]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
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))
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
have inl₁₀ : (μ : (a : Set E) → ℝ≥0∞) {0} = ENNReal.ofReal (μ.real {0} • Real.exp (-HPow.hPow (α := ℝ) 0 p))
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})]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
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))
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
have inl₁₁ : (μ : (a : Set E) → ℝ≥0∞) {0} = ENNReal.ofReal (μ.real {0} • Real.exp (-0))
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})]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
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))
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
have inl₁₂ : (μ : (a : Set E) → ℝ≥0∞) {0} = ENNReal.ofReal (μ.real {0} • Real.exp 0)
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})]