awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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)
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 : ι, HPow.hPow (α := ℝ) |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)
⊢ ∀ (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,
    norm_eq_abs] at eq_zero nm_zero nm_neg nm_add nm_smul

Premises used: WithLp.toLp_smul, WithLp.toLp_neg, WithLp.toLp_add, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 : ι, HPow.hPow (α := ℝ) |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)
linarith : p ≤ 0 → -1 + (1 - p) + (p - 0) = 0
⊢ 0 < p

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 : ι, HPow.hPow (α := ℝ) |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 : ∀ (x : ι → ℝ), LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1 ↔ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < 1
h₃ :
  (2 * Gamma (1 / p + 1)) ^ card ι =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ι → ℝ) ↦
      rexp (-HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) ^ p)
h₄ : (↑(card ι) : ℝ) / p + 1 = (↑(finrank.{0, u_1} ℝ (ι → ℝ)) : ℝ) / p + 1
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1} =
    ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))

Tactic:
convert!
    (measure_lt_one_eq_integral_div_gamma (volume : Measure (ι → ℝ)) (g := fun x =>
      (∑ i, |x i| ^ p) ^ (1 / p)) nm_zero nm_neg nm_add (eq_zero _).mp (fun r x => nm_smul r x)
      (by linarith : 0 < p)) using 4

Premises used: MeasureTheory.measure_lt_one_eq_integral_div_gamma, MeasureTheory.MeasureSpace.volume, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 : ι, HPow.hPow (α := ℝ) |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)
x : ι → ℝ
rw : LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
⊢ LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1 ↔ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < 1

Tactic:
rw [rpow_lt_one_iff' _ (one_div_pos.mpr h₁)]

Premises used: Iff.mpr, one_div_pos, Real.rpow_lt_one_iff'
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 : ι, HPow.hPow (α := ℝ) |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)
x : ι → ℝ
⊢ LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)

Tactic:
Finset.sum_nonneg' (fun _ => rpow_nonneg (abs_nonneg _) _)

Premises used: Finset.sum_nonneg', Real.rpow_nonneg, abs_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 : ι, HPow.hPow (α := ℝ) |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)
x : ι → ℝ
⊢ LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)

Tactic:
exact Finset.sum_nonneg' (fun _ => rpow_nonneg (abs_nonneg _) _)

Premises used: Finset.sum_nonneg', Real.rpow_nonneg, abs_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 : ι, HPow.hPow (α := ℝ) |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 :
  (2 * Gamma (1 / p + 1)) ^ card ι =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ι → ℝ) ↦ ∏ x_1 : ι, rexp (-|x x_1| ^ p)
⊢ (2 * Gamma (1 / p + 1)) ^ card ι =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ι → ℝ) ↦
      rexp (-HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) ^ p)

Tactic:
simp_rw [← rpow_mul (h₂ _), div_mul_cancel₀ _ (ne_of_gt h₁), Real.rpow_one,
      ← Finset.sum_neg_distrib, exp_sum]

Premises used: div_mul_cancel₀, ne_of_gt, Real.rpow_one, Real.rpow_mul, Finset.sum_neg_distrib, Real.exp_sum
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 : ι, HPow.hPow (α := ℝ) |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 :
  (2 * Gamma (1 / p + 1)) ^ card ι =
    HPow.hPow (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-|x| ^ p)) (card ι)
h₃ :
  (2 * Gamma (1 / p + 1)) ^ card ι =
    HMul.hMul (α := ℝ) 2
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (restrict volume (Set.Ioi 0)) fun (x : ℝ) ↦ rexp (-x ^ p)) ^
      card ι
h₄ h₅ : (2 * Gamma (1 / p + 1)) ^ card ι = (2 * Gamma (1 / p + 1)) ^ card ι
⊢ (2 * Gamma (1 / p + 1)) ^ card ι =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ι → ℝ) ↦ ∏ x_1 : ι, rexp (-|x x_1| ^ p)

Tactic:
rw [integral_fintype_prod_volume_eq_pow fun x : ℝ => exp (- |x| ^ p), integral_comp_abs
      (f := fun x => exp (- x ^ p)), integral_exp_neg_rpow h₁]

