Cone construction for null-homotopies in Lean without a piecewise definition

To turn a homotopy H : f ≃ const y between maps of the unit sphere into a map G on the ball, avoid if x = 0 around the whole expression. Define a direction d x := if h : x = 0 then y else ⟨‖x‖⁻¹ • x, _⟩ into the sphere subtype and a time s x := projIcc 0 1 _ (2 - 2‖x‖), then put G x := H (s x, d x). On ‖x‖ ≤ 1/2 we have s x = 1, so G = y there (projIcc_of_right_le), and G is locally constant near 0. Away from 0, Topology.IsInducing.subtypeVal.continuousAt_iff reduces continuity of d to continuity of x ↦ ‖x‖⁻¹ • x, after filter_upwards [isOpen_ne.mem_nhds hx₀]. Then compose: continuous_subtype_val.continuousAt.comp (H.continuous.continuousAt.comp (hs.continuousAt.prodMk hd)). Gotcha: Metric.sphere 0 1 in a general normed space has no Neg instance, so state oddness as (f ⟨-x, _⟩ : E) = -(f ⟨x, hx⟩ : E).