awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      (Set.preimage (β := WithLp 2 (ι → ℝ)) (WithLp.toLp 2) (Metric.ball 0 1)) =
    ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
have inr : ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
    {x : ι → ℝ | LT.lt (α := ℝ) (∑ x_1 : ι, HPow.hPow (β := ℕ) (x x_1) 2) 1} =
  ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
Tactic: simp only [Set.preimage, ball_zero_eq _ zero_le_one, one_pow, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | LT.lt (α := ℝ) (∑ x_1 : ι, HPow.hPow (β := ℕ) (x x_1) 2) 1} =
    ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
have h : ∀ (x : ι → ℝ),
  LT.lt (α := ℝ) (∑ x_1 : ι, HPow.hPow (β := ℕ) (x x_1) 2) 1 ↔ LT.lt (α := ℝ) (∑ i : ι, HPow.hPow (β := ℝ) |x i| 2) 1
Tactic: convert! volume_sum_rpow_lt_one ι one_le_two using 4
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
h :
  ∀ (x : ι → ℝ),
    LT.lt (α := ℝ) (∑ x_1 : ι, HPow.hPow (β := ℕ) (x x_1) 2) 1 ↔ LT.lt (α := ℝ) (∑ i : ι, HPow.hPow (β := ℝ) |x i| 2) 1
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | LT.lt (α := ℝ) (∑ x_1 : ι, HPow.hPow (β := ℕ) (x x_1) 2) 1} =
    ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
have h₁ : √π = 2 * Gamma (1 / 2 + 1)
Tactic: convert! volume_sum_rpow_lt_one ι one_le_two using 4
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
⊢ √π = 2 * Gamma (1 / 2 + 1)
have h : √π = 2 * (1 / 2 * Gamma (1 / 2))
Tactic: rw [Gamma_add_one (by simp), Gamma_one_half_eq, ← mul_assoc, mul_div_cancel₀ _
        two_ne_zero, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
h : √π = 2 * (1 / 2 * Gamma (1 / 2))
⊢ √π = 2 * Gamma (1 / 2 + 1)
have h₁ : √π = 2 * (1 / 2 * √π)
Tactic: rw [Gamma_add_one (by simp), Gamma_one_half_eq, ← mul_assoc, mul_div_cancel₀ _
        two_ne_zero, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
h : √π = 2 * (1 / 2 * Gamma (1 / 2))
h₁ : √π = 2 * (1 / 2 * √π)
⊢ √π = 2 * Gamma (1 / 2 + 1)
have h₂ : √π = 2 * (1 / 2) * √π
Tactic: rw [Gamma_add_one (by simp), Gamma_one_half_eq, ← mul_assoc, mul_div_cancel₀ _
        two_ne_zero, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
h : √π = 2 * (1 / 2 * Gamma (1 / 2))
h₁ : √π = 2 * (1 / 2 * √π)
h₂ : √π = 2 * (1 / 2) * √π
⊢ √π = 2 * Gamma (1 / 2 + 1)
have h₃ : √π = 1 * √π
Tactic: rw [Gamma_add_one (by simp), Gamma_one_half_eq, ← mul_assoc, mul_div_cancel₀ _
        two_ne_zero, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
h : √π = 2 * (1 / 2 * Gamma (1 / 2))
h₁ : √π = 2 * (1 / 2 * √π)
h₂ : √π = 2 * (1 / 2) * √π
h₃ : √π = 1 * √π
⊢ √π = 2 * Gamma (1 / 2 + 1)
have h₄ : √π = √π
Tactic: rw [Gamma_add_one (by simp), Gamma_one_half_eq, ← mul_assoc, mul_div_cancel₀ _
        two_ne_zero, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
⊢ ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.closedBall x r) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
have rw : ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball x r) =
  ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
Tactic: rw [addHaar_closedBall_eq_addHaar_ball, EuclideanSpace.volume_ball]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
rw :
  ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
⊢ ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.closedBall x r) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
have rw₁ : ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1)) =
  ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
Tactic: rw [addHaar_closedBall_eq_addHaar_ball, EuclideanSpace.volume_ball]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : Nontrivial E
x : E
r : ℝ
⊢ ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E *
      ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1))
have rw : (volume : (a : Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) → ℝ≥0∞)
    ((⇑(LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ E))) :
        (a : EuclideanSpace ℝ (Fin (finrank ℝ E))) → E) ⁻¹'
      ball x r) =
  ENNReal.ofReal r ^ finrank ℝ E *
    ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1))
