awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℂ), LE.le (α := ℝ) 0 (∑ i : ι, ‖x i‖ ^ 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)
h : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(∑ i : ι, finrank ℝ ℂ) : ℝ) / p + 1
h₃ : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(∑ i : ι, 2) : ℝ) / p + 1
h₄ :
  HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 =
    (↑(HSMul.hSMul (β := ℕ) (Finset.card.{u_1} (α := ι) Finset.univ) 2) : ℝ) / p + 1
h₅ : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(Finset.card.{u_1} (α := ι) Finset.univ * 2) : ℝ) / p + 1
⊢ HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(finrank.{0, u_1} ℝ (ι → ℂ)) : ℝ) / p + 1
have h₆ : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 =
  HMul.hMul (α := ℝ) (↑(Finset.card.{u_1} (α := ι) Finset.univ) : ℝ) (↑2 : ℝ) / p + 1
Tactic: rw [finrank_pi_fintype, Complex.finrank_real_complex, Finset.sum_const, smul_eq_mul,
      Nat.cast_mul, Nat.cast_ofNat, Fintype.card, mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℂ), LE.le (α := ℝ) 0 (∑ i : ι, ‖x i‖ ^ 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)
h : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(∑ i : ι, finrank ℝ ℂ) : ℝ) / p + 1
h₃ : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(∑ i : ι, 2) : ℝ) / p + 1
h₄ :
  HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 =
    (↑(HSMul.hSMul (β := ℕ) (Finset.card.{u_1} (α := ι) Finset.univ) 2) : ℝ) / p + 1
h₅ : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(Finset.card.{u_1} (α := ι) Finset.univ * 2) : ℝ) / p + 1
h₆ :
  HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 =
    HMul.hMul (α := ℝ) (↑(Finset.card.{u_1} (α := ι) Finset.univ) : ℝ) (↑2 : ℝ) / p + 1
⊢ HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(finrank.{0, u_1} ℝ (ι → ℂ)) : ℝ) / p + 1
have h₇ : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 =
  HMul.hMul (α := ℝ) (↑(Finset.card.{u_1} (α := ι) Finset.univ) : ℝ) 2 / p + 1
Tactic: rw [finrank_pi_fintype, Complex.finrank_real_complex, Finset.sum_const, smul_eq_mul,
      Nat.cast_mul, Nat.cast_ofNat, Fintype.card, mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℂ), LE.le (α := ℝ) 0 (∑ i : ι, ‖x i‖ ^ 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)
h : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(∑ i : ι, finrank ℝ ℂ) : ℝ) / p + 1
h₃ : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(∑ i : ι, 2) : ℝ) / p + 1
h₄ :
  HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 =
    (↑(HSMul.hSMul (β := ℕ) (Finset.card.{u_1} (α := ι) Finset.univ) 2) : ℝ) / p + 1
h₅ : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(Finset.card.{u_1} (α := ι) Finset.univ * 2) : ℝ) / p + 1
h₆ :
  HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 =
    HMul.hMul (α := ℝ) (↑(Finset.card.{u_1} (α := ι) Finset.univ) : ℝ) (↑2 : ℝ) / p + 1
h₇ :
  HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 =
    HMul.hMul (α := ℝ) (↑(Finset.card.{u_1} (α := ι) Finset.univ) : ℝ) 2 / p + 1
⊢ HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(finrank.{0, u_1} ℝ (ι → ℂ)) : ℝ) / p + 1
have h₈ : HMul.hMul (α := ℝ) 2 (↑(Finset.card.{u_1} (α := ι) Finset.univ) : ℝ) / p + 1 =
  HMul.hMul (α := ℝ) (↑(Finset.card.{u_1} (α := ι) Finset.univ) : ℝ) 2 / p + 1
Tactic: rw [finrank_pi_fintype, Complex.finrank_real_complex, Finset.sum_const, smul_eq_mul,
      Nat.cast_mul, Nat.cast_ofNat, Fintype.card, mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℂ), LE.le (α := ℝ) 0 (∑ i : ι, ‖x i‖ ^ 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)
h : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(∑ i : ι, finrank ℝ ℂ) : ℝ) / p + 1
h₃ : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(∑ i : ι, 2) : ℝ) / p + 1
h₄ :
  HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 =
    (↑(HSMul.hSMul (β := ℕ) (Finset.card.{u_1} (α := ι) Finset.univ) 2) : ℝ) / p + 1
h₅ : HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(Finset.card.{u_1} (α := ι) Finset.univ * 2) : ℝ) / p + 1
h₆ :
  HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 =
    HMul.hMul (α := ℝ) (↑(Finset.card.{u_1} (α := ι) Finset.univ) : ℝ) (↑2 : ℝ) / p + 1
h₇ :
  HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 =
    HMul.hMul (α := ℝ) (↑(Finset.card.{u_1} (α := ι) Finset.univ) : ℝ) 2 / p + 1
h₈ :
  HMul.hMul (α := ℝ) 2 (↑(Finset.card.{u_1} (α := ι) Finset.univ) : ℝ) / p + 1 =
    HMul.hMul (α := ℝ) (↑(Finset.card.{u_1} (α := ι) Finset.univ) : ℝ) 2 / p + 1
⊢ HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1 = (↑(finrank.{0, u_1} ℝ (ι → ℂ)) : ℝ) / p + 1
have h₉ : HMul.hMul (α := ℝ) (↑(Finset.card.{u_1} (α := ι) Finset.univ) : ℝ) 2 / p + 1 =
  HMul.hMul (α := ℝ) (↑(Finset.card.{u_1} (α := ι) Finset.univ) : ℝ) 2 / p + 1
Tactic: rw [finrank_pi_fintype, Complex.finrank_real_complex, Finset.sum_const, smul_eq_mul,
      Nat.cast_mul, Nat.cast_ofNat, Fintype.card, mul_comm]
-- 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₁ : ∀ (x : ι → ℂ), LE.le (α := ℝ) 0 (∑ i : ι, ‖x i‖ ^ p)
Tactic: have h₁ (x : ι → ℂ) : 0 ≤ ∑ i, ‖x i‖ ^ p := by positivity
-- 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₁ : ∀ (x : ι → ℂ), LE.le (α := ℝ) 0 (∑ i : ι, ‖x i‖ ^ 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 h₂ : ∀ (x : ι → ℂ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
Tactic: have h₂ : ∀ x : ι → ℂ, 0 ≤ (∑ i, ‖x i‖ ^ p) ^ (1 / p) := fun x => rpow_nonneg (h₁ x) _
-- 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)
⊢ ((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 inl : ∀ (hr : r ≤ 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))
Tactic: obtain hr | hr := le_or_gt r 0
-- 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)
inl :
  ∀ (hr : r ≤ 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))
⊢ ((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 inr : ∀ (hr : 0 < 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))
Tactic: obtain hr | hr := le_or_gt r 0
-- 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 : r ≤ 0
⊢ Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} ∅
have h : ∀ (x : ι → ℂ),
  Membership.mem (γ := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} x ↔
    Membership.mem (γ := Set (ι → ℂ)) ∅ x
Tactic: ext x
-- 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 : r ≤ 0
x : ι → ℂ
⊢ Membership.mem (γ := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} x ↔
    Membership.mem (γ := Set (ι → ℂ)) ∅ x
have h : ∀ (hx : Membership.mem (γ := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} x),
  Membership.mem (γ := Set (ι → ℂ)) ∅ x
Tactic: refine ⟨fun hx => ?_, fun hx => hx.elim⟩
-- 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₁ : ∀ (x : ι → ℂ), LE.le (α := ℝ) 0 (∑ i : ι, ‖x i‖ ^ p)
h₂ : ∀ (x : ι → ℂ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p)
hr : r ≤ 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 this : Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} ∅
Tactic: have : {x : ι → ℂ | (∑ i, ‖x i‖ ^ p) ^ (1 / p) < r} = ∅ := by
      ext x
      refine ⟨fun hx => ?_, fun hx => hx.elim⟩
      exact not_le.mpr (lt_of_lt_of_le (Set.mem_setOf.mp hx) hr) (h₂ x)
