awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
eq_norm :
  ∀ (x : ι → ℂ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) =
      HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : Norm.norm.{u_1} (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) 0) = 0
eq_zero : ∀ (x : ι → ℂ), Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) = 0 ↔ x = 0
nm_neg :
  ∀ (x : ι → ℂ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (-toLp (ENNReal.ofReal p) x) =
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x)
nm_add :
  ∀ (x y : ι → ℂ),
    ‖HAdd.hAdd (α := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) (toLp (ENNReal.ofReal p) y)‖ ≤
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) +
        Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) y)
nm_smul :
  ∀ (r : ℝ) (x : ι → ℂ),
    ‖HSMul.hSMul (β := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℂ) r (toLp (ENNReal.ofReal p) x)‖ ≤
      ‖r‖ * Norm.norm (E := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℂ) (toLp (ENNReal.ofReal p) x)
eq_zero₁ : ∀ (x : ι → ℂ), HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) = 0 ↔ x = 0
nm_zero₁ : HPow.hPow (α := ℝ) (∑ i : ι, Norm.norm (E := ℂ) (0 i) ^ p) (1 / p) = 0
⊢ ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞)
      {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) ≤ r} =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
have nm_neg₁ : ∀ (x : ι → ℂ), HPow.hPow (α := ℝ) (∑ i : ι, ‖(-x) i‖ ^ p) (1 / p) = HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
Tactic: simp_rw [← toLp_neg, ← toLp_add, ← toLp_smul, eq_norm] at eq_zero nm_zero nm_neg nm_add nm_smul
Cleared hypotheses: nm_zero, eq_zero, nm_neg, nm_add, nm_smul
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
eq_norm :
  ∀ (x : ι → ℂ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) =
      HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : Norm.norm.{u_1} (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) 0) = 0
eq_zero : ∀ (x : ι → ℂ), Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) = 0 ↔ x = 0
nm_neg :
  ∀ (x : ι → ℂ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (-toLp (ENNReal.ofReal p) x) =
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x)
nm_add :
  ∀ (x y : ι → ℂ),
    ‖HAdd.hAdd (α := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) (toLp (ENNReal.ofReal p) y)‖ ≤
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) +
        Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) y)
nm_smul :
  ∀ (r : ℝ) (x : ι → ℂ),
    ‖HSMul.hSMul (β := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℂ) r (toLp (ENNReal.ofReal p) x)‖ ≤
      ‖r‖ * Norm.norm (E := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℂ) (toLp (ENNReal.ofReal p) x)
eq_zero₁ : ∀ (x : ι → ℂ), HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) = 0 ↔ x = 0
nm_zero₁ : HPow.hPow (α := ℝ) (∑ i : ι, Norm.norm (E := ℂ) (0 i) ^ p) (1 / p) = 0
nm_neg₁ :
  ∀ (x : ι → ℂ), HPow.hPow (α := ℝ) (∑ i : ι, ‖(-x) i‖ ^ p) (1 / p) = HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
⊢ ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞)
      {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) ≤ r} =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
have nm_add₁ : ∀ (x y : ι → ℂ),
  HPow.hPow (α := ℝ) (∑ i : ι, ‖(x + y) i‖ ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ i : ι, ‖y i‖ ^ p) (1 / p)
Tactic: simp_rw [← toLp_neg, ← toLp_add, ← toLp_smul, eq_norm] at eq_zero nm_zero nm_neg nm_add nm_smul
Cleared hypotheses: nm_zero, eq_zero, nm_neg, nm_add, nm_smul
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
eq_norm :
  ∀ (x : ι → ℂ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) =
      HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : Norm.norm.{u_1} (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) 0) = 0
eq_zero : ∀ (x : ι → ℂ), Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) = 0 ↔ x = 0
nm_neg :
  ∀ (x : ι → ℂ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (-toLp (ENNReal.ofReal p) x) =
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x)
nm_add :
  ∀ (x y : ι → ℂ),
    ‖HAdd.hAdd (α := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) (toLp (ENNReal.ofReal p) y)‖ ≤
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) +
        Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) y)