Tactic: rw [← ((stdOrthonormalBasis ℝ E).measurePreserving_repr_symm).measure_preimage
      measurableSet_ball.nullMeasurableSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : Nontrivial E
x : E
r : ℝ
⊢ (volume : (a : Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) → ℝ≥0∞)
      ((⇑(LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ E))) :
          (a : EuclideanSpace ℝ (Fin (finrank ℝ E))) → E) ⁻¹'
        ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E *
      ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1))
have this : Nonempty (Fin (finrank ℝ E))
Tactic: have : Nonempty (Fin (finrank ℝ E)) := Fin.pos_iff_nonempty.mp finrank_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : Nontrivial E
x : E
r : ℝ
this : Nonempty (Fin (finrank ℝ E))
⊢ (volume : (a : Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) → ℝ≥0∞)
      ((⇑(LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ E))) :
          (a : EuclideanSpace ℝ (Fin (finrank ℝ E))) → E) ⁻¹'
        ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E *
      ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1))
have this₁ : (volume : (a : Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) → ℝ≥0∞)
    (ball
        (((OrthonormalBasis.repr (stdOrthonormalBasis ℝ E) : E ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
            (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
          x)
        r :
      Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) =
  ENNReal.ofReal r ^ Fintype.card (Fin (finrank ℝ E)) *
    ENNReal.ofReal
      (√π ^ Fintype.card (Fin (finrank ℝ E)) /
        Gamma (HDiv.hDiv (α := ℝ) (↑(Fintype.card (Fin (finrank ℝ E))) : ℝ) 2 + 1))
Tactic: have := EuclideanSpace.volume_ball (Fin (finrank ℝ E)) ((stdOrthonormalBasis ℝ E).repr x) r
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : Nontrivial E
x : E
r : ℝ
this_1 : Nonempty (Fin (finrank ℝ E))
this :
  (volume : (a : Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) → ℝ≥0∞)
      (ball
          (((OrthonormalBasis.repr (stdOrthonormalBasis ℝ E) : E ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x)
          r :
        Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) =
    ENNReal.ofReal r ^ Fintype.card (Fin (finrank ℝ E)) *
      ENNReal.ofReal
        (√π ^ Fintype.card (Fin (finrank ℝ E)) /
          Gamma (HDiv.hDiv (α := ℝ) (↑(Fintype.card (Fin (finrank ℝ E))) : ℝ) 2 + 1))
⊢ (volume : (a : Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) → ℝ≥0∞)
      ((⇑(LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ E))) :
          (a : EuclideanSpace ℝ (Fin (finrank ℝ E))) → E) ⁻¹'
        ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E *
      ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1))
have this₁ : (volume : (a : Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) → ℝ≥0∞)
    (ball
        (((OrthonormalBasis.repr (stdOrthonormalBasis ℝ E) : E ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
            (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
          x)
        r :
      Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) =
  ENNReal.ofReal r ^ finrank ℝ E *
    ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1))
Tactic: simp_rw [Fintype.card_fin] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : Nontrivial E
x : E
r : ℝ
this_1 : Nonempty (Fin (finrank ℝ E))
this :
  (volume : (a : Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) → ℝ≥0∞)
      (ball
          (((OrthonormalBasis.repr (stdOrthonormalBasis ℝ E) : E ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x)
          r :
        Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) =
    ENNReal.ofReal r ^ finrank ℝ E *
      ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1))
⊢ (volume : (a : Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) → ℝ≥0∞)
      ((⇑(LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ E))) :
          (a : EuclideanSpace ℝ (Fin (finrank ℝ E))) → E) ⁻¹'
        ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E *
      ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1))
have h : Eq (α := Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
  ((⇑(LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ E))) :
        (a : EuclideanSpace ℝ (Fin (finrank ℝ E))) → E) ⁻¹'
      ball x r :
    Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
  (ball
      (((OrthonormalBasis.repr (stdOrthonormalBasis ℝ E) : E ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
          (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
        x)
      r :
    Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
Tactic: convert! this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : Nontrivial E
x : E
r : ℝ
⊢ ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (closedBall x r) =
    ENNReal.ofReal r ^ finrank ℝ E *
      ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1))
have rw : ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (ball x r) =
  ENNReal.ofReal r ^ finrank ℝ E *
    ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1))
Tactic: rw [addHaar_closedBall_eq_addHaar_ball, InnerProductSpace.volume_ball _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : Nontrivial E
x : E
r : ℝ
rw :
  ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E *
      ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1))
⊢ ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (closedBall x r) =
    ENNReal.ofReal r ^ finrank ℝ E *
      ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1))
