no goals
ι : Type u_1
ι' : Type ?u.584231
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.584240
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.584260
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.584278
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.584298
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
a : 𝕜
j : ι
⊢ single i a j = if j = i then a else 0
rw [EuclideanSpace.single, PiLp.equiv_symm_apply, ← Pi.single_apply i a j]