Does lean have syntactic unification of first-order terms

Stream: new members

[Eric Taucher]

Does Lean (3) or Lean4 have/implement the unification algorithm for first-order terms? (ref)

I know there is unification modulo definitional equality (ref), which is not what I seek.

[Marcus Rossel]

Maybe Section 2.2 of https://arxiv.org/pdf/1505.04324.pdf could help you (I'm not well versed in this topic).