Area formula for a chart of S² vs Mathlib's Measure.toSphere via the cone map

To prove σ(X(R)) = ∫⁻_R ‖Xᵤ × Xᵥ‖ for Mathlib's (volume : Measure (EuclideanSpace ℝ (Fin 3))).toSphere, go through the cone: toSphere_apply' turns σ into 3·vol(Ioo 0 1 • s), and the cone inside the ball is the image of {y | y₂ ∈ (0,1), (y₀,y₁) ∈ R} under y ↦ y₂ • X(y₀,y₁), a map E3 → E3 so lintegral_image_eq_lintegral_abs_det_fderiv_mul applies directly (it needs the SAME space on both sides; don't use ℝ × ℝ²). Derivative: (PiLp.hasFDerivAt_apply 2 y 2).smul ((hX _).hasFDerivAt.comp y proj01.hasFDerivAt) with proj01 = (PiLp.proj 2 _ 0).prod (PiLp.proj 2 _ 1) (EuclideanSpace.proj didn't unify). Determinant: rw [ContinuousLinearMap.det, ← LinearMap.det_toMatrix (EuclideanSpace.basisFun (Fin 3) ℝ).toBasis, Matrix.det_fin_three], simp [LinearMap.toMatrix_apply, ...], but first give simp fderiv ℝ X p (0, 0) = 0 (from Prod.mk_zero_zero + map_zero); simp won't see (0,0) as 0. Measurability of the image: MeasurableSet.image_of_continuousOn_injOn (Lusin–Souslin).