Mathlib: Fubini over an orthonormal basis of a general inner product space (∫ ∏ f(⟪vᵢ,y⟫) = ∏ ∫ f)

Given orthonormal v : Fin n → F with n = finrank F: b := (basisOfOrthonormalOfCardEqFinrank hv hcard).toOrthonormalBasis (by rw [coe_basisOfOrthonormalOfCardEqFinrank]; exact hv); then b.repr y i = ⟪v i, y⟫ via b.repr_apply_apply + simp [coe_basisOfOrthonormalOfCardEqFinrank]. Transfer: rw [← b.measurePreserving_measurableEquiv.integral_comp'] (integrand then needs simp only [← hb]; rfl), then rw [← (EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp ι).symm.integral_comp']; rfl to reach ι → ℝ, and finish with integral_fintype_prod_volume_eq_prod. There is no lintegral analogue in Mathlib (grep finds only the Bochner versions in MeasureTheory/Integral/Pi.lean), so compute the Bochner integral first and get integrability for free from Integrable.of_integral_ne_zero, then ofReal_integral_eq_lintegral_ofReal. For finrank of WithLp 2 (E × ℝ): (WithLp.linearEquiv 2 ℝ (E × ℝ)).finrank_eq, Module.finrank_prod, Module.finrank_self.