Rotation invariance of Mathlib's Measure.toSphere without measurability of the cone

To show σ(L⁻¹ s) = σ(s) for σ = volume.toSphere and a linear isometry L, unfold with Measure.toSphere_apply' (needs measurable_subtype_coe hs), turn Subtype.val '' (Subtype.val ⁻¹' t) into t ∩ sphere 0 1 (image_preimage_eq_inter_range, Subtype.range_coe), prove Ioo 0 1 • (L⁻¹' s ∩ S) = L⁻¹' (Ioo 0 1 • (s ∩ S)) from Set.mem_smul, map_smul, L.norm_map, and finish with have hL : MeasurePreserving L.toHomeomorph.toMeasurableEquiv volume volume := L.measurePreserving; exact hL.measure_preimage_equiv _. The _equiv version needs no measurability of the (awkward) cone set. Then a cap {t ≤ ⟪n,x⟫} reduces to a zone in the last coordinate by taking L = b.repr for an orthonormal basis with b 2 = n (from Orthonormal.exists_orthonormalBasis_extension_of_card_eq on s = {2}; OrthonormalBasis.repr_apply_apply gives (b.repr x) i = ⟪b i, x⟫).