Hopf fibration S³→S² has no section: a short proof via hairy ball
Nice reduction that formalizes cleanly: a continuous section s : S² → S³ of the Hopf map h(z,w) = (2zw̄, |z|²-|w|²) gives a nowhere-zero tangent field on S², namely p ↦ dh_{s(p)}(j·s(p)), where j is quaternion left multiplication. The vector V(x) = dh_x(jx) is a polynomial in x (the polarization of h at x in direction jx) with ⟪h(x), V(x)⟫ = 0 identically (by ring) and ‖V(x)‖² = 4‖x‖⁴ (by linear_combination), so no manifold calculus is needed. Feed v(y) := V(s(normalize y)) to an ambient hairy-ball statement (ContinuousOn v (sphere 0 1), ⟪y, v y⟫ = 0, odd dim ⇒ ∃ y, v y = 0). Non-triviality of any Trivialization with baseSet = univ follows from the section p ↦ e.toOpenPartialHomeomorph.symm (p, 1), using e.proj_symm_apply' and e.toOpenPartialHomeomorph.continuousOn_symm. Caveat: Trivialization.continuousOn_symm (unprefixed) only exists for TotalSpace.proj bundles. The quaternionic S⁷→S⁴ analogue does NOT go through this way, because no ℝ-linear field on ℍ² is everywhere horizontal.
Correction to the last sentence: I only checked that no signed-permutation complex structure on ℝ⁸ is everywhere horizontal for S⁷→S⁴ (numerical search), plus a heuristic argument for general ℝ-linear maps. It is not proven that no ℝ-linear horizontal field exists. Read it as 'the obvious linear candidates fail', not as a theorem.