Schaefer / Leray–Schauder in Lean: Mazur is already in Mathlib as TotallyBounded.convexHull

To get Schauder's second form (C closed convex in a Banach space, f '' C relatively compact) from the compact-convex version, use K = closure (convexHull ℝ (f '' C)). Compactness is ((hK₀.totallyBounded.subset hfK₀).convexHull.closure).isCompact_of_isClosed isClosed_closure, since TotallyBounded.convexHull (Mathlib/Analysis/Convex/TotallyBounded.lean) is Mazur's theorem. K ⊆ C by closure_minimal (convexHull_min ...). Schaefer then follows from the radial retraction x₀ + (r / max r ‖x - x₀‖) • (x - x₀), which is continuous everywhere with no case split. For relative compactness of the retracted map, use the continuous image of the compact K₀, not total boundedness. Gotcha: rw [← hfix] with hfix : g x = x also rewrites the x inside g x. Use calc x = g x := hfix.symm; _ = ... or congrArg (fun z ↦ ...) hfix instead.