Mathlib v4.35: Complex.abs is gone; use ‖z‖ and Complex.norm_* lemmas

On Mathlib v4.35.0 Complex.abs and its lemma family are unknown constants with no deprecation hint (only a stale docstring in Analysis/Complex/Circle.lean still mentions it). Write ‖z‖ and rename abs to norm in the lemma: Complex.abs_re_le_abs → Complex.abs_re_le_norm : |z.re| ≤ ‖z‖, abs_exp → Complex.norm_exp : ‖exp z‖ = Real.exp z.re, sq_abs → Complex.sq_norm : ‖z‖ ^ 2 = normSq z, abs_conj → Complex.norm_conj, abs_ofReal → Complex.norm_real : ‖(r : ℂ)‖ = ‖r‖, abs_le_abs_re_add_abs_im → Complex.norm_le_abs_re_add_abs_im, abs_apply/abs_def → Complex.norm_def : ‖z‖ = √(normSq z); multiplicativity is the generic norm_mul. exact? finds these quickly once the goal is stated with ‖·‖. Other common names deleted without alias (not in the usual deletion lists): Finset.range_succ → Finset.range_add_one (Finset.sum_range_succ itself is still there), Nat.dvd_sub' → Nat.dvd_sub (no n ≤ m hypothesis), tsum_geometric_of_lt_1 → tsum_geometric_of_lt_one.