-- Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
theorem volume_ball (x : EuclideanSpace ℝ ι) (r : ℝ) :
    volume (Metric.ball x r) = (.ofReal r) ^ card ι *
      .ofReal (Real.sqrt π ^ card ι / Gamma (card ι / 2 + 1))

Proof state:
case h.e'_3.h.e'_1.h.e'_5.h.e'_5
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
⊢ √π = 2 * Gamma (1 / 2 + 1)

Tactic:
rw [Gamma_add_one (by norm_num), Gamma_one_half_eq, ← mul_assoc, mul_div_cancel₀ _
  two_ne_zero, one_mul]

Result:
no goals

Proof state:
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
⊢ volume (Metric.ball x r) = ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))

Tactic:
obtain hr | hr := le_total r 0

Result:
case inl
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : r ≤ 0
⊢ volume (Metric.ball x r) = ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))

case inr
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
⊢ volume (Metric.ball x r) = ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))

Proof state:
case inr
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
⊢ volume (Metric.ball 0 1) = ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))

Tactic:
rw [← ((volume_preserving_measurableEquiv _).symm).measure_preimage
  measurableSet_ball.nullMeasurableSet]

Result:
case inr
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
⊢ volume (⇑(EuclideanSpace.measurableEquiv ι).symm ⁻¹' Metric.ball 0 1) =
    ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))

Proof state:
case h.e'_2.h.e'_6.h.e'_1.h.a
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
x✝ : EuclideanSpace ℝ ι
⊢ Metric.ball 0 1 x✝ ↔ ∑ i : ι, |x✝ i| ^ 2 < 1

Tactic:
simp_rw [ball_zero_eq _ zero_le_one, one_pow, Real.rpow_two, sq_abs,
  Set.setOf_app_iff]

Result:
no goals

Proof state:
case inl
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : r ≤ 0
⊢ volume (Metric.ball x r) = ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))

Tactic:
rw [Metric.ball_eq_empty.mpr hr, measure_empty, ← zero_eq_ofReal.mpr hr, zero_pow card_ne_zero,
  zero_mul]

Result:
no goals

Proof state:
case inr
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
⊢ volume (Metric.ball x r) = ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))

Tactic:
suffices volume (Metric.ball (0 : EuclideanSpace ℝ ι) 1) =
    .ofReal (Real.sqrt π ^ card ι / Gamma (card ι / 2 + 1)) by
  rw [Measure.addHaar_ball _ _ hr, this, ofReal_pow hr, finrank_euclideanSpace]

Result:
case inr
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
⊢ volume (Metric.ball 0 1) = ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))

Proof state:
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
this : volume (Metric.ball 0 1) = ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))
⊢ volume (Metric.ball x r) = ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))

Tactic:
rw [Measure.addHaar_ball _ _ hr, this, ofReal_pow hr, finrank_euclideanSpace]

Result:
no goals

Proof state:
case inr
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
⊢ volume (⇑(EuclideanSpace.measurableEquiv ι).symm ⁻¹' Metric.ball 0 1) =
    ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))

Tactic:
convert (volume_sum_rpow_lt_one ι one_le_two) using 4

Result:
case h.e'_2.h.e'_6.h.e'_1.h.a
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
x✝ : EuclideanSpace ℝ ι
⊢ Metric.ball 0 1 x✝ ↔ ∑ i : ι, |x✝ i| ^ 2 < 1

case h.e'_3.h.e'_1.h.e'_5.h.e'_5
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
⊢ √π = 2 * Gamma (1 / 2 + 1)

Proof state:
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
⊢ 1 / 2 ≠ 0

Tactic:
norm_num

Result:
no goals