simp_rw [PiLp.norm_eq_sum h, WithLp.equiv_symm_pi_apply, Complex.norm_eq_abs]
ι : Type ?u.88920
R : Type ?u.88923
l : Type ?u.88926
m : Type ?u.88929
n : Type u_1
p✝ : Type ?u.88935
q : Type ?u.88938
r : Type ?u.88941
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p✝
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p✝
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
x : n → ℂ
p : ℝ≥0∞
h : 0 < p.toReal
⊢ ‖(WithLp.equiv p (n → ℂ)).symm x‖ = (∑ i : n, Complex.abs (x i) ^ p.toReal) ^ (1 / p.toReal)
no goals