等式关系。它只有一条引入规则 Eq.refl。 使用 a = b 作为 Eq a b 的记法。 等式的一项基本性质是它构成等价关系。

不过，等式远不只是一种等价关系。它还具有一项重要性质：每个断言都尊重这种等价，即可以替换相等的表达式而不改变真值。 也就是说，给定 h1 : a = b 和 h2 : p a，可构造 p b 的证明，所用替换为 Eq.subst h1 h2。 示例：

第二种写法中的三角符号是建立在 Eq.subst 和 Eq.symm 之上的宏，可输入 \t 得到它。 更多信息：等式

标识符中记法的约定：

• 标识符中 = 的推荐拼写是 eq。

Eq.refl.{u_1} {α : Sort u_1} (a : α) : a = a

term ::= ...
    | term = term

命题等式通常用中缀运算符 = 表示。

rfl : a = a 是等式类型唯一的构造子。它与 Eq.refl 相同，只不过隐式而非显式地接受 a。

这一定理比初看上去更强，因为尽管其陈述是 a = a，Lean 也会接受与该类型定义相等的任何类型。例如，在 Lean 中，2 + 2 = 4 可用 rfl 证明，因为等式两边在定义等价意义下相同。

等式具有对称性：若 a = b，则 b = a。

因为它位于 Eq 命名空间中，若有变量 h : a = b，则可用 h.symm 作为 Eq.symm h 的简写来证明 b = a。

更多信息：等式

等式具有传递性：若 a = b 且 b = c，则 a = c。

因为它位于 Eq 命名空间中，若有变量或表达式 h₁ : a = b 和 h₂ : b = c，则可用 h₁.trans h₂ : a = c 作为 Eq.trans h₁ h₂ 的简写。

更多信息：等式

等式的替换原理。若 a = b 且 P a 成立，则 P b 也成立。这里依惯例用名称 motive 表示 P；若无法正确推断它，可用例如 Eq.subst (motive := fun x => x < 5) 显式指定。

这一定理是 rw 策略的底层机制；该策略本质上是一种精巧算法，用于寻找合适的 motive 实参，从而有效应用本定理，将目标或假设中出现的 a 替换为 b。

更多信息：等式

沿类型等式进行强制转换。若 h : α = β 是类型等式且 a : α，则直接写 a : β 通常无法通过类型检查；此函数可绕过这一限制，把 a 嵌入类型 β，写作 cast h a : β。

最好尽可能避免使用此函数，因为含有强制转换的项更难推理；但当类型并非定义相等时，有时没有更好的做法。

更多信息：等式

函数与实参两方面的同余性。若 f₁ = f₂ 且 a₁ = a₂，则 f₁ a₁ = f₂ a₂。这仅适用于非依赖函数；在依赖情形下，定理陈述更为复杂。

更多信息：等式

函数应用中函数部分的同余性：若 f = g，则 f a = g a。

函数实参的同余性：若 a₁ = a₂，则 f a₁ = f a₂，其中 f 为任意非依赖函数。这比初看上去更强，因为还可以用 lambda 表达式作为 f，证明 <something containing a₁> = <something containing a₂>。congr 和 simp 等策略在子项内部应用等式时，会在内部使用此函数。

更多信息：等式

若 h : α = β 是类型等式的证明，则 h.mp : α → β 是由它诱导的“强制转换”运算，把 α 的元素映射到 β 的元素。

可对 h 归纳来证明结果元素的定理，因为 rfl.mp 定义上就是恒等函数。

若 h : α = β 是类型等式的证明，则 h.mpr : β → α 是由它诱导的反向“强制转换”运算，把 β 的元素映射到 α 的元素。

可对 h 归纳来证明结果元素的定理，因为 rfl.mpr 定义上就是恒等函数。

term ::= ...
    | term ▸ term

当项的类型包含等式一侧作为子项时，可以使用 ▸ 运算符进行重写。 如果等式两侧都出现在项的类型中，则将左侧重写为右侧。