Using mul_lt_one_of_le_of_lt for reals

Stream: new members

[Brendan Seamas Murphy]

I have a goal a * b < 1 where I know 0 <= a <= 1 and 0 <= b < 1. I wanted to conclude using mul_lt_one_of_le_of_lt, but I get the error invalid apply tactic, failed to synthesize type class instance for covariant_class ℝ ℝ has_mul.mul has_lt.lt. I've see these covariant_class things before in lemmas but this is the first time I've run into an issue with them. It seems like the issue is that if c <= 0 then x < y does not imply c * x < c * y. What's the easiest way to apply (something equivalent to) this lemma in my situation?

[Yaël Dillies]

docs#mul_lt_one_of_nonneg_of_lt_one_left

[Yaël Dillies]

Sorry, algebraic order lemmas are a bit of a maze!

[Brendan Seamas Murphy]

thanks!

[Damiano Testa]

Btw, the covariant_class you mention is the statement that multiplication by any given real on the left is strictly monotone.

The has_mul field tells you which operation to use and the has_lt which relation. The vast majority of covariant classes in mathlib use + or * as operation on the left, their swap for operations on the right, and ≤ or < for monotone/strictly monotone.

The first two fields that are both ℝ in your case, would be superfluous, if it were easy to deduce from the operation which type is acting on which type.

[Damiano Testa]

Btw, if you want to use fancier covariant typeclasses, this also works:

import data.real.basic

example {a b : ℝ} (a0 : 0 ≤ a) (a1 : a ≤ 1) (b0 : 0 ≤ b) (b1 : b < 1) : a * b < 1 :=
zero_lt.mul_lt_of_le_of_lt_one' a1 b1 b0 zero_lt_one

Note that docs#zero_lt.mul_lt_of_le_of_lt_one' is a lemma that is not real-specific.
Edit: I see now that Yaël's suggestion is also not real-specific! What I meant is that it does not use the ordered_semiring typeclass.