How to spell `coe` in Lean4

Stream: mathlib4

[Chris Hughes]

How should we now state lemma about things like (coe : s -> A) '' t. Should this be written Subtype.val '' t now, or is there a way without having to remember the name of the coercion?

[Gabriel Ebner]

((↑) : s → A)

[Chris Hughes]

Is there an import this depends on? It seems to work in one file I'm working on but not the other

[Chris Hughes]

Yes, Mathlib.Tactic.Coe