2.8 Equality Basics

Equality expresses that two terms are identical. In Lean, equality is a proposition. A proof of a = b allows you to replace a with b in other expressions.

Problem

You want to prove statements involving equality or use equalities to transform goals.

Core Idea

Equality in Lean is written:

a = b

A proof of this type shows that a and b are interchangeable.

Reflexivity

Every term is equal to itself.

theorem eq_refl_example (a : Nat) : a = a := by
  rfl

The tactic rfl closes goals where both sides are definitionally equal.

For example:

theorem compute_example : 2 + 2 = 4 := by
  rfl

Lean reduces 2 + 2 to 4, so both sides match.

Using Equalities

If you have:

h : a = b

you can replace a with b using rewriting.

theorem rewrite_example
    (a b : Nat)
    (h : a = b) :
    a + 1 = b + 1 := by
  rw [h]

After rw [h], the goal changes from:

a + 1 = b + 1

to:

b + 1 = b + 1

which is solved by rfl.

Symmetry

Equality can be reversed.

theorem eq_sym_example
    (a b : Nat)
    (h : a = b) :
    b = a := by
  rw [h]

This works because rewriting replaces b with a in the goal.

There is also a direct theorem:

theorem eq_sym_explicit
    (a b : Nat)
    (h : a = b) :
    b = a :=
  Eq.symm h

Transitivity

Equalities can be chained.

theorem eq_trans_example
    (a b c : Nat)
    (h₁ : a = b)
    (h₂ : b = c) :
    a = c := by
  rw [h₁, h₂]

After rewriting with both equalities, the goal becomes:

c = c

which is solved by rfl.

Rewriting Direction

By default, rw [h] replaces left to right.

To reverse the direction, use:

rw [← h]

Example:

theorem rewrite_reverse
    (a b : Nat)
    (h : a = b) :
    b + 1 = a + 1 := by
  rw [← h]

Rewriting in Hypotheses

You can also rewrite inside a hypothesis.

theorem rewrite_in_hypothesis
    (a b : Nat)
    (h : a = b)
    (hp : a + 1 = 3) :
    b + 1 = 3 := by
  rw [h] at hp
  exact hp

The command:

rw [h] at hp

replaces a with b inside hp.

Rewriting Multiple Times

You can rewrite with multiple equalities.

theorem multiple_rewrite
    (a b c : Nat)
    (h₁ : a = b)
    (h₂ : b = c) :
    a = c := by
  rw [h₁, h₂]

The list [h₁, h₂] applies rewrites in sequence.

Equality as Substitution

Conceptually, equality allows substitution. If a = b, then any expression involving a can be rewritten using b.

Example:

theorem substitution_example
    (a b : Nat)
    (h : a = b) :
    a * a = b * b := by
  rw [h]

Lean replaces both occurrences of a with b.

Equality of Functions

Two functions are equal if they give the same result for all inputs.

theorem function_eq_example :
    (fun x : Nat => x + 0) = (fun x => x) := by
  funext x
  rfl

The tactic funext reduces function equality to pointwise equality.

After funext x, the goal becomes:

x + 0 = x

which is solved by rfl.

Using calc

The calc block provides structured rewriting.

theorem calc_example
    (a b c : Nat)
    (h₁ : a = b)
    (h₂ : b = c) :
    a = c := by
  calc
    a = b := h₁
    _ = c := h₂

Each step states a transformation justified by a proof.

Equality and Computation

Lean automatically reduces expressions when possible.

theorem compute_eq : (3 + 2) * 2 = 10 := by
  rfl

This works because Lean computes both sides.

If reduction is not automatic, you can use simp.

theorem simplify_eq (n : Nat) : n + 0 = n := by
  simp

Equality in Logical Contexts

Equality can be used inside other logical forms.

theorem equality_in_implication
    (a b : Nat)
    (h : a = b) :
    a = b := by
  exact h

More interestingly:

theorem equality_transport
    (a b : Nat)
    (h : a = b)
    (P : Nat -> Prop)
    (hp : P a) :
    P b := by
  rw [h] at hp
  exact hp

The property P is transported along the equality.

Common Patterns

To prove:

⊢ a = a

use:

rfl

To use:

h : a = b

use:

rw [h]

To reverse:

rw [← h]

To chain equalities:

rw [h₁, h₂]

To rewrite in a hypothesis:

rw [h] at hp

Common Pitfalls

Do not assume all equalities are solved by rfl. It only works when both sides reduce to the same expression.

Do not forget rewrite direction. If rewriting fails, try reversing the equality.

Do not confuse definitional equality with propositional equality. Some equalities require explicit proofs.

Do not expect rewriting to apply inside all contexts automatically. Some cases require more advanced rewriting techniques.

Takeaway

Equality is a tool for substitution. A proof of a = b allows you to replace a with b. The main operations are rfl for reflexivity, rw for rewriting, and chaining equalities through composition. These form the foundation for structured reasoning in Lean.