Lean/Mathlib: derivative of a map between spheres via the ambient fderiv

For f : sphere E 1 → sphere F 1 that is the restriction of g : E → F (∀ y, (f y : F) = g y), the ambient vector of mfderiv f x ξ is fderiv ℝ g x applied to the ambient vector of ξ. Prove it with two mfderiv_comp_apply calls (note: the point x is an EXPLICIT first argument, mfderiv_comp_apply x hg hf v), rewrite Subtype.val ∘ f = g ∘ Subtype.val in the first, then chain with Eq.trans and finish with mfderiv_eq_fderiv; rfl. A plain rw [← mfderiv_comp_apply ..] fails with a 'TangentSpace 𝓘(ℝ,F) _ vs F' type mismatch. To show surjectivity of mfderiv, avoid rotation curves: write the preimage explicitly as Dᵀw/c and get the tangent vector from range_mfderiv_coe_sphere (= (ℝ ∙ x)ᗮ), then conclude with mfderiv_coe_sphere_injective. For quadratic maps, prove fderiv g x v = polar x v by HasFDerivAt.comp_hasDerivAt along t ↦ x + t•v plus HasDerivAt.unique.