2.10 Symmetry and Transitivity

Equality supports two structural operations: reversing direction (symmetry) and chaining steps (transitivity). These operations turn isolated equalities into usable proof pipelines.

Problem

You have equalities in the wrong direction, or you need to combine several equalities to reach a target.

Symmetry

If you know:

h : a = b

then you can reverse it to obtain:

b = a

Tactic form

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

Here rw [h] replaces b with a in the goal.

Term form

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

Eq.symm explicitly reverses an equality.

When to use symmetry

Use symmetry when the goal direction does not match the available equality.

-- goal: b = a
-- have: h : a = b

Either rewrite with h, or explicitly use Eq.symm h.

Transitivity

If you know:

h₁ : a = b
h₂ : b = c

then you can combine them to obtain:

a = c

Tactic form

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

The rewrites apply sequentially.

Term form

theorem eq_trans_term
    (a b c : Nat)
    (h₁ : a = b)
    (h₂ : b = c) :
    a = c :=
  Eq.trans h₁ h₂

Eq.trans composes two equalities.

Combining Symmetry and Transitivity

Often equalities are not aligned in the right direction.

theorem eq_chain_mixed
    (a b c : Nat)
    (h₁ : b = a)
    (h₂ : b = c) :
    a = c := by
  have h₁' : a = b := Eq.symm h₁
  rw [h₁', h₂]

Steps:

1. Reverse h₁ to match direction
2. Chain with h₂

The term version:

theorem eq_chain_mixed_term
    (a b c : Nat)
    (h₁ : b = a)
    (h₂ : b = c) :
    a = c :=
  Eq.trans (Eq.symm h₁) h₂

Structured Reasoning with calc

The calc block expresses symmetry and transitivity in a readable chain.

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

Each step uses a known equality. The _ means “same as previous expression”.

You can include symmetry inside calc.

theorem eq_calc_with_symm
    (a b c : Nat)
    (h₁ : b = a)
    (h₂ : b = c) :
    a = c := by
  calc
    a = b := Eq.symm h₁
    _ = c := h₂

This style scales well when chaining many steps.

Rewriting vs Explicit Transitivity

The following two proofs are equivalent:

rw [h₁, h₂]

and:

Eq.trans h₁ h₂

The difference is:

• rw performs substitution inside a goal
• Eq.trans constructs a new equality term

Use rw for local transformations. Use Eq.trans when building equalities as values.

Equality Chains in Larger Expressions

Symmetry and transitivity apply inside expressions.

theorem eq_inside_expression
    (a b c : Nat)
    (h₁ : a = b)
    (h₂ : b = c) :
    (a + 1) * 2 = (c + 1) * 2 := by
  rw [h₁, h₂]

Lean rewrites a to b, then b to c.

The chain is implicit in the rewriting.

Multiple-Step Chains

Longer chains are handled naturally.

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

Or with calc:

theorem eq_long_chain_calc
    (a b c d : Nat)
    (h₁ : a = b)
    (h₂ : b = c)
    (h₃ : c = d) :
    a = d := by
  calc
    a = b := h₁
    _ = c := h₂
    _ = d := h₃

Symmetry as a Rewrite Tool

Instead of writing:

rw [← h]

you can write:

rw [Eq.symm h]

These are equivalent. The arrow notation is shorter and preferred in tactic scripts.

Common Patterns

Reverse equality:

rw [← h]

or:

Eq.symm h

Chain equalities:

rw [h₁, h₂]

or:

Eq.trans h₁ h₂

Readable chain:

calc
  a = b := h₁
  _ = c := h₂

Common Pitfalls

Do not assume equalities are oriented correctly. Check direction before rewriting.

Do not mix directions accidentally in chains. A single reversed equality can block the entire rewrite.

Do not overuse rw when building equalities as values. Use Eq.trans or calc when the result itself is an equality object.

Do not write long rw chains without structure. For more than a few steps, use calc.

Takeaway

Symmetry flips equalities. Transitivity composes them. Together, they form equality chains. In practice, rw performs these operations implicitly, while Eq.symm, Eq.trans, and calc expose them explicitly.