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.