The equality relation. It has one introduction rule, Eq.refl. We use a = b as notation for Eq a b. A fundamental property of equality is that it is an equivalence relation.

Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given h1 : a = b and h2 : p a, we can construct a proof for p b using substitution: Eq.subst h1 h2. Example:

The triangle in the second presentation is a macro built on top of Eq.subst and Eq.symm, and you can enter it by typing \t. For more information: Equality

Conventions for notations in identifiers:

• The recommended spelling of = in identifiers is eq.

Constructors

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

term ::= ...
    | The equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.term = term

命题等价 通常由中缀 = 运算符表示。

rfl : a = a is the unique constructor of the equality type. This is the same as Eq.refl except that it takes a implicitly instead of explicitly.

This is a more powerful theorem than it may appear at first, because although the statement of the theorem is a = a, Lean will allow anything that is definitionally equal to that type. So, for instance, 2 + 2 = 4 is proven in Lean by rfl, because both sides are the same up to definitional equality.

Equality is symmetric: if a = b then b = a.

Because this is in the Eq namespace, if you have a variable h : a = b, h.symm can be used as shorthand for Eq.symm h as a proof of b = a.

For more information: Equality

Equality is transitive: if a = b and b = c then a = c.

Because this is in the Eq namespace, if you have variables or expressions h₁ : a = b and h₂ : b = c, you can use h₁.trans h₂ : a = c as shorthand for Eq.trans h₁ h₂.

For more information: Equality

The substitution principle for equality. If a = b and P a holds, then P b also holds. We conventionally use the name motive for P here, so that you can specify it explicitly using e.g. Eq.subst (motive := fun x => x < 5) if it is not otherwise inferred correctly.

This theorem is the underlying mechanism behind the rw tactic, which is essentially a fancy algorithm for finding good motive arguments to usefully apply this theorem to replace occurrences of a with b in the goal or hypotheses.

For more information: Equality

Cast across a type equality. If h : α = β is an equality of types, and a : α, then a : β will usually not typecheck directly, but this function will allow you to work around this and embed a in type β as cast h a : β.

It is best to avoid this function if you can, because it is more complicated to reason about terms containing casts, but if the types don't match up definitionally sometimes there isn't anything better you can do.

For more information: Equality

Congruence in both function and argument. If f₁ = f₂ and a₁ = a₂ then f₁ a₁ = f₂ a₂. This only works for nondependent functions; the theorem statement is more complex in the dependent case.

For more information: Equality

Congruence in the function part of an application: If f = g then f a = g a.

Congruence in the function argument: if a₁ = a₂ then f a₁ = f a₂ for any (nondependent) function f. This is more powerful than it might look at first, because you can also use a lambda expression for f to prove that <something containing a₁> = <something containing a₂>. This function is used internally by tactics like congr and simp to apply equalities inside subterms.

For more information: Equality

If h : α = β is a proof of type equality, then h.mp : α → β is the induced "cast" operation, mapping elements of α to elements of β.

You can prove theorems about the resulting element by induction on h, since rfl.mp is definitionally the identity function.

If h : α = β is a proof of type equality, then h.mpr : β → α is the induced "cast" operation in the reverse direction, mapping elements of β to elements of α.

You can prove theorems about the resulting element by induction on h, since rfl.mpr is definitionally the identity function.

term ::= ...
    | `h ▸ e` is a macro built on top of `Eq.rec` and `Eq.symm` definitions.
Given `h : a = b` and `e : p a`, the term `h ▸ e` has type `p b`.
You can also view `h ▸ e` as a "type casting" operation
where you change the type of `e` by using `h`.

The macro tries both orientations of `h`. If the context provides an
expected type, it rewrites the expected type, else it rewrites the type of e`.

See the Chapter "Quantifiers and Equality" in the manual
"Theorem Proving in Lean" for additional information.
term ▸ term

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