-- Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
lemma volume_ball_of_dim_odd {k : ℕ} (hk : finrank ℝ E = 2 * k + 1) (x : E) (r : ℝ) :
    volume (ball x r) =
      .ofReal r ^ finrank ℝ E * .ofReal (π ^ k * 2 ^ (k + 1) / (finrank ℝ E : ℕ)‼)

Proof state:
case e_a.e_r.e_a
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
⊢ √π / Gamma (↑(2 * k + 1) / 2 + 1) = 2 ^ (k + 1) / ↑(2 * k + 1)‼

Tactic:
simp? [add_div, add_right_comm, -one_div, Gamma_nat_add_one_add_half] says
  simp only [Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat, Nat.cast_one, add_div, ne_eq,
    OfNat.ofNat_ne_zero, not_false_eq_true, mul_div_cancel_left₀, add_right_comm,
    Gamma_nat_add_one_add_half]

Result:
case e_a.e_r.e_a
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
⊢ √π / (↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)) = 2 ^ (k + 1) / ↑(2 * k + 1)‼

Proof state:
case e_a.e_r.e_a
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
⊢ √π * 2 ^ (k + 1) * ↑(2 * k + 1)‼ = 2 ^ (k + 1) * (↑(2 * k + 1)‼ * √π)

Tactic:
ring

Result:
no goals

Proof state:
case e_a.e_r.e_a
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
⊢ √π / Gamma (↑(2 * k + 1) / 2 + 1) = 2 ^ (k + 1) / ↑(2 * k + 1)‼

Tactic:
simp only [Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat, Nat.cast_one, add_div, ne_eq,
  OfNat.ofNat_ne_zero, not_false_eq_true, mul_div_cancel_left₀, add_right_comm,
  Gamma_nat_add_one_add_half]

Result:
case e_a.e_r.e_a
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
⊢ √π / (↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)) = 2 ^ (k + 1) / ↑(2 * k + 1)‼

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
⊢ volume (ball x r) = ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k * 2 ^ (k + 1) / ↑(finrank ℝ E)‼)

Tactic:
rw [volume_ball, hk, pow_succ (√π), pow_mul, sq_sqrt pi_nonneg, mul_div_assoc, mul_div_assoc]

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
⊢ ENNReal.ofReal r ^ (2 * k + 1) * ENNReal.ofReal (π ^ k * (√π / Gamma (↑(2 * k + 1) / 2 + 1))) =
    ENNReal.ofReal r ^ (2 * k + 1) * ENNReal.ofReal (π ^ k * (2 ^ (k + 1) / ↑(2 * k + 1)‼))

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
⊢ ENNReal.ofReal r ^ (2 * k + 1) * ENNReal.ofReal (π ^ k * (√π / Gamma (↑(2 * k + 1) / 2 + 1))) =
    ENNReal.ofReal r ^ (2 * k + 1) * ENNReal.ofReal (π ^ k * (2 ^ (k + 1) / ↑(2 * k + 1)‼))

Tactic:
congr 3

Result:
case e_a.e_r.e_a
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
⊢ √π / Gamma (↑(2 * k + 1) / 2 + 1) = 2 ^ (k + 1) / ↑(2 * k + 1)‼

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
⊢ volume (ball x r) = ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k * 2 ^ (k + 1) / ↑(finrank ℝ E)‼)

Tactic:
have : Nontrivial E := Module.nontrivial_of_finrank_pos (R := ℝ) (hk ▸ (2 * k).succ_pos)

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
⊢ volume (ball x r) = ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k * 2 ^ (k + 1) / ↑(finrank ℝ E)‼)

Proof state:
case e_a.e_r.e_a
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
⊢ √π / (↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)) = 2 ^ (k + 1) / ↑(2 * k + 1)‼

Tactic:
field_simp

Result:
case e_a.e_r.e_a
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
⊢ √π * 2 ^ (k + 1) * ↑(2 * k + 1)‼ = 2 ^ (k + 1) * (↑(2 * k + 1)‼ * √π)