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

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ volume (⇑(stdOrthonormalBasis ℝ E).repr.symm ⁻¹' ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (↑(finrank ℝ E) / 2 + 1))

Tactic:
have : Nonempty (Fin (finrank ℝ E)) := Fin.pos_iff_nonempty.mp finrank_pos

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nontrivial E
x : E
r : ℝ
this : Nonempty (Fin (finrank ℝ E))
⊢ volume (⇑(stdOrthonormalBasis ℝ E).repr.symm ⁻¹' ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (↑(finrank ℝ E) / 2 + 1))

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nontrivial E
x : E
r : ℝ
this✝ : Nonempty (Fin (finrank ℝ E))
this :
  volume (ball ((stdOrthonormalBasis ℝ E).repr x) r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (↑(finrank ℝ E) / 2 + 1))
⊢ volume (⇑(stdOrthonormalBasis ℝ E).repr.symm ⁻¹' ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (↑(finrank ℝ E) / 2 + 1))

Tactic:
convert this

Result:
case h.e'_2.h.e'_6
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nontrivial E
x : E
r : ℝ
this✝ : Nonempty (Fin (finrank ℝ E))
this :
  volume (ball ((stdOrthonormalBasis ℝ E).repr x) r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (↑(finrank ℝ E) / 2 + 1))
⊢ ⇑(stdOrthonormalBasis ℝ E).repr.symm ⁻¹' ball x r = ball ((stdOrthonormalBasis ℝ E).repr x) r

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nontrivial E
x : E
r : ℝ
this : Nonempty (Fin (finrank ℝ E))
⊢ volume (⇑(stdOrthonormalBasis ℝ E).repr.symm ⁻¹' ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (↑(finrank ℝ E) / 2 + 1))

Tactic:
have := EuclideanSpace.volume_ball (Fin (finrank ℝ E)) ((stdOrthonormalBasis ℝ E).repr x) r

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nontrivial E
x : E
r : ℝ
this✝ : Nonempty (Fin (finrank ℝ E))
this :
  volume (ball ((stdOrthonormalBasis ℝ E).repr x) r) =
    ENNReal.ofReal r ^ Fintype.card (Fin (finrank ℝ E)) *
      ENNReal.ofReal (√π ^ Fintype.card (Fin (finrank ℝ E)) / Gamma (↑(Fintype.card (Fin (finrank ℝ E))) / 2 + 1))
⊢ volume (⇑(stdOrthonormalBasis ℝ E).repr.symm ⁻¹' ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (↑(finrank ℝ E) / 2 + 1))

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

Tactic:
rw [← ((stdOrthonormalBasis ℝ E).measurePreserving_repr_symm).measure_preimage
    measurableSet_ball.nullMeasurableSet]

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ volume (⇑(stdOrthonormalBasis ℝ E).repr.symm ⁻¹' ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (↑(finrank ℝ E) / 2 + 1))

Proof state:
case h.e'_2.h.e'_6
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nontrivial E
x : E
r : ℝ
this✝ : Nonempty (Fin (finrank ℝ E))
this :
  volume (ball ((stdOrthonormalBasis ℝ E).repr x) r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (↑(finrank ℝ E) / 2 + 1))
⊢ ⇑(stdOrthonormalBasis ℝ E).repr.symm ⁻¹' ball x r = ball ((stdOrthonormalBasis ℝ E).repr x) r

Tactic:
simp only [LinearIsometryEquiv.preimage_ball, LinearIsometryEquiv.symm_symm, _root_.map_zero]

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nontrivial E
x : E
r : ℝ
this✝ : Nonempty (Fin (finrank ℝ E))
this :
  volume (ball ((stdOrthonormalBasis ℝ E).repr x) r) =
    ENNReal.ofReal r ^ Fintype.card (Fin (finrank ℝ E)) *
      ENNReal.ofReal (√π ^ Fintype.card (Fin (finrank ℝ E)) / Gamma (↑(Fintype.card (Fin (finrank ℝ E))) / 2 + 1))
⊢ volume (⇑(stdOrthonormalBasis ℝ E).repr.symm ⁻¹' ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (↑(finrank ℝ E) / 2 + 1))

Tactic:
simp_rw [Fintype.card_fin] at this

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nontrivial E
x : E
r : ℝ
this✝ : Nonempty (Fin (finrank ℝ E))
this :
  volume (ball ((stdOrthonormalBasis ℝ E).repr x) r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (↑(finrank ℝ E) / 2 + 1))
⊢ volume (⇑(stdOrthonormalBasis ℝ E).repr.symm ⁻¹' ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (↑(finrank ℝ E) / 2 + 1))