## Stream: general

### Topic: More mono problems

#### Abhimanyu Pallavi Sudhir (May 07 2019 at 10:14):

I still can't get mono to work in #835 -- in Line 467 here, I get the error:

/home/travis/build/leanprover-community/mathlib/src/data/real/hyperreal.lean:467:14: error: type mismatch at application
le_of_lt (hxr' (d / abs s / 2) (half_pos (div_pos hd (abs_pos_of_ne_zero hs))))
term
hxr' (d / abs s / 2) (half_pos (div_pos hd (abs_pos_of_ne_zero hs)))
has type
abs (x - ↑r) < ↑(d / abs s / 2)
but is expected to have type
abs (x - of r) * abs (of s) < of (d / abs s / 2) * abs (of s)


This doesn't seem to make much sense, since I've already performed mono with 0 ≤ abs (of s) to simplify the goal to abs (x - ↑r) < ↑(d / abs s / 2).

#### Abhimanyu Pallavi Sudhir (May 07 2019 at 10:35):

Ah, never mind, I can do this without mono.

Last updated: May 13 2021 at 17:42 UTC