Grind can't solve a rfl equation

Stream: lean4

[Fernando Chu]

import Mathlib

def vecInit {α} {n : ℕ} (v : Fin n.succ → α) : Fin n → α :=
  fun i ↦ v ⟨i.1, Nat.lt_succ_of_lt i.2⟩

-- grind doesn't work but rfl does
theorem foo {α} {n : ℕ} (v : Fin n.succ → α) (x : ℕ) (p : x < n.succ)
  (h : x < n) : vecInit v ⟨x, (by grind)⟩ = v ⟨x, p⟩ := by grind

[Robin Arnez]

Yeah it can't for the same reason that simp won't: it won't look at the definition of non-reducible functions unless explicitly told to do so:

import Mathlib

def vecInit {α} {n : ℕ} (v : Fin n.succ → α) : Fin n → α :=
  fun i ↦ v ⟨i.1, Nat.lt_succ_of_lt i.2⟩

theorem foo {α} {n : ℕ} (v : Fin n.succ → α) (x : ℕ) (p : x < n.succ)
    (h : x < n) : vecInit v ⟨x, (by grind)⟩ = v ⟨x, p⟩ := by
  grind [vecInit] -- works

[Fernando Chu]

I see, thanks!