More mono problems

Stream: general

[Abhimanyu Pallavi Sudhir]

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]

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