grind failure and Classical

Stream: mathlib4

[Yannick Seurin]

Does anyone know why grind fails here?

example (q : Nat) (h : q ≠ 0) : 1 ≤ q := by
  grind

example (q : Nat) (h : q ≠ 0) : 1 ≤ q := by
  have := Classical.propDecidable
  grind
/-
(kernel) application type mismatch
  of_decide_eq_true (Eq.refl true)
argument has type
  true = true
but function has type
  decide (1 ≤ 1) = true → 1 ≤ 1
-/

[Eric Wieser]

If you edit the above to use Nat instead of ℕ and remove the import, I'll move to this to #lean4 for you

[Yannick Seurin]

Done!