mono: asserting side conditions

Stream: general

[Abhimanyu Pallavi Sudhir]

This is one error I can't fix in #835 -- see https://travis-ci.org/leanprover-community/mathlib/jobs/528542225

The error message states there is an ambiguity in using mono in line 466 as

abs (x - of r) * abs (of s) ≤ of (d / abs s / 2) * abs (of s)

can be reduced either to 0 ≤ abs (of s) | abs (x - of r) ≤ of (d / abs s / 2) or abs (of s) ≤ 0 | of (d / abs s / 2) ≤ abs (x - of r). It suggests that I assert a side condition -- so I tried writing mono using 0 ≤ abs (of s), but this gives two errors for the mono using ... line:

invalid begin-end expression, ',' expected

(all my brackets are closed, etc. -- I can't see what the problem is)

and for the exact le_of lt ... line:

sync

Perhaps I don't understand the syntax for mono using -- what am I doing wrong?

[Kevin Buzzard]

You're not posting the full error message, for one thing:

ambiguous match:

mul_mono_nonpos
0 ≥ abs (of s)
of (d / abs s / 2) ≤ abs (x - of r)

mul_mono_nonneg
0 ≤
  abs (of s)
abs (x - of r) ≤ of (d / abs s / 2)

Tip: try asserting a side condition to distinguish between the lemmas
state:
x y : ℝ*,
r s : ℝ,
hxr : is_st x r,
hys : is_st y s,
hs : s ≠ 0,
hxr' : ∀ (δ : ℝ), δ > 0 → abs (x - ↑r) < ↑δ,
hys' : ∀ (δ : ℝ), δ > 0 → abs (y - ↑s) < ↑δ,
h : ∃ (r s : ℝ), ↑r < abs x ∧ abs x < ↑s,
u : ℝ,
h' : ∃ (s : ℝ), ↑u < abs x ∧ abs x < ↑s,
t : ℝ,
_x : ↑u < abs x ∧ abs x < ↑t,
_fun_match : ↑u < abs x ∧ abs x < ↑t → is_st (x * y) (r * s),
hu : ↑u < abs x,
ht : abs x < ↑t,
d : ℝ,
hd : d > 0
⊢ abs (x - of r) * abs (of s) ≤ of (d / abs s / 2) * abs (of s)

And you're not revising for my exam, that's another thing ;-)

[Kevin Buzzard]

mono with 0 ≤ abs (of s), swap,  exact le_of_lt (hxr' _ (half_pos (div_pos hd (abs_pos_of_ne_zero hs)))),
        apply abs_nonneg,

seems to deal with it (you probably know what's going on better than I do with the swap and can fix things up better)

[Abhimanyu Pallavi Sudhir]

Ah, it's with -- I thought the keyword was using for some reason. Thanks.

[Kevin Buzzard]

I just hovered over mono and read the docs. For all I know it changed...

[Mario Carneiro]

that's a surprisingly helpful error message. Thanks Simon!