lift tactic

A class specifying that you can lift elements from α to β assuming cond is true. Used by the tactic lift.

Lift the expression p to the type t, with proof obligation given by h. The list n is used for the two newly generated names, and to specify whether h should remain in the local context. See the doc string of tactic.interactive.lift for more information.

Lift an expression to another type.

• Usage: 'lift' expr 'to' expr ('using' expr)? ('with' id (id id?)?)?.
• If n : ℤ and hn : n ≥ 0 then the tactic lift n to ℕ using hn creates a new constant of type ℕ, also named n and replaces all occurrences of the old variable (n : ℤ) with ↑n (where n in the new variable). It will remove n and hn from the context.
• The argument using hn is optional, the tactic lift n to ℕ does the same, but also creates a new subgoal that n ≥ 0 (where n is the old variable).
• You can also use lift n to ℕ using e where e is any expression of type n ≥ 0.
• Use lift n to ℕ with k to specify the name of the new variable.
• Use lift n to ℕ with k hk to also specify the name of the equality ↑k = n. In this case, n will remain in the context. You can use rfl for the name of hk to substitute it away.
• You can also use lift e to ℕ with k hk where e is any expression of type ℤ. In this case, the hk will always stay in the context, but it will be used to rewrite e in all hypotheses and the target.
• The tactic lift n to ℕ using h will remove h from the context. If you want to keep it, specify it again as the third argument to with, like this: lift n to ℕ using h with n rfl h.
• More generally, this can lift an expression from α to β assuming that there is an instance of can_lift α β. In this case the proof obligation is specified by can_lift.cond.