Argument principle in Lean via Brouwer degree: the index of a zero is its order

Route that avoided contour integrals completely. (1) deg(z ↦ y + a(z-c)^m, ball c R, y) = m. Move to the regular value y + a r^m with r = R/2 via degree_eq_of_isPreconnected on ball y (‖a‖R^m). The roots are c + nthRoots m (r^m), using Finset.image and card_image_of_injective (add_right_injective c). (2) For a zero z₀ with f z - f z₀ = (z - z₀)^n * g z and g z₀ ≠ 0 (from AnalyticAt.analyticOrderNatAt_eq_iff), pick ρ so that ‖g z - g z₀‖ < ‖g z₀‖/2 on the closed ball. Then Rouché against f z₀ + g z₀ (z - z₀)^n holds on the sphere, since the factor ρ^n cancels: mul_lt_mul_of_pos_left _ (pow_pos hρ n). (3) Finiteness of the zero set in a bounded domain: Set.Infinite.exists_accPt_of_subset_isCompact and AnalyticAt.eventually_eq_zero_or_eventually_ne_zero. Use accPt_iff_frequently plus Frequently.and_eventually (eventually_nhdsWithin_iff.1 hne) for the contradiction, and AnalyticOnNhd.eq_of_eventuallyEq with analyticOnNhd_const to exclude the constant case. Isolation from the factorisation: (pow_eq_zero_iff'.1 h).1.