a / b ≤ c simp-normal form

Stream: mathlib4

[Violeta Hernández]

#34443 came across something weird. The simp-normal form of a / b ≤ c is a ≤ c * b, via docs#div_le_iff_le_mul. Likewise, a - b ≤ c simplifies to a ≤ c + b via docs#tsub_le_iff_right. However, the 2 × 3 variants of these theorems, using < or moving the division to the RHS, are not tagged simp.

[Violeta Hernández]

Should all of these be tagged simp? Or perhaps none of these?

[Jovan Gerbscheid]

This sounds very similar to #mathlib4 > Should `Set.diff_subset_iff`/`sdiff_le_iff` be `@[simp]`?

[Violeta Hernández]

The issue isn't about the additive/multiplicative variants being different, rather, the issue is that the different variants aren't consistently tagged

[Eric Wieser]

What breaks if you try tagging them as simp?

[Kevin Buzzard]

The additivised version sub_le_iff_le_add of div_le_iff_le_mul doesn't seem to be tagged simp either?