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
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)
⊢ (μ : (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 (HSMul.hSMul (β := ℝ) (μ.real {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))
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)
⊢ (μ : (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} * 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)
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)
⊢ (μ : (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})
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))
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})
⊢ (μ : (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 (ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) {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))
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}))
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
have inl₁₇ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {0} : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {0} : ℝ≥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 (hypothesis)
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 : Nontrivial E
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
have this : LT.lt (α := ℝ) 0 (↑(finrank ℝ E) : ℝ)
Tactic: have : (0 : ℝ) < finrank ℝ E := Nat.cast_pos.mpr finrank_pos
-- 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 : Nontrivial E
this : LT.lt (α := ℝ) 0 (↑(finrank ℝ E) : ℝ)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (restrict volume (Set.Ioi 0)) fun (y : ℝ) ↦
          y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) /
        Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1) *
      (↑(finrank ℝ E) : ℝ) =
    1
have simp_rw : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (restrict volume (Set.Ioi 0)) fun (y : ℝ) ↦
        y ^ HSub.hSub (α := ℝ) (↑(finrank ℝ E) : ℝ) 1 * Real.exp (-y ^ p)) /
      Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1) *
    (↑(finrank ℝ E) : ℝ) =
  1
Tactic: simp_rw [← Real.rpow_natCast _ (finrank ℝ E - 1), smul_eq_mul, Nat.cast_sub finrank_pos,
        Nat.cast_one]
-- 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 : Nontrivial E
this : LT.lt (α := ℝ) 0 (↑(finrank ℝ E) : ℝ)
⊢ -1 < HSub.hSub (α := ℝ) (↑(finrank ℝ E) : ℝ) 1
have linarith : HSub.hSub (α := ℝ) (↑(finrank ℝ E) : ℝ) 1 ≤ -1 →
  HSub.hSub (α := ℝ) 0 (↑(finrank ℝ E) : ℝ) + (HSub.hSub (α := ℝ) (↑(finrank ℝ E) : ℝ) 1 - -1) = 0
Tactic: linarith
-- 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 : Nontrivial E
this : LT.lt (α := ℝ) 0 (↑(finrank ℝ E) : ℝ)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (restrict volume (Set.Ioi 0)) fun (y : ℝ) ↦
          y ^ HSub.hSub (α := ℝ) (↑(finrank ℝ E) : ℝ) 1 * Real.exp (-y ^ p)) /
        Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1) *
      (↑(finrank ℝ E) : ℝ) =
    1
have rw : 1 / p * Real.Gamma ((↑(finrank ℝ E) : ℝ) / p) / ((↑(finrank ℝ E) : ℝ) / p * Real.Gamma ((↑(finrank ℝ E) : ℝ) / p)) *
    (↑(finrank ℝ E) : ℝ) =
  1
Tactic: rw [integral_rpow_mul_exp_neg_rpow hp (by linarith), sub_add_cancel,
        Real.Gamma_add_one (ne_of_gt (by positivity))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (hypothesis)
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 : Nontrivial E
this : LT.lt (α := ℝ) 0 (↑(finrank ℝ E) : ℝ)
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
have this₁ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (restrict volume (Set.Ioi 0)) fun (y : ℝ) ↦
        y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) /
      Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1) *
    (↑(finrank ℝ E) : ℝ) =
  1
Tactic: have : ((∫ y in Set.Ioi (0 : ℝ), y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) /
        Real.Gamma ((finrank ℝ E) / p + 1)) * (finrank ℝ E) = 1 := by
      simp_rw [← Real.rpow_natCast _ (finrank ℝ E - 1), smul_eq_mul, Nat.cast_sub finrank_pos,
        Nat.cast_one]
      rw [integral_rpow_mul_exp_neg_rpow hp (by linarith), sub_add_cancel,
        Real.Gamma_add_one (ne_of_gt (by positivity))]
      field
-- 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 : Nontrivial E
this_1 : LT.lt (α := ℝ) 0 (↑(finrank ℝ E) : ℝ)
this :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (restrict volume (Set.Ioi 0)) fun (y : ℝ) ↦
          y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) /
        Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1) *
      (↑(finrank ℝ E) : ℝ) =
    1
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
have rw : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [integral_fun_norm_addHaar μ (fun x => Real.exp (-x ^ p)), nsmul_eq_mul, smul_eq_mul,
      mul_div_assoc, mul_div_assoc, mul_comm, mul_assoc, this, mul_one, ofReal_measureReal _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (hypothesis)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
p_1 : ℝ
hp : 0 < p_1
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this : MeasurableSpace F := borel F
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | g x < 1} =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p_1) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p_1 + 1))
have this₁ : BorelSpace F
Tactic: have : BorelSpace F := { measurable_eq := rfl }
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
p_1 : ℝ
hp : 0 < p_1
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | g x < 1} =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p_1) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p_1 + 1))
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x < 1} : ℝ≥0∞) ((ν : (a : Set F) → ℝ≥0∞) (Metric.ball 0 1) : ℝ≥0∞)
Tactic: convert! (measure_unitBall_eq_integral_div_gamma ν hp) using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
p_1 : ℝ
hp : 0 < p_1
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x < 1} : ℝ≥0∞) ((ν : (a : Set F) → ℝ≥0∞) (Metric.ball 0 1) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | g x < 1} =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p_1) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p_1 + 1))
have h₁ : ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p_1) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p_1 + 1)) =
  ENNReal.ofReal ((∫ (x : F), Real.exp (-‖x‖ ^ p_1) ∂ν) / Real.Gamma ((↑(finrank ℝ F) : ℝ) / p_1 + 1))
Tactic: convert! (measure_unitBall_eq_integral_div_gamma ν hp) using 1