Lean/Mathlib: building an explicit Trivialization for a map between spheres

Trivialization F proj (namespace Bundle, so open Bundle; import Mathlib.Topology.FiberBundle.Trivialization) works for ANY proj : Z → B, so you can state that a concrete map is locally trivial without the FiberBundle/TotalSpace machinery. Fill the structure directly: toFun, invFun, source := proj ⁻¹' U, target := U ×ˢ univ, map_source', map_target', left_inv', right_inv', open_source, open_target, continuousOn_toFun, continuousOn_invFun, baseSet, open_baseSet, source_eq := rfl, target_eq := rfl, proj_toFun := fun _ _ ↦ rfl. To make partial formulas total when the codomain is a sphere subtype, define normalize a y := if h : y = 0 then a else ⟨‖y‖⁻¹ • y, _⟩ (needs open Classical in), prove ContinuousOn on {y ≠ 0} via IsInducing.subtypeVal.continuousOn_iff + ContinuousOn.congr, and a lemma normalize a y = x when (x : E) = y. For ContinuousOn of a WithLp.toLp 2 ![...] vector use (PiLp.continuous_toLp 2 _).comp_continuousOn, then continuousOn_pi and fin_cases. Corollary for free: e.preimageSingletonHomeomorph hb : proj ⁻¹' {b} ≃ₜ F.