**DEPRECATED**: `restate_axiom`

was necessary in Lean 3 but is no longer needed for Lean 4.
It is still present for backwards compatibility but will probably be removed in the future.

# Original Docstring #

`restate_axiom`

makes a new copy of a structure field, first definitionally simplifying the type.
This is useful to remove `auto_param`

or `opt_param`

from the statement.

As an example, we have:

```
structure A :=
(x : ℕ)
(a' : x = 1 . skip)
example (z : A) : z.x = 1 := by rw A.a' -- rewrite tactic failed, lemma is not an equality nor a iff
restate_axiom A.a'
example (z : A) : z.x = 1 := by rw A.a
```

By default, `restate_axiom`

names the new lemma by removing a trailing `'`

, or otherwise appending
`_lemma`

if there is no trailing `'`

. You can also give `restate_axiom`

a second argument to
specify the new name, as in

```
restate_axiom A.a f
example (z : A) : z.x = 1 := by rw A.f
```

## Equations

- One or more equations did not get rendered due to their size.