have rw₁ : ENNReal.ofReal r ^ finrank ℝ E *
    ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1)) =
  ENNReal.ofReal r ^ finrank ℝ E *
    ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (HDiv.hDiv (α := ℝ) (↑(finrank ℝ E) : ℝ) 2 + 1))
Tactic: rw [addHaar_closedBall_eq_addHaar_ball, InnerProductSpace.volume_ball _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : Nontrivial E
k : ℕ
hk : finrank ℝ E = 2 * k
x : E
r : ℝ
⊢ ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k / (↑k ! : ℝ))
have rw : HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 ^ k * ENNReal.ofReal (π ^ k / Gamma (HDiv.hDiv (α := ℝ) (↑(2 * k) : ℝ) 2 + 1)) =
  HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 ^ k * ENNReal.ofReal (π ^ k / (↑k ! : ℝ))
Tactic: rw [volume_ball, hk, pow_mul, pow_mul, sq_sqrt pi_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : Nontrivial E
k : ℕ
hk : finrank ℝ E = 2 * k
x : E
r : ℝ
⊢ HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 ^ k *
      ENNReal.ofReal (π ^ k / Gamma (HDiv.hDiv (α := ℝ) (↑(2 * k) : ℝ) 2 + 1)) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 ^ k * ENNReal.ofReal (π ^ k / (↑k ! : ℝ))
have e_a : Gamma (HDiv.hDiv (α := ℝ) (↑(2 * k) : ℝ) 2 + 1) = (↑k ! : ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : Nontrivial E
k : ℕ
hk : finrank ℝ E = 2 * k
x : E
r : ℝ
⊢ ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (closedBall x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k / (↑k ! : ℝ))
have rw : ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (ball x r) =
  ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k / (↑k ! : ℝ))
Tactic: rw [addHaar_closedBall_eq_addHaar_ball, volume_ball_of_dim_even hk x]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : Nontrivial E
k : ℕ
hk : finrank ℝ E = 2 * k
x : E
r : ℝ
rw :
  ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k / (↑k ! : ℝ))
⊢ ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (closedBall x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k / (↑k ! : ℝ))
have rw₁ : ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k / (↑k ! : ℝ)) =
  ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k / (↑k ! : ℝ))
Tactic: rw [addHaar_closedBall_eq_addHaar_ball, volume_ball_of_dim_even hk x]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
⊢ ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k * HPow.hPow (α := ℝ) 2 (k + 1) / (↑(finrank ℝ E)‼ : ℝ))
have this : Nontrivial E
Tactic: have : Nontrivial E := Module.nontrivial_of_finrank_pos (R := ℝ) (hk ▸ (2 * k).succ_pos)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
⊢ ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k * HPow.hPow (α := ℝ) 2 (k + 1) / (↑(finrank ℝ E)‼ : ℝ))
have rw : ENNReal.ofReal r ^ (2 * k + 1) * ENNReal.ofReal (π ^ k * (√π / Gamma (HDiv.hDiv (α := ℝ) (↑(2 * k + 1) : ℝ) 2 + 1))) =
  ENNReal.ofReal r ^ (2 * k + 1) * ENNReal.ofReal (π ^ k * (HPow.hPow (α := ℝ) 2 (k + 1) / (↑(2 * k + 1)‼ : ℝ)))
Tactic: rw [volume_ball, hk, pow_succ (√π), pow_mul, sq_sqrt pi_nonneg, mul_div_assoc, mul_div_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : 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 (HDiv.hDiv (α := ℝ) (↑(2 * k + 1) : ℝ) 2 + 1))) =
    ENNReal.ofReal r ^ (2 * k + 1) * ENNReal.ofReal (π ^ k * (HPow.hPow (α := ℝ) 2 (k + 1) / (↑(2 * k + 1)‼ : ℝ)))
have e_a : √π / Gamma (HDiv.hDiv (α := ℝ) (↑(2 * k + 1) : ℝ) 2 + 1) = HPow.hPow (α := ℝ) 2 (k + 1) / (↑(2 * k + 1)‼ : ℝ)
Tactic: congr 3
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
⊢ √π / Gamma (HDiv.hDiv (α := ℝ) (↑(2 * k + 1) : ℝ) 2 + 1) = HPow.hPow (α := ℝ) 2 (k + 1) / (↑(2 * k + 1)‼ : ℝ)
have e_a : √π / ((↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)) = HPow.hPow (α := ℝ) 2 (k + 1) / (↑(2 * k + 1)‼ : ℝ)
Tactic: suffices √π / (↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)) = 2 ^ (k + 1) / ↑(2 * k + 1)‼ by
    simpa [add_div, add_right_comm, -one_div, Gamma_nat_add_one_add_half]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
