awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ : ∀ (x : ι → ℂ), LE.le (α := ℝ) 0 (∑ i : ι, ‖x i‖ ^ p)
h₂ : ∀ (x : ι → ℂ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
hr : 0 < r
h :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    (Set.preimage (β := ι → ℂ) (fun (x : ι → ℂ) ↦ r⁻¹ • x) {x : ι → ℂ | LT.lt (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) 1})
h₃ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | LT.lt (α := ℝ) (∑ i : ι, ‖(r⁻¹ • a) i‖ ^ p) 1}
h₄ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | LT.lt (α := ℝ) (∑ x : ι, ‖r⁻¹ • a x‖ ^ p) 1}
h₅ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | LT.lt (α := ℝ) (∑ x : ι, (‖r⁻¹‖ * ‖a x‖) ^ p) 1}
h₆ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | LT.lt (α := ℝ) (∑ x : ι, ‖r⁻¹‖ ^ p * ‖a x‖ ^ p) 1}
h₇ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹| ^ p * ‖a x‖ ^ p) 1}
h₈ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | LT.lt (α := ℝ) (∑ x : ι, |r|⁻¹ ^ p * ‖a x‖ ^ p) 1}
h₉ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | LT.lt (α := ℝ) (∑ x : ι, (|r| ^ p)⁻¹ * ‖a x‖ ^ p) 1}
h₁₀ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | (|r| ^ p)⁻¹ * ∑ i : ι, ‖a i‖ ^ p < 1}
h₁₁ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | (r ^ p)⁻¹ * ∑ i : ι, ‖a i‖ ^ p < 1}
h₁₂ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | ∑ i : ι, ‖a i‖ ^ p < r ^ p * 1}
⊢ {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} =
    HSMul.hSMul (β := Set (ι → ℂ)) r {x : ι → ℂ | LT.lt (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) 1}
have h₁₃ : Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
  {a : ι → ℂ | ∑ i : ι, ‖a i‖ ^ p < r ^ p}
Tactic: simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hr), Set.preimage_setOf_eq, Pi.smul_apply,
        norm_smul, mul_rpow (norm_nonneg _) (norm_nonneg _), Real.norm_eq_abs, abs_inv, inv_rpow
        (abs_nonneg _), ← Finset.mul_sum, abs_eq_self.mpr (le_of_lt hr), inv_mul_lt_iff₀
        (rpow_pos_of_pos hr _), mul_one, ← rpow_lt_rpow_iff (rpow_nonneg (h₁ _) _)
        (le_of_lt hr) (by linarith : 0 < p), ← rpow_mul (h₁ _), div_mul_cancel₀ _
        (ne_of_gt (by linarith) : p ≠ 0), Real.rpow_one]
-- 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₁ : ∀ (x : ι → ℂ), LE.le (α := ℝ) 0 (∑ i : ι, ‖x i‖ ^ p)
h₂ : ∀ (x : ι → ℂ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
hr : 0 < r
h :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    (Set.preimage (β := ι → ℂ) (fun (x : ι → ℂ) ↦ r⁻¹ • x) {x : ι → ℂ | LT.lt (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) 1})
h₃ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | LT.lt (α := ℝ) (∑ i : ι, ‖(r⁻¹ • a) i‖ ^ p) 1}
h₄ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | LT.lt (α := ℝ) (∑ x : ι, ‖r⁻¹ • a x‖ ^ p) 1}
h₅ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | LT.lt (α := ℝ) (∑ x : ι, (‖r⁻¹‖ * ‖a x‖) ^ p) 1}
h₆ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | LT.lt (α := ℝ) (∑ x : ι, ‖r⁻¹‖ ^ p * ‖a x‖ ^ p) 1}
h₇ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹| ^ p * ‖a x‖ ^ p) 1}
h₈ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | LT.lt (α := ℝ) (∑ x : ι, |r|⁻¹ ^ p * ‖a x‖ ^ p) 1}
h₉ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | LT.lt (α := ℝ) (∑ x : ι, (|r| ^ p)⁻¹ * ‖a x‖ ^ p) 1}
h₁₀ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | (|r| ^ p)⁻¹ * ∑ i : ι, ‖a i‖ ^ p < 1}
h₁₁ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | (r ^ p)⁻¹ * ∑ i : ι, ‖a i‖ ^ p < 1}
h₁₂ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | ∑ i : ι, ‖a i‖ ^ p < r ^ p * 1}
h₁₃ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | ∑ i : ι, ‖a i‖ ^ p < r ^ p}
⊢ {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} =
    HSMul.hSMul (β := Set (ι → ℂ)) r {x : ι → ℂ | LT.lt (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) 1}
