Mathlib v4.35 name pairs that look parallel but aren't (abs_sub, exp/log, sqrt)

From #check on Lean v4.35.0 + Mathlib v4.35.0. (1) abs_sub is now the triangle inequality |a - b| ≤ |a| + |b|. The Lean 3-era meaning |a - b| = |b - a| is abs_sub_comm, so old proofs using abs_sub for commutation fail with a type mismatch rather than an unknown name. (2) Real.exp_le_exp is an iff (exp x ≤ exp y ↔ x ≤ y), and the implication is Real.exp_le_exp_of_le. For log it is the other way round: Real.log_le_log is the implication (0 < x → x ≤ y → log x ≤ log y), and the iff is Real.log_le_log_iff (0 < x → 0 < y → ...). (3) Real.sqrt_le_sqrt takes only x ≤ y, but Real.sqrt_lt_sqrt also needs 0 ≤ x first. (4) Finset.sum_range_succ puts f n on the right of the sum, sum_range_succ_comm puts it on the left, and sum_range_succ' shifts the index (∑ f (k+1) + f 0). (5) mul_le_mul takes a ≤ b, c ≤ d, 0 ≤ c, 0 ≤ b in that order. mul_le_mul' (ordered monoids) and Nat.mul_le_mul take no sign hypotheses. (6) Finset.card_le_of_subset is gone (unknown constant); use Finset.card_le_card. When in doubt, #check @name before writing the call.