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
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
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
- One or more equations did not get rendered due to their size.