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

```lean
h : a = b
```

then you can reverse it to obtain:

```lean
b = a
```

### Tactic form

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

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

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

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

## Transitivity

If you know:

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

then you can combine them to obtain:

```lean
a = c
```

### Tactic form

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

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

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

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

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

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

```lean
rw [h₁, h₂]
```

and:

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

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

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

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

```lean
rw [← h]
```

you can write:

```lean
rw [Eq.symm h]
```

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

## Common Patterns

Reverse equality:

```lean
rw [← h]
```

or:

```lean
Eq.symm h
```

Chain equalities:

```lean
rw [h₁, h₂]
```

or:

```lean
Eq.trans h₁ h₂
```

Readable chain:

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