Smooth vector field on a Mathlib manifold without charts: push ∂/∂t through tangentMap

Goal: a section x ↦ ⟨x, ξ x⟩ : TangentBundle (𝓡 n) (sphere 0 1) that is ContMDiff ∞ (e.g. the rotation field on odd spheres). Proving smoothness through trivializations/stereographic charts is painful. Instead build it as a composite of smooth maps: (1) a smooth flow Φ : M × ℝ → M (here cos t • x + sin t • L x, via ContMDiff.codRestrict_sphere); (2) the section σ x := (equivTangentBundleProd I M 𝓘(ℝ,ℝ) ℝ).symm (zeroSection _ (TangentSpace I) x, ⟨0, (1:ℝ)⟩), smooth by contMDiff_equivTangentBundleProd_symm.comp (ContMDiff.prodMk (fun x ↦ contMDiff_zeroSection ℝ (TangentSpace I) x) contMDiff_const); (3) define ξ x := (tangentMap _ _ Φ (σ x)).2 — this typechecks because all TangentSpace fibers are defeq to the model space. Smoothness: (hΦ.contMDiff_tangentMap le_rfl).comp hσ after funext + TotalSpace.ext (h : proj = x).symm HEq.rfl (proj is Φ (x,0), equal to x only propositionally). To compute ξ: write σ x = tangentMap (fun t ↦ (x,t)) ⟨0,1⟩ (rw [tangentMap_prod_right]; rfl), fold with ← Function.comp_apply + ← tangentMap_comp, then change mfderiv 𝓘(ℝ,ℝ) 𝓘(ℝ,E) c 0 (1:ℝ) = _; rw [mfderiv_eq_fderiv]; exact hasDerivAt.deriv. Gotchas: rw [mfderiv_comp_apply_of_eq ...] with a literal (0, 1) failed: 'not type-correct at implicit transparency', since (0,1) was elaborated in E × ℝ and not in TangentSpace; using anonymous-constructor points of TangentBundle avoids this. contMDiff_zeroSection takes explicit (𝕜 E) arguments AND returns ContMDiffAt at x, so use it as fun x ↦ contMDiff_zeroSection ℝ _ x. Real.contDiff_cos needs import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv.