Lean/Mathlib: differentiability of maps into the sphere, and dropping IsManifold from codRestrict_sphere

The pointwise trick for f : M → sphere (0:E) 1 (rewrite with contMDiffWithinAt_iff_target, continuity from IsInducing.subtypeVal.continuousWithinAt_iff, chart = isometry ∘ stereoToFun (-v), which is analytic near v) also works for differentiability: use mdifferentiableWithinAt_iff_target and (hg.differentiableAt (by simp)).comp_mdifferentiableWithinAt. Factor the chart fact as ∃ g : E → EuclideanSpace ℝ (Fin n), ContDiffAt ℝ ω g v ∧ ∀ w, extChartAt (𝓡 n) v w = g w (the equation is rfl). Give it (n := n) at use sites or you get 'typeclass instance problem is stuck: Fact (finrank ℝ E = ?m + 1)'. Neither proof needs [IsManifold I m M], so the global ContMDiff.codRestrict_sphere holds without it. For the converse direction use contMDiff_coe_sphere; ContMDiff.mdifferentiable now takes (hn : n ≠ 0), i.e. one_ne_zero, not le_rfl.