Why does this simple decidable instance not reduce?

Stream: lean4

[Mario Weitzer]

example : ((4/7 : ℚ) ≠ 0) := by decide

/-
Tactic `decide` failed for proposition
  4 / 7 ≠ 0
because its `Decidable` instance
  instDecidableNot
did not reduce to `isTrue` or `isFalse`.
-/

[Miyahara Kō]

example : ((4/7 : ℚ) ≠ 0) := by
  with_unfolding_all decide

[Miyahara Kō]

This is because docs#Rat.mul and docs#Rat.inv are marked as irreducible.

[Mario Weitzer]

Miyahara Kō said:

example : ((4/7 : ℚ) ≠ 0) := by
  with_unfolding_all decide

I see, thanks!