Decision procedure for equations over fields

Stream: new members

[Benjamin]

Is there a tactic to automatically prove goals like the following?

example (n k : ℚ) (hn : n ≠ 0) (hk : k ≠ 0) : n / (n * k) - 1 / k = 0

[Michael Stoll]

field_simp?

[Benjamin]

Thanks!

[Michael Rothgang]

Perhaps you also want to call ring afterwards.

[Ruben Van de Velde]

In this case simp cleans up everything, but yeah, in general ring is a good next step