# 4.13 Substitution and `subst`

# 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:

```lean
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:

```lean
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:

```lean
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:

```lean
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:

```lean
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.

```lean
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.