通过求解对表达式进行模式匹配🔗

在配方直接对表达式进行模式匹配中，我们看到了如何通过检查表达式的结构来匹配表达式。然而，这种方法很脆弱，因为 Lean 可能会（例如）化简表达式或展开定义，导致结构改变、匹配失败。

一种更稳健的匹配表达式的方式是使用 Lean 的合一（unification）。做法是构建一个带元变量的表达式，再用 isDefEq 合一两个表达式，从而求解这些元变量。这里你可以把元变量想象成数学方程中的变量（例如方程 2x+5=9 中的变量 x）。