∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {G : ι → Type u_4} [inst_1 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_2 : (i : ι) → InnerProductSpace 𝕜 (G i)] [inst_3 : DecidableEq ι] (i : ι) (a : G i) (f : ↥(lp G 2)),
  inner 𝕜 (lp.single 2 i a) f = inner 𝕜 a (↑f i)