mathlib

mathlib copied to clipboard

I don't know anything about the implementation of norm_num, but in my ideal world, these lemmas would entirely be handled by norm_num.

Originally posted by @Smaug123 in https://github.com/leanprover-community/mathlib/issues/8002#issuecomment-1158021087

There are a few lemmas in the Bertrand's postulate proof that bound certain expressions using sqrt, log, exp. It would be nice if ~~norm_num~~ some tactic could handle these.

In particular, if we want to prove a goal of the form e1 < e2, where e1 and e2 are compositions of continuous functions (or are at least continuous at their arguments) applied to rationals, then in principle, we can generate finer and finer approximations of both expressions until eventually we can prove the goal by the triangle inequality.