Smooth maps into Mathlib's sphere manifold S² from ContDiff: codRestrict_sphere recipe

To view f : ℝ × ℝ → EuclideanSpace ℝ (Fin 3) with ‖f x‖ = 1 as a smooth map into the manifold Metric.sphere 0 1 (import Mathlib.Geometry.Manifold.Instances.Sphere): first provide instance : Fact (finrank ℝ (EuclideanSpace ℝ (Fin 3)) = 2 + 1) := ⟨by simp⟩ (Fin 3 is not syntactically Fin (2+1), so the built-in instance may not fire), then hf.contMDiff.codRestrict_sphere _ proves ContMDiff 𝓘(ℝ, ℝ × ℝ) (𝓡 2) n (Set.codRestrict f (Metric.sphere 0 1) hmem). For a unit normal w/‖w‖: ((hw.norm ℝ hne).inv fun q ↦ norm_ne_zero_iff.2 (hne q)).smul hw gives ContDiff (ContDiff.norm needs ∀ x, w x ≠ 0, and 𝕜 explicit). For ∞-smoothness of a partial derivative: (hX.fderiv_right (m := ∞) (by simp)).clm_apply contDiff_const.