From a Mathlib TangentBundle section of the sphere to an ambient vector field (and the errors on the way)

To turn a section ξ x : TangentSpace (𝓡 n) x of the unit sphere into a continuous E-valued field w x ⟂ x, use the tangent map of the inclusion: ambient p := (tangentBundleModelSpaceHomeomorph 𝓘(ℝ,E) (tangentMap (𝓡 n) 𝓘(ℝ,E) ((↑) : sphere (0:E) 1 → E) p)).2. It equals mfderiv ... x ξ by rfl. It is continuous via ContMDiff.continuous_tangentMap (contMDiff_coe_sphere (m := 1)) le_rfl. It is orthogonal to x via range_mfderiv_coe_sphere (deprecated in favour of range_mvfderiv_subtypeVal, but it matches tangentMap's mfderiv) and Submodule.mem_orthogonal_singleton_iff_inner_right, and it is injective via mfderiv_coe_sphere_injective. Gotchas: (1) contMDiff_coe_sphere.continuous_tangentMap fails with 'unknown constant' / 'Function.continuous_tangentMap'. The lemma has implicit args and is stated pointwise, so call ContMDiff.continuous_tangentMap (...) explicitly, and import Mathlib.Geometry.Manifold.ContMDiffMFDeriv. (2) 'typeclass instance problem is stuck Fact (finrank ℝ E = ?m + 1)' means you must pass (n := n) to every sphere lemma. (3) No instance Fact (finrank ℝ (EuclideanSpace ℝ (Fin 3)) = 2 + 1) is found; declare one with ⟨by simp⟩ and attribute [local instance]. (4) simp turns y ∈ sphere 0 1 into ‖y‖ = 1 inside dite conditions; use simp only [hy, ↓reduceDIte].