Zulip Chat Archive

Stream: new members

Topic: Automated tactic for solving trivial (in)equalities on reals


view this post on Zulip Donald Sebastian Leung (Feb 25 2020 at 07:06):

So I want to prove the following goal: (1 : ℝ) / 10 ≠ 1. Is there any automated tactic (in stdlib/mathlib) capable of solving the following goal immediately, or would I have to prove it from first principles?

view this post on Zulip Kevin Buzzard (Feb 25 2020 at 07:11):

Does norm_num work?

view this post on Zulip Donald Sebastian Leung (Feb 25 2020 at 08:20):

Kevin Buzzard said:

Does norm_num work?

That did the trick, thanks!


Last updated: May 11 2021 at 00:31 UTC