-- Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
theorem Complex.volume_sum_rpow_lt_one {p : ℝ} (hp : 1 ≤ p) :
    volume {x : ι → ℂ | ∑ i, ‖x i‖ ^ p < 1} =
      .ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * card ι / p + 1))

Proof state:
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ 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} =
    ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(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

Result:
case h.e'_2.h.e'_6.h.e'_2.h.a
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ 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)
x✝ : ι → ℂ
⊢ ∑ i : ι, ‖x✝ i‖ ^ p < 1 ↔ (∑ i : ι, ‖x✝ i‖ ^ p) ^ (1 / p) < 1

case h.e'_3.h.e'_1.h.e'_5
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ 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)
⊢ (π * Real.Gamma (2 / p + 1)) ^ card ι = ∫ (x : ι → ℂ), rexp (-((∑ i : ι, ‖x i‖ ^ p) ^ (1 / p)) ^ p)

case h.e'_3.h.e'_1.h.e'_6.h.e'_1
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ 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)
⊢ 2 * ↑(card ι) / p + 1 = ↑(finrank ℝ (ι → ℂ)) / p + 1

Proof state:
case h.e'_3.h.e'_1.h.e'_6.h.e'_1
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ 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)
⊢ 2 * ↑(card ι) / p + 1 = ↑(finrank ℝ (ι → ℂ)) / 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]

Result:
no goals

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

Tactic:
have eq_norm := fun x : ι → ℂ => (PiLp.norm_eq_sum (p := .ofReal p) (f := x)
  ((toReal_ofReal (le_of_lt h₁)).symm ▸ h₁))

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

Proof state:
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ 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} =
    ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))

Tactic:
have eq_zero := fun x : ι → ℂ => norm_eq_zero (E := PiLp (.ofReal p) (fun _ : ι => ℂ)) (a := x)

Result:
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ 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} =
    ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))

Proof state:
case h.e'_2.h.e'_6.h.e'_2.h.a
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ 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)
x✝ : ι → ℂ
⊢ ∑ i : ι, ‖x✝ i‖ ^ p < 1 ↔ (∑ i : ι, ‖x✝ i‖ ^ p) ^ (1 / p) < 1

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

Result:
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ 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)
x✝ : ι → ℂ
⊢ 0 ≤ ∑ i : ι, ‖x✝ i‖ ^ p