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.
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.
So for example the tactic lift n to ℕ using hn transforms the goal
n : ℤ, hn : n ≥ 0, h : P n ⊢ n = 3 to n : ℕ, h : P ↑n ⊢ ↑n = 3
(here P is some term of type ℤ → Prop).
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).
So for example the tactic lift n to ℕ transforms the goal
n : ℤ, h : P n ⊢ n = 3 to two goals
n : ℕ, h : P ↑n ⊢ ↑n = 3 and n : ℤ, h : P n ⊢ n ≥ 0.
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 n away
(i.e. the default behavior).
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.
So for example the tactic lift n + 3 to ℕ using hn with k hk transforms the goal
n : ℤ, hn : n + 3 ≥ 0, h : P (n + 3) ⊢ n + 3 = 2 * n to the goal
n : ℤ, k : ℕ, hk : ↑k = n + 3, h : P ↑k ⊢ ↑k = 2 * n.
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.
Given an instance can_lift β γ, it can also lift α → β to α → γ; more generally, given
β : Π a : α, Type*, γ : Π a : α, Type*, and [Π a : α, can_lift (β a) (γ a)], it
automatically generates an instance can_lift (Π a, β a) (Π a, γ a).
lift is in some sense dual to the zify tactic. lift (z : ℤ) to ℕ will change the type of an
integer z (in the supertype) to ℕ (the subtype), given a proof that z ≥ 0;
propositions concerning z will still be over ℤ. zify changes propositions about ℕ (the
subtype) to propositions about ℤ (the supertype), without changing the type of any variable.