chore: use suffix ₚ for lemmas with positivity assumptions, create aliases

[FR-vdash-bot]

This PR uses the suffix ₚ on some lemmas which assume positivity.

This allows the names to be clearly distinguished from versions that do not require positivity assumptions, and also do not become too long.

I've kept most of the previous names (short names and long names suffixed with _of_pos or _of_nonneg) as aliases, but not for wrong names and confusing names.

Due to name conflicts, some similar lemmas have dissimilar names before this PR:

theorem mul_lt_mul_of_nonneg_of_pos [PosMulMono α] [MulPosStrictMono α]
    (h₁ : a < b) (h₂ : c ≤ d) (a0 : 0 ≤ a) (d0 : 0 < d) : a * c < b * d
theorem mul_lt_mul_of_le_of_lt' [PosMulMono α] [MulPosStrictMono α]
    (h₁ : a < b) (h₂ : c ≤ d) (b0 : 0 ≤ b) (c0 : 0 < c) : a * c < b * d

If there is a better way to resolve name conflicts, please feel free to comment.

---

Ported from leanprover-community/mathlib3#16523

[j-loreaux]

These statements are not identical. mul_lt_mul holds in a StrictOrderedSemiring. Of course, the lemma you are aliasing holds in more generality, but it also makes Lean work harder to synthesize type classes. I am dubious whether we are actually okay with this unless I see a !bench showing the effect is negligible.

I've highlighted mul_lt_mul, but I suspect the same is true for many of the aliases you have in this PR.

[j-loreaux]

I've opened a Zulip thread because I think this is a somewhat significant change to our naming conventions and as such I've marked this as RFC.

[FR-vdash-bot]

!bench

[leanprover-bot]

Here are the benchmark results for commit 7559b09.
There were no significant changes against commit fb3fd7c.