Brouwer degree deg(F,Ω,y) in Lean/Mathlib: measure-free definition plus truncation trick

Measure-free definition that works well: IsDegree F Ω y d := ∃ δ > 0, ∀ G, ContDiff ℝ ∞ G → (∀ x ∈ closure Ω, ‖G x - F x‖ < δ) → ∀ y', ‖y'-y‖ < δ → (y' regular for G on Ω) → ∑ᶠ x ∈ {x | x ∈ Ω ∧ G x = y'}, sign det DG x = d, and degree := if h : ∃ d, IsDegree .. then h.choose else 0. Uniqueness only needs a smooth approximant (Tietze ContinuousMap.exists_restrict_eq for finite-dim E, then Continuous.exists_contDiff_dist_le_of_forall_mem_ball_dist_le with the uniform-continuity modulus on cthickening 1 (closure Ω)) and a regular value (Sard: addHaar_image_eq_zero_of_det_fderivWithin_eq_zero on {det = 0}, then a ball has positive measure). Haar measure is used only inside proofs (borelize E; Measure.addHaar). To move a whole-space homotopy-of-integrals lemma to an open Ω: truncate fun q => if q.2 ∈ Ω then f q else 0; if f vanishes on ℝ × (Ω \ K) with K ⊆ Ω compact, it is EventuallyEq to f (near ℝ × Ω) or to 0 (near ℝ × Kᶜ). So ContDiff and fderiv transfer through ContDiffAt.congr_of_eventuallyEq / EventuallyEq.fderiv_eq, and integral_indicator finishes. Use Real.smoothTransition as the time reparametrisation so homotopies are defined for all t ∈ ℝ with values in [0,1].