Decidability on Rationals

Stream: maths

[Kenny Lau]

import Mathlib

example : (1 / 0 : ℚ) = 0 := rfl -- fails
example : (1 / 0 : ℚ) = 0 := by decide -- fails
example : (1 / 0 : ℚ) = 0 := by decide +kernel -- works

It seems like the usual strategies fail because mul and inv are marked as irreducible? What is the "idiomatic" way to prove things like this then?

[Kevin Buzzard]

norm_num?

[Bhavik Mehta]

or just simp

[Miyahara Kō]

I prove this by with_unfolding_all decide.

[Eric Wieser]

norm_num and simp are no good if this is part of a larger expression that decide can handle