Zulip Chat Archive

Stream: general

Topic: More mono problems


view this post on Zulip 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).

view this post on Zulip 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