nm_smul :
  ∀ (r : ℝ) (x : ι → ℂ),
    ‖HSMul.hSMul (β := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℂ) r (toLp (ENNReal.ofReal p) x)‖ ≤
      ‖r‖ * Norm.norm (E := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℂ) (toLp (ENNReal.ofReal p) x)
eq_zero₁ : ∀ (x : ι → ℂ), HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) = 0 ↔ x = 0
nm_zero₁ : HPow.hPow (α := ℝ) (∑ i : ι, Norm.norm (E := ℂ) (0 i) ^ p) (1 / p) = 0
nm_neg₁ :
  ∀ (x : ι → ℂ), HPow.hPow (α := ℝ) (∑ i : ι, ‖(-x) i‖ ^ p) (1 / p) = HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
nm_add₁ :
  ∀ (x y : ι → ℂ),
    HPow.hPow (α := ℝ) (∑ i : ι, ‖(x + y) i‖ ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ i : ι, ‖y i‖ ^ p) (1 / p)
⊢ ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞)
      {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) ≤ r} =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
have nm_smul₁ : ∀ (r : ℝ) (x : ι → ℂ),
  HPow.hPow (α := ℝ) (∑ i : ι, ‖(r • x) i‖ ^ p) (1 / p) ≤ ‖r‖ * HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
Tactic: simp_rw [← toLp_neg, ← toLp_add, ← toLp_smul, eq_norm] at eq_zero nm_zero nm_neg nm_add nm_smul
Cleared hypotheses: nm_zero, eq_zero, nm_neg, nm_add, nm_smul
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
eq_norm :
  ∀ (x : ι → ℂ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) =
      HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
eq_zero : ∀ (x : ι → ℂ), HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) = 0 ↔ x = 0
nm_zero : HPow.hPow (α := ℝ) (∑ i : ι, Norm.norm (E := ℂ) (0 i) ^ p) (1 / p) = 0
nm_neg :
  ∀ (x : ι → ℂ), HPow.hPow (α := ℝ) (∑ i : ι, ‖(-x) i‖ ^ p) (1 / p) = HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
nm_add :
  ∀ (x y : ι → ℂ),
    HPow.hPow (α := ℝ) (∑ i : ι, ‖(x + y) i‖ ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ i : ι, ‖y i‖ ^ p) (1 / p)
nm_smul :
  ∀ (r : ℝ) (x : ι → ℂ),
    HPow.hPow (α := ℝ) (∑ i : ι, ‖(r • x) i‖ ^ p) (1 / p) ≤ ‖r‖ * HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
⊢ ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞)
      {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) ≤ r} =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
have rw : ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞)
    {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} =
  ENNReal.ofReal r ^ (2 * card ι) *
    ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
Tactic: rw [measure_le_eq_lt _ nm_zero (fun x ↦ nm_neg x) (fun x y ↦ nm_add x y) (eq_zero _).mp
    (fun r x => nm_smul r x), Complex.volume_sum_rpow_lt _ hp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
eq_norm :
  ∀ (x : ι → ℂ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) =
      HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
eq_zero : ∀ (x : ι → ℂ), HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) = 0 ↔ x = 0
nm_zero : HPow.hPow (α := ℝ) (∑ i : ι, Norm.norm (E := ℂ) (0 i) ^ p) (1 / p) = 0
nm_neg :
  ∀ (x : ι → ℂ), HPow.hPow (α := ℝ) (∑ i : ι, ‖(-x) i‖ ^ p) (1 / p) = HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
nm_add :
  ∀ (x y : ι → ℂ),
    HPow.hPow (α := ℝ) (∑ i : ι, ‖(x + y) i‖ ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ i : ι, ‖y i‖ ^ p) (1 / p)
nm_smul :
  ∀ (r : ℝ) (x : ι → ℂ),
    HPow.hPow (α := ℝ) (∑ i : ι, ‖(r • x) i‖ ^ p) (1 / p) ≤ ‖r‖ * HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
rw :
  ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞)
      {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
⊢ ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞)
      {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) ≤ r} =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
have rw₁ : ENNReal.ofReal r ^ (2 * card ι) *
    ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1)) =
  ENNReal.ofReal r ^ (2 * card ι) *
    ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
