tactic.restate_axiom - mathlib3 docs

meta def restate_axiom (d : declaration) (new_name : name) :

restate_axiom takes a structure field, and makes a new, definitionally simplified copy of it. If the existing field name ends with a ', the new field just has the prime removed. Otherwise, we append _lemma. The main application is to provide clean versions of structure fields that have been tagged with an auto_param.

source

meta def restate_axiom_cmd (_x : interactive.parse (lean.parser.tk "restate_axiom")) :

lean.parser unit

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

source

def tactic_doc.command.restate_axiom :

tactic_doc_entry

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