-- 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 : r ≤ 0
this : Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (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 inl : ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞) ∅ =
  ENNReal.ofReal r ^ (2 * card ι) *
    ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
Tactic: rw [this, measure_empty, ← zero_eq_ofReal.mpr hr, zero_pow Fin.pos'.ne', zero_mul]
-- 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 : r ≤ 0
this : Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} ∅
inl :
  ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞) ∅ =
    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 inl₁ : 0 =
  ENNReal.ofReal r ^ (2 * card ι) *
    ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
Tactic: rw [this, measure_empty, ← zero_eq_ofReal.mpr hr, zero_pow Fin.pos'.ne', zero_mul]
-- 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 : r ≤ 0
this : Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} ∅
inl :
  ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞) ∅ =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
inl₁ :
  0 =
    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 inl₂ : 0 =
  HPow.hPow (α := ℝ≥0∞) 0 (2 * card ι) *
    ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
Tactic: rw [this, measure_empty, ← zero_eq_ofReal.mpr hr, zero_pow Fin.pos'.ne', zero_mul]
-- 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 : r ≤ 0
this : Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} ∅
inl :
  ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞) ∅ =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
inl₁ :
  0 =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
inl₂ :
  0 =
    HPow.hPow (α := ℝ≥0∞) 0 (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 inl₃ : 0 =
  0 * ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
Tactic: rw [this, measure_empty, ← zero_eq_ofReal.mpr hr, zero_pow Fin.pos'.ne', zero_mul]
-- 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 : r ≤ 0
this : Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} ∅
inl :
  ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞) ∅ =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
inl₁ :
  0 =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
inl₂ :
  0 =
    HPow.hPow (α := ℝ≥0∞) 0 (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (HMul.hMul (α := ℝ) 2 (↑(card ι) : ℝ) / p + 1))
inl₃ :
  0 =
    0 *
      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 inl₄ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [this, measure_empty, ← zero_eq_ofReal.mpr hr, zero_pow Fin.pos'.ne', zero_mul]
-- 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
⊢ ((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 inr : ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞)
    {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} =
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ (2 * card ι)))
    (((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞) {x : ι → ℂ | LT.lt (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) 1} : ℝ≥0∞)
Tactic: rw [← Complex.volume_sum_rpow_lt_one _ hp, ← ENNReal.ofReal_pow (le_of_lt hr)]
-- 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
⊢ ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞)
      {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ (2 * card ι)))
      (((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞) {x : ι → ℂ | LT.lt (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) 1} :
        ℝ≥0∞)
have h : {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} =
  HSMul.hSMul (β := Set (ι → ℂ)) r {x : ι → ℂ | LT.lt (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) 1}
Tactic: convert! addHaar_smul_of_nonneg volume (le_of_lt hr) {x : ι → ℂ | ∑ i, ‖x i‖ ^ p < 1} using 2
-- 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 :
  {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} =
    HSMul.hSMul (β := Set (ι → ℂ)) r {x : ι → ℂ | LT.lt (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) 1}
⊢ ((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞)
      {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r} =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ (2 * card ι)))
      (((volume : Measure (ι → ℂ)) : (a : Set (ι → ℂ)) → ℝ≥0∞) {x : ι → ℂ | LT.lt (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) 1} :
        ℝ≥0∞)
have h₃ : ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (r ^ finrank.{0, u_1} ℝ (ι → ℂ))
Tactic: convert! addHaar_smul_of_nonneg volume (le_of_lt hr) {x : ι → ℂ | ∑ i, ‖x i‖ ^ p < 1} using 2
-- 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
⊢ 0 < p
have linarith : p ≤ 0 → -1 + (1 - p) + (p - 0) = 0
Tactic: linarith