[Merged by Bors] - chore(Algebra/Order/GroupWithZero/Unbundled): resolving name inconsistencies

[FR-vdash-bot]

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

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

Statement	New name	Old name
a * c ≤ b * d	mul_le_mul_of_nonneg	mul_le_mul_of_le_of_le
	mul_le_mul_of_nonneg'	mul_le_mul (still there)
a * c < b * d	mul_lt_mul_of_le_of_lt_of_pos_of_nonneg	mul_lt_mul_of_pos_of_nonneg (still there)
	mul_lt_mul_of_le_of_lt_of_nonneg_of_pos / mul_lt_mul_of_nonneg_of_pos'	mul_lt_mul_of_le_of_le' / mul_lt_mul' (still there)
	mul_lt_mul_of_lt_of_le_of_nonneg_of_pos	mul_lt_mul_of_nonneg_of_pos (still there)
	mul_lt_mul_of_lt_of_le_of_pos_of_nonneg / mul_lt_mul_of_pos_of_nonneg'	mul_lt_mul_of_le_of_lt' / mul_lt_mul (still there)
	mul_lt_mul_of_pos	mul_lt_mul_of_pos_of_pos
	mul_lt_mul_of_pos'	mul_lt_mul_of_lt_of_lt'
	(Left.)mul_lt_mul_of_nonneg	mul_lt_mul'' (still there)
	Right.mul_lt_mul_of_nonneg
a * b < 0 → 0 ≤ b → a < 0	(Left.)neg_of_mul_neg_left	neg_of_mul_neg_left / Left.neg_of_mul_neg_right
	Right.neg_of_mul_neg_left	Right.neg_of_mul_neg_right
a * b < 0 → 0 ≤ a → b < 0	(Left.)neg_of_mul_neg_right	neg_of_mul_neg_right / Left.neg_of_mul_neg_left
	Right.neg_of_mul_neg_right	Right.neg_of_mul_neg_left

Lines 304 - 321 and 476 - 495 were just moved together.

Some variable names are changed to be consistent with the rest of the file.

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

---

Split from #9249

Zulip

[YaelDillies]

I appreciate the effort. However your new names seem unnecessarily long (I know it gives more consistency, but the length really is unwieldy). Here are some guidelines:

• op_rel_op_of_rel_of_rel should just be op_rel_op
• _of_pred_of_pred can simply be _of_pred

This makes your table look like this

Statement	New name	Old name
a * c ≤ b * d	mul_le_mul_of_nonneg	mul_le_mul_of_le_of_le
	mul_le_mul_of_nonneg'	mul_le_mul (still there)
a * c < b * d	mul_lt_mul_of_le_of_lt_of_pos_of_nonneg	mul_lt_mul_of_pos_of_nonneg
	mul_lt_mul_of_le_of_lt_of_nonneg_of_pos	mul_lt_mul_of_le_of_le' / mul_lt_mul' (still there)
	mul_lt_mul_of_lt_of_le_of_nonneg_of_pos	mul_lt_mul_of_nonneg_of_pos
	mul_lt_mul_of_lt_of_le_of_pos_of_nonneg	mul_lt_mul_of_le_of_lt' / mul_lt_mul (still there)
	mul_lt_mul_of_pos	mul_lt_mul_of_pos_of_pos
	mul_lt_mul_of_pos'	mul_lt_mul_of_lt_of_lt'
	(Left.)mul_lt_mul_of_nonneg	mul_lt_mul'' (still there)
	Right.mul_lt_mul_of_nonneg
a * b < 0 → 0 ≤ b → a < 0	(Left.)neg_of_mul_neg_left	neg_of_mul_neg_left / Left.neg_of_mul_neg_right
	Right.neg_of_mul_neg_left	Right.neg_of_mul_neg_right
a * b < 0 → 0 ≤ a → b < 0	(Left.)neg_of_mul_neg_right	neg_of_mul_neg_right / Left.neg_of_mul_neg_left
	Right.neg_of_mul_neg_right	Right.neg_of_mul_neg_left

There are still a few lines that are not great (eg mul_lt_mul_of_lt_of_le_of_nonneg_of_pos/mul_lt_mul_of_lt_of_le_of_nonneg_of_pos), but it's already much better.

[YaelDillies]

Could you keep mul_lt_mul_of_pos_of_nonneg/mul_lt_mul_of_nonneg_of_pos as aliases of the new names? I think they are still somewhat not ambiguous

[YaelDillies]

Thanks. This is now definitely an improvement.

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style