have h₁₄ : Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) ^ p < r ^ p}
  {a : ι → ℂ | ∑ i : ι, ‖a i‖ ^ p < r ^ p}
Tactic: simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hr), Set.preimage_setOf_eq, Pi.smul_apply,
        norm_smul, mul_rpow (norm_nonneg _) (norm_nonneg _), Real.norm_eq_abs, abs_inv, inv_rpow
        (abs_nonneg _), ← Finset.mul_sum, abs_eq_self.mpr (le_of_lt hr), inv_mul_lt_iff₀
        (rpow_pos_of_pos hr _), mul_one, ← rpow_lt_rpow_iff (rpow_nonneg (h₁ _) _)
        (le_of_lt hr) (by linarith : 0 < p), ← rpow_mul (h₁ _), div_mul_cancel₀ _
        (ne_of_gt (by linarith) : p ≠ 0), Real.rpow_one]
-- 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₁ : ∀ (x : ι → ℂ), LE.le (α := ℝ) 0 (∑ i : ι, ‖x i‖ ^ p)
h₂ : ∀ (x : ι → ℂ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
hr : 0 < r
⊢ ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (r ^ finrank.{0, u_1} ℝ (ι → ℂ))
have h : ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (HPow.hPow (β := ℕ) r (∑ i : ι, finrank ℝ ℂ))
Tactic: simp_rw [finrank_pi_fintype ℝ, Complex.finrank_real_complex, Finset.sum_const, smul_eq_mul,
        mul_comm, Fintype.card]
-- 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₁ : ∀ (x : ι → ℂ), LE.le (α := ℝ) 0 (∑ i : ι, ‖x i‖ ^ p)
h₂ : ∀ (x : ι → ℂ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
hr : 0 < r
h : ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (HPow.hPow (β := ℕ) r (∑ i : ι, finrank ℝ ℂ))
⊢ ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (r ^ finrank.{0, u_1} ℝ (ι → ℂ))
have h₃ : ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (HPow.hPow (β := ℕ) r (∑ x : ι, 2))
Tactic: simp_rw [finrank_pi_fintype ℝ, Complex.finrank_real_complex, Finset.sum_const, smul_eq_mul,
        mul_comm, Fintype.card]
-- 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₁ : ∀ (x : ι → ℂ), LE.le (α := ℝ) 0 (∑ i : ι, ‖x i‖ ^ p)
h₂ : ∀ (x : ι → ℂ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
hr : 0 < r
h : ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (HPow.hPow (β := ℕ) r (∑ i : ι, finrank ℝ ℂ))
h₃ : ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (HPow.hPow (β := ℕ) r (∑ x : ι, 2))
⊢ ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (r ^ finrank.{0, u_1} ℝ (ι → ℂ))
have h₄ : ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (r ^ HSMul.hSMul (β := ℕ) (Finset.card.{u_1} (α := ι) Finset.univ) 2)
Tactic: simp_rw [finrank_pi_fintype ℝ, Complex.finrank_real_complex, Finset.sum_const, smul_eq_mul,
        mul_comm, Fintype.card]
-- 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₁ : ∀ (x : ι → ℂ), LE.le (α := ℝ) 0 (∑ i : ι, ‖x i‖ ^ p)
h₂ : ∀ (x : ι → ℂ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
hr : 0 < r
h : ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (HPow.hPow (β := ℕ) r (∑ i : ι, finrank ℝ ℂ))
h₃ : ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (HPow.hPow (β := ℕ) r (∑ x : ι, 2))
h₄ :
  ENNReal.ofReal (r ^ (2 * card ι)) =
    ENNReal.ofReal (r ^ HSMul.hSMul (β := ℕ) (Finset.card.{u_1} (α := ι) Finset.univ) 2)
⊢ ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (r ^ finrank.{0, u_1} ℝ (ι → ℂ))
have h₅ : ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (r ^ (Finset.card.{u_1} (α := ι) Finset.univ * 2))
Tactic: simp_rw [finrank_pi_fintype ℝ, Complex.finrank_real_complex, Finset.sum_const, smul_eq_mul,
        mul_comm, Fintype.card]
-- 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₁ : ∀ (x : ι → ℂ), LE.le (α := ℝ) 0 (∑ i : ι, ‖x i‖ ^ p)
h₂ : ∀ (x : ι → ℂ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
hr : 0 < r
h : ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (HPow.hPow (β := ℕ) r (∑ i : ι, finrank ℝ ℂ))
h₃ : ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (HPow.hPow (β := ℕ) r (∑ x : ι, 2))
h₄ :
  ENNReal.ofReal (r ^ (2 * card ι)) =
    ENNReal.ofReal (r ^ HSMul.hSMul (β := ℕ) (Finset.card.{u_1} (α := ι) Finset.univ) 2)
h₅ : ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (r ^ (Finset.card.{u_1} (α := ι) Finset.univ * 2))
⊢ ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (r ^ finrank.{0, u_1} ℝ (ι → ℂ))
have h₆ : ENNReal.ofReal (r ^ (card ι * 2)) = ENNReal.ofReal (r ^ (Finset.card.{u_1} (α := ι) Finset.univ * 2))
Tactic: simp_rw [finrank_pi_fintype ℝ, Complex.finrank_real_complex, Finset.sum_const, smul_eq_mul,
        mul_comm, Fintype.card]
-- 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 : ℝ
⊢ ((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 h₁ : 0 < p
Tactic: have h₁ : 0 < p := by linarith
-- 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
⊢ ((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 this : (ENNReal.ofReal p).toReal = p
Tactic: have : (ENNReal.ofReal p).toReal = p := toReal_ofReal (le_of_lt h₁)
-- 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 : (ENNReal.ofReal p).toReal = 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 eq_norm : ∀ (x : ι → ℂ),
  Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) =
    HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
Tactic: have eq_norm (x : ι → ℂ) : ‖toLp (.ofReal p) x‖ = (∑ i, ‖x i‖ ^ p) ^ (1 / p) := by
    simp [PiLp.norm_eq_sum (f := toLp (.ofReal p) x) (this.symm ▸ h₁), this]
-- 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 : (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)
⊢ ((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 this₁ : Fact (1 ≤ ENNReal.ofReal p)
Tactic: have : Fact (1 ≤ ENNReal.ofReal p) := fact_iff.mpr (ENNReal.ofReal_one ▸ (ofReal_le_ofReal hp))
-- 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)
⊢ ((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_zero : Norm.norm.{u_1} (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) 0) = 0
Tactic: have nm_zero : ‖toLp (.ofReal p) (0 : ι → ℂ)‖ = 0 := norm_zero
-- 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
⊢ ((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 eq_zero : ∀ (x : ι → ℂ), Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x) = 0 ↔ x = 0
Tactic: have eq_zero (x : ι → ℂ) : ‖toLp (.ofReal p) x‖ = 0 ↔ x = 0 :=
    norm_eq_zero.trans (toLp_eq_zero _)
-- 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
⊢ ((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 : ι → ℂ),
  Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (-toLp (ENNReal.ofReal p) x) =
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℂ)) (toLp (ENNReal.ofReal p) x)
Tactic: have nm_neg := fun x : ι → ℂ => norm_neg (toLp (.ofReal p) x)
-- 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)
⊢ ((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 : ι → ℂ),
  ‖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)
Tactic: have nm_add := fun x y : ι → ℂ => norm_add_le (toLp (.ofReal p) x) (toLp (.ofReal p) y)
-- 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)
⊢ ((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 : ι → ℂ),
  ‖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)
Tactic: have nm_smul := fun (r : ℝ) (x : ι → ℂ) =>
    norm_smul_le (β := PiLp (.ofReal p) (fun _ : ι => ℂ)) r (toLp (.ofReal p) x)
-- 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)
⊢ ((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 eq_zero₁ : ∀ (x : ι → ℂ), HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) = 0 ↔ x = 0
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
⊢ ((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_zero₁ : HPow.hPow (α := ℝ) (∑ i : ι, Norm.norm (E := ℂ) (0 i) ^ p) (1 / p) = 0
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