-- Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
theorem MeasureTheory.volume_sum_rpow_le [Nonempty ι] {p : ℝ} (hp : 1 ≤ p) (r : ℝ) :
    volume {x : ι → ℝ | (∑ i, |x i| ^ p) ^ (1 / p) ≤ r} = (.ofReal r) ^ card ι *
      .ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (card ι / p + 1))

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Tactic:
have h₁ : 0 < p := by linarith

Result:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
eq_zero : ∀ (x : ι → ℝ), (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) = 0 ↔ x = 0
nm_zero : (∑ x : ι, |0 x| ^ p) ^ (1 / p) = 0
nm_neg : ∀ (x : ι → ℝ), (∑ x_1 : ι, |(-x) x_1| ^ p) ^ (1 / p) = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)
nm_add :
  ∀ (x y : ι → ℝ),
    (∑ x_1 : ι, |(x + y) x_1| ^ p) ^ (1 / p) ≤ (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) + (∑ x : ι, |y x| ^ p) ^ (1 / p)
nm_smul : ∀ (r : ℝ) (x : ι → ℝ), ‖r • x‖ ≤ ‖r‖ * ‖x‖
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Tactic:
simp_rw [eq_norm, norm_eq_abs] at nm_smul

Result:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
eq_zero : ∀ (x : ι → ℝ), (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) = 0 ↔ x = 0
nm_zero : (∑ x : ι, |0 x| ^ p) ^ (1 / p) = 0
nm_neg : ∀ (x : ι → ℝ), (∑ x_1 : ι, |(-x) x_1| ^ p) ^ (1 / p) = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)
nm_add :
  ∀ (x y : ι → ℝ),
    (∑ x_1 : ι, |(x + y) x_1| ^ p) ^ (1 / p) ≤ (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) + (∑ x : ι, |y x| ^ p) ^ (1 / p)
nm_smul : ∀ (r : ℝ) (x : ι → ℝ), (∑ x_1 : ι, |(r • x) x_1| ^ p) ^ (1 / p) ≤ |r| * (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Tactic:
have : Fact (1 ≤ ENNReal.ofReal p) := fact_iff.mpr (ofReal_one ▸ (ofReal_le_ofReal hp))

Result:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Tactic:
have nm_zero := norm_zero (E := PiLp (.ofReal p) (fun _ : ι => ℝ))

Result:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : ‖0‖ = 0
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
⊢ 0 < p

Tactic:
linarith

Result:
no goals

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : ‖0‖ = 0
eq_zero : ∀ (x : ι → ℝ), ‖x‖ = 0 ↔ x = 0
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Tactic:
have nm_neg := fun x : ι → ℝ => norm_neg (E := PiLp (.ofReal p) (fun _ : ι => ℝ)) x

Result:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : ‖0‖ = 0
eq_zero : ∀ (x : ι → ℝ), ‖x‖ = 0 ↔ x = 0
nm_neg : ∀ (x : ι → ℝ), ‖-x‖ = ‖x‖
⊢ volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))