Tactic: rw [measure_le_eq_lt _ nm_zero (fun x ↦ nm_neg x) (fun x y ↦ nm_add x y) (eq_zero _).mp
    (fun r x => nm_smul r x), Complex.volume_sum_rpow_lt _ hp]
-- 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.ball x r) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
have inl : ∀ (hr : r ≤ 0),
  ((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: obtain hr | hr := le_total r 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
inl :
  ∀ (hr : r ≤ 0),
    ((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.ball x r) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
have inr : ∀ (hr : 0 ≤ r),
  ((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: obtain hr | hr := le_total r 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : r ≤ 0
⊢ ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
have inl : ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) ∅ =
  ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : r ≤ 0
inl :
  ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) ∅ =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
⊢ ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
have inl₁ : 0 = ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : r ≤ 0
inl :
  ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) ∅ =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
inl₁ : 0 = ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
⊢ ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
have inl₂ : 0 = HPow.hPow (α := ℝ≥0∞) 0 (card ι) * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : r ≤ 0
inl :
  ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) ∅ =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
inl₁ : 0 = ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
inl₂ :
  0 = HPow.hPow (α := ℝ≥0∞) 0 (card ι) * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
⊢ ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
have inl₃ : 0 = 0 * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Nonempty ι
inst_1 : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : r ≤ 0
inl :
  ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) ∅ =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
inl₁ : 0 = ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
inl₂ :
  0 = HPow.hPow (α := ℝ≥0∞) 0 (card ι) * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
inl₃ : 0 = 0 * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
⊢ ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
have inl₄ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [Metric.ball_eq_empty.mpr hr, measure_empty, ← zero_eq_ofReal.mpr hr, zero_pow card_ne_zero,
      zero_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
this :
  ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
⊢ ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
have rw : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ Module.finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι)))
    (((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball 0 1) : ℝ≥0∞) =
  ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
Tactic: rw [Measure.addHaar_ball _ _ hr, this, ofReal_pow hr, finrank_euclideanSpace]
-- 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
this :
  ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
rw :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ Module.finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι)))
      (((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball 0 1) : ℝ≥0∞) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
⊢ ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
have rw₁ : ENNReal.ofReal (r ^ Module.finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι)) *
    ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1)) =
  ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
Tactic: rw [Measure.addHaar_ball _ _ hr, this, ofReal_pow hr, finrank_euclideanSpace]
-- 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
this :
  ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
rw :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ Module.finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι)))
      (((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball 0 1) : ℝ≥0∞) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
rw₁ :
  ENNReal.ofReal (r ^ Module.finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι)) *
      ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1)) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
⊢ ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
have rw₂ : ENNReal.ofReal r ^ Module.finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι) *
    ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1)) =
  ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
Tactic: rw [Measure.addHaar_ball _ _ hr, this, ofReal_pow hr, finrank_euclideanSpace]
-- 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
this :
  ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
rw :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ Module.finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι)))
      (((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball 0 1) : ℝ≥0∞) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
rw₁ :
  ENNReal.ofReal (r ^ Module.finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι)) *
      ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1)) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
rw₂ :
  ENNReal.ofReal r ^ Module.finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι) *
      ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1)) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
⊢ ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball 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 [Measure.addHaar_ball _ _ hr, this, ofReal_pow hr, finrank_euclideanSpace]
-- 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 (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball x r) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
have inr : ((volume : Measure (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball 0 1) =
  ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
Tactic: suffices volume (Metric.ball (0 : EuclideanSpace ℝ ι) 1) =
        .ofReal (√π ^ card ι / Gamma (card ι / 2 + 1)) by
      rw [Measure.addHaar_ball _ _ hr, this, ofReal_pow hr, finrank_euclideanSpace]
-- 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 (EuclideanSpace ℝ ι)) : (a : Set (EuclideanSpace ℝ ι)) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal (√π ^ card ι / Gamma (HDiv.hDiv (α := ℝ) (↑(card ι) : ℝ) 2 + 1))
have inr : ((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))
Tactic: rw [← (PiLp.volume_preserving_toLp ι).measure_preimage
      measurableSet_ball.nullMeasurableSet]