rw [← EuclideanSpace.inner_piLp_equiv_symm, inner_self_eq_norm_sq_to_K, Complex.ofReal_pow]
ι : Type ?u.87124
R : Type ?u.87127
l : Type ?u.87130
m : Type ?u.87133
n : Type u_1
p : Type ?u.87139
q : Type ?u.87142
r : Type ?u.87145
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 → ℂ
⊢ ↑(‖(WithLp.equiv 2 (n → ℂ)).symm x‖ ^ 2) = star x ⬝ᵥ x
ι : Type ?u.87124
R : Type ?u.87127
l : Type ?u.87130
m : Type ?u.87133
n : Type u_1
p : Type ?u.87139
q : Type ?u.87142
r : Type ?u.87145
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 → ℂ
⊢ ↑‖(WithLp.equiv 2 (n → ℂ)).symm x‖ ^ 2 = ↑‖(WithLp.equiv 2 (n → ℂ)).symm x‖ ^ 2