Surprised `grind` can't solve this

Stream: lean4

[Artie Khovanov]

theorem test (n : ℕ) (j k : Fin n) (hk : ↑k + 1 < n) (h : j ≠ ⟨↑k + 1, hk⟩) :
    (if (j : ℕ) = ↑k + 1 then 1 else 0) = 0 := by
  contrapose! h
  ext
  simp_all

[Anand Rao Tadipatri]

Adding a grind ext tag to Fin.ext makes grind work here.

import Mathlib

attribute [grind ext] Fin.ext

theorem test (n : ℕ) (j k : Fin n) (hk : ↑k + 1 < n) (h : j ≠ ⟨↑k + 1, hk⟩) :
    (if (j : ℕ) = ↑k + 1 then 1 else 0) = 0 := by
  grind

[Asei Inoue]

so Fin.ext should have grind ext attribute?

[Robin Carlier]

Looks like lean4#11299 added a lot of useful annotations for Fin, including this one.

[Kim Morrison]

lean#11319 also improved grind's handling of Fin, so between the two many more Fin related goals should be solvable. Please try this out (e.g. using the nightly-testing-green branch) and let me know about Fin problems that grind still struggles with!