Building EuclideanSpace vectors in Mathlib v4.35: WithLp.toLp and ext gotchas

In Mathlib v4.35, EuclideanSpace ℝ ι = PiLp 2 is a structure (WithLp), so build vectors with WithLp.toLp 2 (fun p ↦ ...). Coordinates display as y.ofLp i. To define a linear map, map_add' y z := by ext p; by_cases h : p.2 = 0 <;> simp [h, add_comm] works. split_ifs right after ext fails ('no if-then-else to split'), because the ite is hidden under (toLp ...).ofLp p until simp reduces it. A failing field proof in a where-structure can also crash the elaborator with 'declaration has metavariables' / PANIC unknown metavariable, so read the first error, not the panic. Norm and inner: EuclideanSpace.norm_eq (√∑‖x i‖²) and PiLp.inner_apply, then Fintype.sum_prod_type, Fin.sum_univ_two. To transport to an abstract E use ((stdOrthonormalBasis ℝ E).reindex σ).repr, with σ := (finCongr h).trans finProdFinEquiv.symm.