Premises used: MeasureTheory.integral_fintype_prod_volume_eq_pow, abs, integral_comp_abs, Real.exp, integral_exp_neg_rpow, HPow.hPow, Neg.neg
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 : ι, HPow.hPow (α := ℝ) |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 h₃ : (↑(card ι) : ℝ) / p + 1 = (↑(card ι) : ℝ) / p + 1
⊢ (↑(card ι) : ℝ) / p + 1 = (↑(finrank.{0, u_1} ℝ (ι → ℝ)) : ℝ) / p + 1

Tactic:
rw [finrank_fintype_fun_eq_card]

Premises used: Module.finrank_fintype_fun_eq_card
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
x : ι → ℝ
⊢ LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
⊢ ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)

Tactic:
have h₁ (x : ι → ℝ) : 0 ≤ ∑ i, |x i| ^ p := by positivity
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
⊢ ∀ (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) _
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
inr :
  ∀ (hr : 0 < r),
    ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
        {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
      ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))

Tactic:
obtain hr | hr := le_or_gt r 0

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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
h :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} x ↔
      Membership.mem (γ := Set (ι → ℝ)) ∅ x
⊢ Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} ∅

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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

Tactic:
⟨fun hx => ?_, fun hx => hx.elim⟩

Premises used: False.elim, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 : ι → ℝ
h :
  ∀ (hx : Membership.mem (γ := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} x),
    Membership.mem (γ := Set (ι → ℝ)) ∅ x
⊢ 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⟩
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} x
⊢ Membership.mem (γ := Set (ι → ℝ)) ∅ x

Tactic:
not_le.mpr (lt_of_lt_of_le (Set.mem_setOf.mp hx) hr) (h₂ x)

Premises used: not_le, Iff.mpr, Set.Mem, Set.mem_setOf, Iff.mp, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} x
⊢ Membership.mem (γ := Set (ι → ℝ)) ∅ x

Tactic:
exact not_le.mpr (lt_of_lt_of_le (Set.mem_setOf.mp hx) hr) (h₂ x)

Premises used: not_le, Iff.mpr, Set.mem_setOf, Iff.mp, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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} ∅

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)
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
inl₁ :
  0 = ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
inl₂ :
  0 =
    HPow.hPow (α := ℝ≥0∞) 0 (card ι) *
      ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
inl₃ : 0 = 0 * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
inl₄ inl₅ : Eq (α := ℝ≥0∞) 0 0
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))

Tactic:
rw [this, measure_empty, ← zero_eq_ofReal.mpr hr, zero_pow Fin.pos'.ne', zero_mul]

Premises used: Iff.mpr, MulZeroClass.zero_mul, MeasureTheory.measure_empty, LT.lt.ne', Fin.pos', ENNReal.zero_eq_ofReal, zero_pow
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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
inr :
  ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank.{0, u_1} ℝ (ι → ℝ)))
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1} :
        ℝ≥0∞)
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))

Tactic:
rw [← volume_sum_rpow_lt_one _ hp, ← ofReal_pow (le_of_lt hr), ← finrank_pi ℝ]

Premises used: Real, le_of_lt, Module.finrank_pi, ENNReal.ofReal_pow, MeasureTheory.volume_sum_rpow_lt_one
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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∞)
      (HSMul.hSMul (β := Set (ι → ℝ)) r {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1}) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank.{0, u_1} ℝ (ι → ℝ)))
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1} :
        ℝ≥0∞)

Tactic:
addHaar_smul_of_nonneg volume (le_of_lt hr) {x : ι → ℝ | ∑ i, |x i| ^ p < 1}

Premises used: Finset.univ, abs, setOf, le_of_lt, HPow.hPow, MeasureTheory.MeasureSpace.volume, MeasureTheory.Measure.addHaar_smul_of_nonneg, LT.lt, OfNat.ofNat, Finset.sum
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 ^ finrank.{0, u_1} ℝ (ι → ℝ)))
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1} :
        ℝ≥0∞)

Tactic:
convert! addHaar_smul_of_nonneg volume (le_of_lt hr) {x : ι → ℝ | ∑ i, |x i| ^ p < 1} using 2

Premises used: Finset.univ, abs, setOf, le_of_lt, HPow.hPow, MeasureTheory.MeasureSpace.volume, MeasureTheory.Measure.addHaar_smul_of_nonneg, LT.lt, OfNat.ofNat, Finset.sum
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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
linarith : p ≤ 0 → -1 + (1 - p) + (p - 0) = 0
⊢ 0 < p

Tactic:
linarith