le_mul_of_one_le_of_le' for reals

Stream: Is there code for X?

[Artem Vasilev]

Is there something like this in mathlib?

lemma le_mul_of_one_le_of_le' {α} {a b c: α} [ordered_semiring α] (ha : 1 ≤ a) (hbc : b ≤ c) (hb : 0 ≤ b) :
b ≤ a * c := calc
b = 1 * b : (one_mul b).symm
... ≤ a * c : mul_le_mul ha hbc hb (zero_le_one.trans ha)

There is a version of this lemma for [covariant_class α α (*) (≤)], but I want to apply it to reals.
Is [ordered_semiring α] the best scope for it?

[Floris van Doorn]

The ordered refactor hasn't hit rings/fields yet, so that's why the lemmas are less complete for them. With the current classes ordered_semiring is indeed the best class for this.

[Floris van Doorn]

And to answer your question: no this doesn't seem to be there yet. I thought there would be a variant where b and c are identical, but I also cannot find that version.

[Floris van Doorn]

Oh, the version where b and c are identical is docs#le_mul_of_one_le_left.

[Artem Vasilev]

Thank you! So

lemma le_mul_of_one_le_of_le' {α} {a b c: α} [ordered_semiring α] (ha : 1 ≤ a) (hbc : b ≤ c) (hb : 0 ≤ b) :
b ≤ a * c := (le_mul_of_one_le_left hb ha).trans (mul_le_mul_of_nonneg_left hbc (zero_le_one.trans ha))

works for me. Is there a demand for PRing individual lemmas like this one?

[Scott Morrison]

Yes, a PR is good, thanks!