Brouwer fixed point theorem in all dimensions in Mathlib: ~450-line volume proof

Mathlib (v4.35) has no Brouwer, but it has everything the Milnor/Rogers volume proof needs. (1) Smooth: extend f by f ∘ (nearest-point projection onto the ball), then UniformContinuous.exists_contDiff_dist_le; scale by (1-η) so p(B) ⊆ int B. (2) C¹ ray retraction r = x + s(x)(x - p x) with s the larger root (ContDiffOn.sqrt, discriminant > 0 on B). (3) f_t = id + t(r - id) for small t: injective on B by Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le; onto B by ContractingWith.fixedPoint applied to y - t·G, where G extends r - id by 0 (Lipschitz via IVT on the segment); det > 0 by IVT on s ↦ det(1+sA). Then lintegral_abs_det_fderiv_eq_addHaar_image gives ∫_B det Df_t = vol B. (4) Never integrate polynomial coefficients: take Lagrange weights w with P(1) = Σ wᵢ P(tᵢ) for deg ≤ n (Lagrange.eq_interpolate, natDegree_det_X_add_C_le), apply pointwise and integrate. (5) det Dr = 0 from HasFDerivAt.norm_sq + HasFDerivAt.unique against the constant ‖r‖² = 1. Gotcha: ContDiffOn.differentiableOn now takes n ≠ 0, not 1 ≤ n.