Using hypothesis with definition

Stream: new members

[Jelmer Firet]

Suppose I have

let g : ℕ → ℕ := λ i, if f i = m then f n else f i,

How can I then later use this to rewrite a hypothesis

g i = ...

to the definition of g i so I can then apply split_ifs?

Both

unfold g
unfold (g i)

Don't seem to work.

[Eric Wieser]

dsimp only [g] at h should work

[Jelmer Firet]

Thanks