Mathlib: mul_le_mul_left now means b*a ≤ c*a (ordered monoid), not the field iff
In current Mathlib (checked on v4.35.0), mul_le_mul_left and mul_le_mul_right were reused for the ordered-monoid lemmas, and the naming is the reverse of what you'd guess: mul_le_mul_right (h : b ≤ c) (a) : a * b ≤ a * c (this was mul_le_mul_left') and mul_le_mul_left (h : b ≤ c) (a) : b * a ≤ c * a (this was mul_le_mul_right'). So old proofs that use mul_le_mul_left hc for 0 < c → (c * a ≤ c * b ↔ a ≤ b) don't fail with an unknown identifier; they fail with a confusing type mismatch. For the iff with a positivity hypothesis, use mul_le_mul_iff_of_pos_left hc / mul_le_mul_iff_of_pos_right hc. For ℕ, Nat.mul_le_mul_left k h : k * m ≤ k * n keeps its old meaning. gcongr avoids the naming question entirely for monotonicity goals.
Confirmed on Mathlib v4.35.0 via #check: mul_le_mul_left : b ≤ c → ∀ a, b * a ≤ c * a [MulRightMono], mul_le_mul_right : b ≤ c → ∀ a, a * b ≤ a * c [MulLeftMono]; mul_le_mul_iff_of_pos_left/right are as stated, and Nat.mul_le_mul_left (k) : n ≤ m → k * n ≤ k * m. One addition: mul_le_mul_left' is now an unknown identifier (removed, not deprecated), so code using the primed names fails with 'Unknown identifier' rather than a type mismatch.
Further check on Mathlib v4.35.0: the swap is not limited to mul_le_mul_*. The additive and strict versions follow it: add_le_add_left : b ≤ c → ∀ a, b + a ≤ c + a and add_le_add_right : … a + b ≤ a + c (the reverse of the long-standing meaning); likewise mul_lt_mul_left/right and add_lt_add_left. Meanwhile the suffixed families keep the old reading, with the fixed operand on the left: mul_le_mul_of_nonneg_left : b ≤ c → 0 ≤ a → a * b ≤ a * c, mul_lt_mul_of_pos_left, mul_le_mul_iff_left (a) : a * b ≤ a * c ↔ b ≤ c, add_le_add_iff_left, sub_le_sub_left : a ≤ b → ∀ c, c - b ≤ c - a, mul_le_mul_left_of_neg. So 'left' means opposite things in the bare and the suffixed names; #check before use, or use gcongr.