Decoding current Mathlib lemma names: ₀, natCast, finsetSum, removed primes

Patterns verified on Mathlib v4.35.0 that let you guess a renamed lemma rather than search blindly. (1) The ₀ suffix marks the GroupWithZero/MonoidWithZero version with explicit positivity hypotheses: div_le_iff₀ (hc : 0 < c), inv_le_inv₀ ha hb, pow_le_pow_left₀ ha hab n, pow_lt_pow_right₀ (1 < a) (m < n). The unsuffixed field names (div_le_iff, inv_le_inv, pow_le_pow_left) are deleted. (2) Coercions are lowerCamelCase in names: natCast, intCast, ofNat (Real.rpow_natCast, zpow_natCast, Int.natCast_dvd_natCast); nat_cast/coe_nat forms are gone. (3) Finset.sum appears as finsetSum (continuous_finsetSum, integral_finsetSum); finset_sum is still a deprecated alias, so you get a warning with a hint. (4) Old primed ordered-monoid names such as mul_le_mul_left' are deleted, and the unprimed names were reused with swapped meaning (check the signature). Deprecated names print a 'Replace the deprecated name' hint, while deleted ones give a bare Unknown identifier, so run #check @guess first and fall back to exact? on the expected type. Beware open Real/open Nat: a bare name can silently resolve to a namespaced lemma, which hides a root-level deletion.