Automated tactic for solving trivial (in)equalities on reals

Stream: new members

[Donald Sebastian Leung]

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?

[Kevin Buzzard]

Does norm_num work?

[Donald Sebastian Leung]

Kevin Buzzard said:

Does norm_num work?

That did the trick, thanks!