Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case e'_2
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this✝ : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i, ‖x i‖ ^ p
eq_norm : ∀ (x : ι → ℂ), ‖toLp (ENNReal.ofReal p) x‖ = (∑ i, ‖x i‖ ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
eq_zero : ∀ (x : ι → ℂ), (∑ i, ‖x i‖ ^ p) ^ (1 / p) = 0 ↔ x = 0
nm_zero : (∑ i, ‖0 i‖ ^ p) ^ (1 / p) = 0
nm_neg : ∀ (x : ι → ℂ), (∑ i, ‖(-x) i‖ ^ p) ^ (1 / p) = (∑ i, ‖x i‖ ^ p) ^ (1 / p)
nm_add : ∀ (x y : ι → ℂ), (∑ i, ‖(x + y) i‖ ^ p) ^ (1 / p) ≤ (∑ i, ‖x i‖ ^ p) ^ (1 / p) + (∑ i, ‖y i‖ ^ p) ^ (1 / p)
nm_smul : ∀ (r : ℝ) (x : ι → ℂ), (∑ i, ‖(r • x) i‖ ^ p) ^ (1 / p) ≤ ‖r‖ * (∑ i, ‖x i‖ ^ p) ^ (1 / p)
x✝ : ι → ℂ
⊢ ∑ i, ‖x✝ i‖ ^ p < 1 ↔ (∑ i, ‖x✝ i‖ ^ p) ^ (1 / p) < 1

pp: case e'_3.e'_5
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this✝ : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i, ‖x i‖ ^ p
eq_norm : ∀ (x : ι → ℂ), ‖toLp (ENNReal.ofReal p) x‖ = (∑ i, ‖x i‖ ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
eq_zero : ∀ (x : ι → ℂ), (∑ i, ‖x i‖ ^ p) ^ (1 / p) = 0 ↔ x = 0
nm_zero : (∑ i, ‖0 i‖ ^ p) ^ (1 / p) = 0
nm_neg : ∀ (x : ι → ℂ), (∑ i, ‖(-x) i‖ ^ p) ^ (1 / p) = (∑ i, ‖x i‖ ^ p) ^ (1 / p)
nm_add : ∀ (x y : ι → ℂ), (∑ i, ‖(x + y) i‖ ^ p) ^ (1 / p) ≤ (∑ i, ‖x i‖ ^ p) ^ (1 / p) + (∑ i, ‖y i‖ ^ p) ^ (1 / p)
nm_smul : ∀ (r : ℝ) (x : ι → ℂ), (∑ i, ‖(r • x) i‖ ^ p) ^ (1 / p) ≤ ‖r‖ * (∑ i, ‖x i‖ ^ p) ^ (1 / p)
⊢ (π * Real.Gamma (2 / p + 1)) ^ card ι = ∫ (x : ι → ℂ), rexp (-((∑ i, ‖x i‖ ^ p) ^ (1 / p)) ^ p)

pp: case e'_3.e'_6
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this✝ : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i, ‖x i‖ ^ p
eq_norm : ∀ (x : ι → ℂ), ‖toLp (ENNReal.ofReal p) x‖ = (∑ i, ‖x i‖ ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
eq_zero : ∀ (x : ι → ℂ), (∑ i, ‖x i‖ ^ p) ^ (1 / p) = 0 ↔ x = 0
nm_zero : (∑ i, ‖0 i‖ ^ p) ^ (1 / p) = 0
nm_neg : ∀ (x : ι → ℂ), (∑ i, ‖(-x) i‖ ^ p) ^ (1 / p) = (∑ i, ‖x i‖ ^ p) ^ (1 / p)
nm_add : ∀ (x y : ι → ℂ), (∑ i, ‖(x + y) i‖ ^ p) ^ (1 / p) ≤ (∑ i, ‖x i‖ ^ p) ^ (1 / p) + (∑ i, ‖y i‖ ^ p) ^ (1 / p)
nm_smul : ∀ (r : ℝ) (x : ι → ℂ), (∑ i, ‖(r • x) i‖ ^ p) ^ (1 / p) ≤ ‖r‖ * (∑ i, ‖x i‖ ^ p) ^ (1 / p)
⊢ 2 * ↑(card ι) / p + 1 = ↑(finrank ℝ (ι → ℂ)) / p + 1

Tactic:
· rw [rpow_lt_one_iff' _ (one_div_pos.mpr h₁)]
    exact Finset.sum_nonneg' (fun _ => rpow_nonneg (norm_nonneg _) _)

Goal state after:
case e'_3.e'_5
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this✝ : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i, ‖x i‖ ^ p
eq_norm : ∀ (x : ι → ℂ), ‖toLp (ENNReal.ofReal p) x‖ = (∑ i, ‖x i‖ ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
eq_zero : ∀ (x : ι → ℂ), (∑ i, ‖x i‖ ^ p) ^ (1 / p) = 0 ↔ x = 0
nm_zero : (∑ i, ‖0 i‖ ^ p) ^ (1 / p) = 0
nm_neg : ∀ (x : ι → ℂ), (∑ i, ‖(-x) i‖ ^ p) ^ (1 / p) = (∑ i, ‖x i‖ ^ p) ^ (1 / p)
nm_add : ∀ (x y : ι → ℂ), (∑ i, ‖(x + y) i‖ ^ p) ^ (1 / p) ≤ (∑ i, ‖x i‖ ^ p) ^ (1 / p) + (∑ i, ‖y i‖ ^ p) ^ (1 / p)
nm_smul : ∀ (r : ℝ) (x : ι → ℂ), (∑ i, ‖(r • x) i‖ ^ p) ^ (1 / p) ≤ ‖r‖ * (∑ i, ‖x i‖ ^ p) ^ (1 / p)
⊢ (π * Real.Gamma (2 / p + 1)) ^ card ι = ∫ (x : ι → ℂ), rexp (-((∑ i, ‖x i‖ ^ p) ^ (1 / p)) ^ p)

case e'_3.e'_6
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this✝ : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i, ‖x i‖ ^ p
eq_norm : ∀ (x : ι → ℂ), ‖toLp (ENNReal.ofReal p) x‖ = (∑ i, ‖x i‖ ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
eq_zero : ∀ (x : ι → ℂ), (∑ i, ‖x i‖ ^ p) ^ (1 / p) = 0 ↔ x = 0
nm_zero : (∑ i, ‖0 i‖ ^ p) ^ (1 / p) = 0
nm_neg : ∀ (x : ι → ℂ), (∑ i, ‖(-x) i‖ ^ p) ^ (1 / p) = (∑ i, ‖x i‖ ^ p) ^ (1 / p)
nm_add : ∀ (x y : ι → ℂ), (∑ i, ‖(x + y) i‖ ^ p) ^ (1 / p) ≤ (∑ i, ‖x i‖ ^ p) ^ (1 / p) + (∑ i, ‖y i‖ ^ p) ^ (1 / p)
nm_smul : ∀ (r : ℝ) (x : ι → ℂ), (∑ i, ‖(r • x) i‖ ^ p) ^ (1 / p) ≤ ‖r‖ * (∑ i, ‖x i‖ ^ p) ^ (1 / p)
⊢ 2 * ↑(card ι) / p + 1 = ↑(finrank ℝ (ι → ℂ)) / p + 1