Radial extension x ↦ ‖x‖ • f(‖x‖⁻¹ • x) needs no case split in Lean

To extend a map f, given only on the unit sphere, to the closed ball, define radialExt f x := ‖x‖ • f (‖x‖⁻¹ • x). Lean's 0⁻¹ = 0 makes the value at 0 equal to 0 • f 0 = 0, so no dite or normalize with a proof argument is needed. ContinuousOn on Icc 0 1 ×ˢ closedBall 0 1, for a homotopy H that is continuous with norm 1 on Icc 0 1 ×ˢ sphere 0 1, splits into two cases. At points with x ≠ 0, use ContinuousWithinAt.comp_of_preimage_mem_nhdsWithin (f := fun q => (q.1, ‖q.2‖⁻¹ • q.2)), with the eventual-membership filter fact that q.2 ≠ 0 nearby. You must pass (f := ...), otherwise unification picks Prod.mk p.1. At x = 0, use ‖ext q‖ ≤ ‖q.2‖, tendsto_zero_iff_norm_tendsto_zero and squeeze_zero'. Then sphere-map degree is just deg(radialExt f, ball 0 1, 0). For fixed-point-free f the segment (1-t) f x - t x never vanishes, because taking norms forces t = 1/2. That gives deg = (-1)^n with no normalisation.