4.13 Substitution and `subst`

Substitution is the direct elimination of equalities from the context. Given a hypothesis h : x = t, the tactic subst h replaces every occurrence of x with t in the goal and in all hypotheses, and then removes h. In Lean, this is a structured form of rewriting that updates the entire context in one step.

The basic pattern:

example (x y : Nat) (h : x = y) :
  x + x = y + y := by
  subst h
  rfl

After subst h, the context contains no x; all occurrences have been replaced by y. The goal reduces to y + y = y + y, which closes by reflexivity.

Substitution is particularly effective when a variable is equated to a concrete term:

example (x : Nat) (h : x = 3) :
  x + 1 = 4 := by
  subst h
  rfl

This removes the indirection and exposes a computable expression.

Compared with rw, substitution is global and destructive. It updates every occurrence and deletes the equality. This is often desirable when the equality defines a variable completely. In contrast, rw is local and preserves the hypothesis.

Substitution also simplifies dependent contexts. If types depend on a variable, subst transports those dependencies automatically:

example (x y : Nat) (h : x = y)
  (P : Nat -> Prop) (Hx : P x) :
  P y := by
  subst h
  exact Hx

After substitution, the goal becomes P x, matching the hypothesis.

A common use case is normalizing a context before further reasoning:

example (x y : Nat) (h : x = y)
  (H : x + 2 = 5) :
  y + 2 = 5 := by
  subst h
  exact H

This avoids repeated rewriting and keeps the context consistent.

Substitution can be applied repeatedly:

example (x y z : Nat)
  (h₁ : x = y) (h₂ : y = z) :
  x = z := by
  subst h₁
  subst h₂
  rfl

Each step removes one equality and simplifies the goal.

There are limits. Substitution works best when the left-hand side is a variable. For general equalities such as a + b = c, subst does not apply directly. In those cases, use rw or structured rewriting.

Another consideration is direction. If the equality is oriented as t = x, Lean will substitute x with t. If the orientation is not suitable, you may need to rewrite first or use symmetry.

example (x y : Nat) (h : y = x) :
  x + 1 = y + 1 := by
  subst h
  rfl

Here x is replaced by y.

A practical guideline:

Use subst when a variable is fully determined by an equality.
Use rw when you need local, controlled replacement.
Normalize the context early to reduce complexity.

Substitution reduces the number of symbols in the context and often exposes definitional equalities. It is a strong simplification step and should be applied when it aligns the goal with available hypotheses.

In summary, subst performs global replacement and removes equalities. It is the most direct way to eliminate variables defined by equalities and to simplify both goals and contexts.