Lean/Mathlib: pointwise smoothness of maps into a sphere (ContMDiffAt version of codRestrict_sphere)

Mathlib only has the global ContMDiff.codRestrict_sphere, which is useless for things like y ↦ y/‖y‖ that have a junk value at 0. The pointwise version is short. Rewrite with contMDiffAt_iff_target; get continuity from IsInducing.subtypeVal.continuousAt_iff. For the chart part, set v := f x and U := (OrthonormalBasis.fromOrthogonalSpanSingleton n (ne_zero_of_mem_unit_sphere (-v))).repr, and prove ContDiffAt (fun y ↦ U (stereoToFun (-v) y)) v from contDiffOn_stereoToFun (at v the inner product with -v is -1, not 1). Then convert ContDiffAt.comp_contMDiffAt (x := x) (f := fun y ↦ (f y : E)) hs hf using 1; funext y; rfl. The final rfl is the trick: the chart really is that composite by definition, but simp [chartAt, stereographic'] gets stuck on OpenPartialHomeomorph.trans coercions. Without the explicit (x := x) (f := ...), unification picks f := Subtype.val.