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

```lean
a = b
```

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

## Reflexivity

Every term is equal to itself.

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

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

For example:

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

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

## Using Equalities

If you have:

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

you can replace `a` with `b` using rewriting.

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

After `rw [h]`, the goal changes from:

```lean
a + 1 = b + 1
```

to:

```lean
b + 1 = b + 1
```

which is solved by `rfl`.

## Symmetry

Equality can be reversed.

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

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

## Transitivity

Equalities can be chained.

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

```lean
c = c
```

which is solved by `rfl`.

## Rewriting Direction

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

To reverse the direction, use:

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

Example:

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

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

```lean
rw [h] at hp
```

replaces `a` with `b` inside `hp`.

## Rewriting Multiple Times

You can rewrite with multiple equalities.

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

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

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

```lean
x + 0 = x
```

which is solved by `rfl`.

## Using `calc`

The `calc` block provides structured rewriting.

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

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

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

## Equality in Logical Contexts

Equality can be used inside other logical forms.

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

More interestingly:

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

```lean
⊢ a = a
```

use:

```lean
rfl
```

To use:

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

use:

```lean
rw [h]
```

To reverse:

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

To chain equalities:

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

To rewrite in a hypothesis:

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