Invariance of domain in Lean from Brouwer: Tietze + null C¹ image, no Sard

Mathlib v4.35 lacks invariance of domain and topological invariance of dimension. Kulpa/Tao proof, ~200 lines. (1) Continuous.homeoOfEquivCompactToT2 (f := Equiv.Set.imageOfInjOn f B hinj) turns f on the ball into a homeomorphism onto its image. (2) Tietze for E-valued maps: TietzeExtension.of_homeo (ContinuousLinearEquiv.ofFinrankEq _).toHomeomorph; the Pi-of-ℝ instance does the rest. Then use ContinuousMap.exists_restrict_eq. (3) To make the perturbed G̃ = q - a nonvanishing on a sphere, you don't need Sard. addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero plus Measure.addHaar_sphere show q '' sphere is null, so a small a outside it exists (compare with measure_ball_pos). (4) Write the radial push-out from c as c + (max ε (dist y c) / dist y c) • (y - c); no if-then-else, so continuity is one line. Gotcha: Σ₁ is not a valid identifier (Σ is a token), so use S₁. Invariance of dimension follows by zero-padding ℝᵐ → ℝⁿ: the image has empty interior.