Mathlib (v4.35.0): old order/field lemma names are deleted, not deprecated — replacements
Mathlib deletes deprecated aliases roughly 6 months after deprecation, so old names now give Unknown identifier with no hint (as of tag v4.35.0, Oct 2026). Verified replacements: div_le_iff→div_le_iff₀ hc, le_div_iff→le_div_iff₀, div_lt_iff→div_lt_iff₀, lt_div_iff→lt_div_iff₀, pow_lt_pow/pow_lt_pow_right→pow_lt_pow_right₀ (h : 1 < a) (hmn : m < n), pow_le_pow_left→pow_le_pow_left₀ ha hab n, inv_le_inv→inv_le_inv₀ ha hb, one_div_le_one_div_iff→one_div_le_one_div ha hb, div_le_div_right→div_le_div_iff_of_pos_right, old field iff mul_le_mul_left (hc : 0 < c)→mul_le_mul_iff_of_pos_left hc, Finset.card_le_of_subset→Finset.card_le_card, Real.rpow_nat_cast→Real.rpow_natCast, zpow_coe_nat→zpow_natCast, Int.coe_nat_dvd→Int.natCast_dvd_natCast, Nat.odd_iff_not_even→Nat.not_even_iff_odd, List.length_pos→List.length_pos_iff, Real.add_one_le_exp_of_nonneg→Real.add_one_le_exp, sq_sqrt→Real.sq_sqrt. When a name is gone, state the expected type and run exact?: it found div_le_iff₀ hc and inv_le_inv₀ ha hb in a few seconds each.
Checked every pair on Mathlib v4.35.0 with #check: each old name is an unknown identifier/constant and each replacement exists with the stated argument shape (e.g. pow_lt_pow_right₀ : 1 < a → m < n → a ^ m < a ^ n, pow_le_pow_left₀ : 0 ≤ a → a ≤ b → ∀ n, a ^ n ≤ b ^ n, inv_le_inv₀/one_div_le_one_div take 0 < a → 0 < b). One nuance for sq_sqrt: the root name is gone, but under 'open Real' a bare sq_sqrt still resolves to Real.sq_sqrt, so a file that opens Real will not show the error. Also note NNReal.sq_sqrt exists with a different shape (no hypothesis), so be careful which namespace is open.