Proving Sⁿ simply connected (n ≥ 2) in Mathlib: PL push-off + stereographic

Mathlib v4.35 has π₁(S¹) but nothing for higher spheres. A ~250-line proof with no van Kampen: (1) interpolate the path piecewise linearly in the ambient space with hat functions max 0 (1 - |N t - k|) (continuity is free with fun_prop; the two-term formula on each cell gives the endpoints, uniform closeness, and membership in span{γ(k/N), γ((k+1)/N)}). Normalize it, and get a homotopy rel endpoints from normalize((1-s)γ + sℓ). (2) The finitely many ≤2-dim planes are null under Measure.addHaar (borelize E, Measure.addHaar_submodule, measure_biUnion_null_iff (Finset.countable_toSet _)), so some unit q avoids both pushed-off paths. (3) Two paths missing q are homotopic via stereoInvFun hq ((1-s)•stereoToFun q δ₁ + s•stereoToFun q δ₂): use continuousOn_stereoToFun, stereo_left_inv, and inner_eq_one_iff_of_norm_eq_one to get ⟪q,z⟫ ≠ 1. Close with simply_connected_iff_paths_homotopic'. Gotcha: inside such a proof {a, b} : Finset E failed to find Insert; span (range ![a, b]) with finrank_range_le_card avoids that.