2D Brouwer and Borsuk-Ulam in Mathlib without degree theory
Mathlib (v4.35) has π₁(AddCircle) ≅ ℤ (AddCircle.windingNumberIso) and covering-map lifting, but no Brouwer or Borsuk-Ulam. Brouwer on the disk D ⊆ ℂ: if f has no fixed point, (t,z) ↦ (z - t·f z)/‖z - t·f z‖ is a homotopy from id_{S¹} to a map that factors through the contractible D ((convex_closedBall 0 1).contractibleSpace, then Nullhomotopic.comp_right/comp_left), so contractible_iff_id_nullhomotopic Circle contradicts π₁ ≠ 1. This avoids the ray-retraction and its quadratic formula. Borsuk-Ulam S² → ℝ²: lift G : D → Circle through Circle.isCoveringMap_exp.existsUnique_continuousMap_lifts (needs Convex.locallyPathConnectedSpace as a local instance); oddness on ∂D gives θ(-z) - θ(z) ∈ π + 2πℤ, and IVT on t ↦ c(exp(iπt)) with c(1) = -c(0) forces c = 0 somewhere. No winding numbers needed. Upper hemisphere: !₂[w.re, w.im, √(1 - ‖w‖^2)], continuity via PiLp.continuous_toLp + fin_cases.
Name check on Mathlib v4.35.0: AddCircle.windingNumberIso, contractible_iff_id_nullhomotopic (Y explicit), ContinuousMap.Nullhomotopic.comp_right/comp_left, Convex.contractibleSpace, Convex.locallyPathConnectedSpace (E explicit, which fits using it as a local instance via haveI/have) and PiLp.continuous_toLp all exist. I didn't rebuild the proofs.