⊢ ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (closedBall x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k * HPow.hPow (α := ℝ) 2 (k + 1) / (↑(finrank ℝ E)‼ : ℝ))
have this : Nontrivial E
Tactic: have : Nontrivial E := Module.nontrivial_of_finrank_pos (R := ℝ) (hk ▸ (2 * k).succ_pos)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
⊢ ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (closedBall x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k * HPow.hPow (α := ℝ) 2 (k + 1) / (↑(finrank ℝ E)‼ : ℝ))
have rw : ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (ball x r) =
  ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k * HPow.hPow (α := ℝ) 2 (k + 1) / (↑(finrank ℝ E)‼ : ℝ))
Tactic: rw [addHaar_closedBall_eq_addHaar_ball, volume_ball_of_dim_odd hk x r]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
rw :
  ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (ball x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k * HPow.hPow (α := ℝ) 2 (k + 1) / (↑(finrank ℝ E)‼ : ℝ))
⊢ ((volume : Measure E) : (a : Set E) → ℝ≥0∞) (closedBall x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k * HPow.hPow (α := ℝ) 2 (k + 1) / (↑(finrank ℝ E)‼ : ℝ))
have rw₁ : ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k * HPow.hPow (α := ℝ) 2 (k + 1) / (↑(finrank ℝ E)‼ : ℝ)) =
  ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k * HPow.hPow (α := ℝ) 2 (k + 1) / (↑(finrank ℝ E)‼ : ℝ))
Tactic: rw [addHaar_closedBall_eq_addHaar_ball, volume_ball_of_dim_odd hk x r]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
x : EuclideanSpace ℝ (Fin 2)
r : ℝ
⊢ (volume : (a : Set (EuclideanSpace ℝ (Fin 2))) → ℝ≥0∞) (closedBall x r) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 * ENNReal.ofReal π
have rw : (volume : (a : Set (EuclideanSpace ℝ (Fin 2))) → ℝ≥0∞) (ball x r) =
  HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 * ENNReal.ofReal π
Tactic: rw [addHaar_closedBall_eq_addHaar_ball, volume_ball_fin_two x r]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
x : EuclideanSpace ℝ (Fin 2)
r : ℝ
rw :
  (volume : (a : Set (EuclideanSpace ℝ (Fin 2))) → ℝ≥0∞) (ball x r) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 * ENNReal.ofReal π
⊢ (volume : (a : Set (EuclideanSpace ℝ (Fin 2))) → ℝ≥0∞) (closedBall x r) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 * ENNReal.ofReal π
have rw₁ : HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 * ENNReal.ofReal π = HPow.hPow (β := ℕ) (ENNReal.ofReal r) 2 * ENNReal.ofReal π
Tactic: rw [addHaar_closedBall_eq_addHaar_ball, volume_ball_fin_two x r]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
x : EuclideanSpace ℝ (Fin 3)
r : ℝ
⊢ (volume : (a : Set (EuclideanSpace ℝ (Fin 3))) → ℝ≥0∞) (closedBall x r) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal r) 3 * ENNReal.ofReal (π * 4 / 3)
have rw : (volume : (a : Set (EuclideanSpace ℝ (Fin 3))) → ℝ≥0∞) (ball x r) =
  HPow.hPow (β := ℕ) (ENNReal.ofReal r) 3 * ENNReal.ofReal (π * 4 / 3)
Tactic: rw [addHaar_closedBall_eq_addHaar_ball, volume_ball_fin_three x]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
x : EuclideanSpace ℝ (Fin 3)
r : ℝ
rw :
  (volume : (a : Set (EuclideanSpace ℝ (Fin 3))) → ℝ≥0∞) (ball x r) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal r) 3 * ENNReal.ofReal (π * 4 / 3)
⊢ (volume : (a : Set (EuclideanSpace ℝ (Fin 3))) → ℝ≥0∞) (closedBall x r) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal r) 3 * ENNReal.ofReal (π * 4 / 3)
have rw₁ : HPow.hPow (β := ℕ) (ENNReal.ofReal r) 3 * ENNReal.ofReal (π * 4 / 3) =
  HPow.hPow (β := ℕ) (ENNReal.ofReal r) 3 * ENNReal.ofReal (π * 4 / 3)
Tactic: rw [addHaar_closedBall_eq_addHaar_ball, volume_ball_fin_three x]