internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
case inl
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
⊢ liftN n (bvar i) k =
    if liftVar n i k < n + j then bvar (liftVar n i k)
    else if liftVar n i k = n + j then liftN (n + j) e else bvar (liftVar n i k - 1)
Tactic:
rw [if_pos]
Proof state after:
case inl
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
⊢ liftN n (bvar i) k = bvar (liftVar n i k)

case inl.hc
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
⊢ liftVar n i k < n + j
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
case inl.hc
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
⊢ liftVar n i k < n + j
Tactic:
simp only [liftN, liftVar]
Proof state after:
case inl.hc
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
⊢ (if i < k then i else n + i) < n + j
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
case inl.hc
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
⊢ (if i < k then i else n + i) < n + j
Tactic:
split <;> rename_i hk
Proof state after:
case inl.hc.inl
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
hk : i < k
⊢ i < n + j

case inl.hc.inr
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
hk : ¬i < k
⊢ n + i < n + j
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
case inl
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
⊢ liftN n (bvar i) k = bvar (liftVar n i k)
Tactic:
rfl
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
case inl.hc.inl
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
hk : i < k
⊢ i < n + j
Tactic:
exact Nat.lt_add_left _ h
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
case inl.hc.inr
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
hk : ¬i < k
⊢ n + i < n + j
Tactic:
exact Nat.add_lt_add_left h _
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
case inr.inl
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : ¬i < j
h' : i = j
⊢ liftN n (liftN j e) k =
    if liftVar n i k < n + j then bvar (liftVar n i k)
    else if liftVar n i k = n + j then liftN (n + j) e else bvar (liftVar n i k - 1)
Tactic:
subst i
Proof state after:
case inr.inl
n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : ¬j < j
⊢ liftN n (liftN j e) k =
    if liftVar n j k < n + j then bvar (liftVar n j k)
    else if liftVar n j k = n + j then liftN (n + j) e else bvar (liftVar n j k - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
case inr.inl
n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : ¬j < j
⊢ liftN n (liftN j e) k =
    if liftVar n j k < n + j then bvar (liftVar n j k)
    else if liftVar n j k = n + j then liftN (n + j) e else bvar (liftVar n j k - 1)
Tactic:
rw [liftN'_liftN' (h1 := Nat.zero_le _) (h2 := hj), liftVar_le hj,
  if_neg (by simp), if_pos rfl, Nat.add_comm]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : ¬j < j
⊢ ¬n + j < n + j
Tactic:
simp
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
case inr.inr
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : ¬i < j
h' : ¬i = j
⊢ liftN n (bvar (i - 1)) k =
    if liftVar n i k < n + j then bvar (liftVar n i k)
    else if liftVar n i k = n + j then liftN (n + j) e else bvar (liftVar n i k - 1)
Tactic:
rw [Nat.not_lt] at h
Proof state after:
case inr.inr
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : j ≤ i
h' : ¬i = j
⊢ liftN n (bvar (i - 1)) k =
    if liftVar n i k < n + j then bvar (liftVar n i k)
    else if liftVar n i k = n + j then liftN (n + j) e else bvar (liftVar n i k - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
case inr.inr
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : j ≤ i
h' : ¬i = j
⊢ liftN n (bvar (i - 1)) k =
    if liftVar n i k < n + j then bvar (liftVar n i k)
    else if liftVar n i k = n + j then liftN (n + j) e else bvar (liftVar n i k - 1)
Tactic:
rw [liftVar_le (Nat.le_trans hj h)]
Proof state after:
case inr.inr
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : j ≤ i
h' : ¬i = j
⊢ liftN n (bvar (i - 1)) k =
    if n + i < n + j then bvar (n + i) else if n + i = n + j then liftN (n + j) e else bvar (n + i - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
case inr.inr
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : j ≤ i
h' : ¬i = j
⊢ liftN n (bvar (i - 1)) k =
    if n + i < n + j then bvar (n + i) else if n + i = n + j then liftN (n + j) e else bvar (n + i - 1)
Tactic:
have hk := Nat.lt_of_le_of_ne h (Ne.symm h')
Proof state after:
case inr.inr
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : j ≤ i
h' : ¬i = j
hk : j < i
⊢ liftN n (bvar (i - 1)) k =
    if n + i < n + j then bvar (n + i) else if n + i = n + j then liftN (n + j) e else bvar (n + i - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
case inr.inr
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : j ≤ i
h' : ¬i = j
hk : j < i
⊢ liftN n (bvar (i - 1)) k =
    if n + i < n + j then bvar (n + i) else if n + i = n + j then liftN (n + j) e else bvar (n + i - 1)
Tactic:
let i+1 := i
Proof state after:
case inr.inr
i✝ n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
i : Nat
h : j ≤ i + 1
h' : ¬i + 1 = j
hk : j < i + 1
⊢ liftN n (bvar (i + 1 - 1)) k =
    if n + (i + 1) < n + j then bvar (n + (i + 1))
    else if n + (i + 1) = n + j then liftN (n + j) e else bvar (n + (i + 1) - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
case inr.inr
i✝ n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
i : Nat
h : j ≤ i + 1
h' : ¬i + 1 = j
hk : j < i + 1
⊢ liftN n (bvar (i + 1 - 1)) k =
    if n + (i + 1) < n + j then bvar (n + (i + 1))
    else if n + (i + 1) = n + j then liftN (n + j) e else bvar (n + (i + 1) - 1)
Tactic:
have := Nat.add_lt_add_left hk n
Proof state after:
case inr.inr
i✝ n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
i : Nat
h : j ≤ i + 1
h' : ¬i + 1 = j
hk : j < i + 1
this : n + j < n + (i + 1)
⊢ liftN n (bvar (i + 1 - 1)) k =
    if n + (i + 1) < n + j then bvar (n + (i + 1))
    else if n + (i + 1) = n + j then liftN (n + j) e else bvar (n + (i + 1) - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
case inr.inr
i✝ n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
i : Nat
h : j ≤ i + 1
h' : ¬i + 1 = j
hk : j < i + 1
this : n + j < n + (i + 1)
⊢ liftN n (bvar (i + 1 - 1)) k =
    if n + (i + 1) < n + j then bvar (n + (i + 1))
    else if n + (i + 1) = n + j then liftN (n + j) e else bvar (n + (i + 1) - 1)
Tactic:
rw [if_neg (Nat.lt_asymm this), if_neg (Nat.ne_of_gt this)]
Proof state after:
case inr.inr
i✝ n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
i : Nat
h : j ≤ i + 1
h' : ¬i + 1 = j
hk : j < i + 1
this : n + j < n + (i + 1)
⊢ liftN n (bvar (i + 1 - 1)) k = bvar (n + (i + 1) - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
case inr.inr
i✝ n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
i : Nat
h : j ≤ i + 1
h' : ¬i + 1 = j
hk : j < i + 1
this : n + j < n + (i + 1)
⊢ liftN n (bvar (i + 1 - 1)) k = bvar (n + (i + 1) - 1)
Tactic:
simp only [liftN]
Proof state after:
case inr.inr
i✝ n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
i : Nat
h : j ≤ i + 1
h' : ¬i + 1 = j
hk : j < i + 1
this : n + j < n + (i + 1)
⊢ bvar (liftVar n (i + 1 - 1) k) = bvar (n + (i + 1) - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
case inr.inr
i✝ n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
i : Nat
h : j ≤ i + 1
h' : ¬i + 1 = j
hk : j < i + 1
this : n + j < n + (i + 1)
⊢ bvar (liftVar n (i + 1 - 1) k) = bvar (n + (i + 1) - 1)
Tactic:
rw [liftVar_le (Nat.le_trans hj <| by exact Nat.le_of_lt_succ hk)]
Proof state after:
case inr.inr
i✝ n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
i : Nat
h : j ≤ i + 1
h' : ¬i + 1 = j
hk : j < i + 1
this : n + j < n + (i + 1)
⊢ bvar (n + (i + 1 - 1)) = bvar (n + (i + 1) - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
case inr.inr
i✝ n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
i : Nat
h : j ≤ i + 1
h' : ¬i + 1 = j
hk : j < i + 1
this : n + j < n + (i + 1)
⊢ bvar (n + (i + 1 - 1)) = bvar (n + (i + 1) - 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
i✝ n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
i : Nat
h : j ≤ i + 1
h' : ¬i + 1 = j
hk : j < i + 1
this : n + j < n + (i + 1)
⊢ j ≤ i + 1 - 1
Tactic:
exact Nat.le_of_lt_succ hk
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_instVar_hi
Proof state before:
i : Nat
e2 : VExpr
n k j : Nat
⊢ liftN n (instVar i e2 j) (k + j) = instVar (liftVar n i (k + j + 1)) (liftN n e2 k) j
Tactic:
simp [instVar]
Proof state after:
i : Nat
e2 : VExpr
n k j : Nat
⊢ liftN n (if i < j then bvar i else if i = j then liftN j e2 else bvar (i - 1)) (k + j) =
    if liftVar n i (k + j + 1) < j then bvar (liftVar n i (k + j + 1))
    else if liftVar n i (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n i (k + j + 1) - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_hi
Proof state before:
i : Nat
e2 : VExpr
n k j : Nat
⊢ liftN n (if i < j then bvar i else if i = j then liftN j e2 else bvar (i - 1)) (k + j) =
    if liftVar n i (k + j + 1) < j then bvar (liftVar n i (k + j + 1))
    else if liftVar n i (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n i (k + j + 1) - 1)
Tactic:
split <;> rename_i h
Proof state after:
case inl
i : Nat
e2 : VExpr
n k j : Nat
h : i < j
⊢ liftN n (bvar i) (k + j) =
    if liftVar n i (k + j + 1) < j then bvar (liftVar n i (k + j + 1))
    else if liftVar n i (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n i (k + j + 1) - 1)

case inr
i : Nat
e2 : VExpr
n k j : Nat
h : ¬i < j
⊢ liftN n (if i = j then liftN j e2 else bvar (i - 1)) (k + j) =
    if liftVar n i (k + j + 1) < j then bvar (liftVar n i (k + j + 1))
    else if liftVar n i (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n i (k + j + 1) - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_hi
Proof state before:
case inr
i : Nat
e2 : VExpr
n k j : Nat
h : ¬i < j
⊢ liftN n (if i = j then liftN j e2 else bvar (i - 1)) (k + j) =
    if liftVar n i (k + j + 1) < j then bvar (liftVar n i (k + j + 1))
    else if liftVar n i (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n i (k + j + 1) - 1)
Tactic:
split <;> rename_i h'
Proof state after:
case inr.inl
i : Nat
e2 : VExpr
n k j : Nat
h : ¬i < j
h' : i = j
⊢ liftN n (liftN j e2) (k + j) =
    if liftVar n i (k + j + 1) < j then bvar (liftVar n i (k + j + 1))
    else if liftVar n i (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n i (k + j + 1) - 1)

case inr.inr
i : Nat
e2 : VExpr
n k j : Nat
h : ¬i < j
h' : ¬i = j
⊢ liftN n (bvar (i - 1)) (k + j) =
    if liftVar n i (k + j + 1) < j then bvar (liftVar n i (k + j + 1))
    else if liftVar n i (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n i (k + j + 1) - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_hi
Proof state before:
case inl
i : Nat
e2 : VExpr
n k j : Nat
h : i < j
⊢ liftN n (bvar i) (k + j) =
    if liftVar n i (k + j + 1) < j then bvar (liftVar n i (k + j + 1))
    else if liftVar n i (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n i (k + j + 1) - 1)
Tactic:
have := Nat.lt_add_left k h
Proof state after:
case inl
i : Nat
e2 : VExpr
n k j : Nat
h : i < j
this : i < k + j
⊢ liftN n (bvar i) (k + j) =
    if liftVar n i (k + j + 1) < j then bvar (liftVar n i (k + j + 1))
    else if liftVar n i (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n i (k + j + 1) - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_hi
Proof state before:
case inl
i : Nat
e2 : VExpr
n k j : Nat
h : i < j
this : i < k + j
⊢ liftN n (bvar i) (k + j) =
    if liftVar n i (k + j + 1) < j then bvar (liftVar n i (k + j + 1))
    else if liftVar n i (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n i (k + j + 1) - 1)
Tactic:
rw [liftVar_lt <| Nat.lt_succ_of_lt this, if_pos h]
Proof state after:
case inl
i : Nat
e2 : VExpr
n k j : Nat
h : i < j
this : i < k + j
⊢ liftN n (bvar i) (k + j) = bvar i
Theorem: Lean4Lean.VExpr.liftN_instVar_hi
Proof state before:
case inl
i : Nat
e2 : VExpr
n k j : Nat
h : i < j
this : i < k + j
⊢ liftN n (bvar i) (k + j) = bvar i
Tactic:
simp [liftN, liftVar_lt this]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_instVar_hi
Proof state before:
case inr.inl
i : Nat
e2 : VExpr
n k j : Nat
h : ¬i < j
h' : i = j
⊢ liftN n (liftN j e2) (k + j) =
    if liftVar n i (k + j + 1) < j then bvar (liftVar n i (k + j + 1))
    else if liftVar n i (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n i (k + j + 1) - 1)
Tactic:
subst i
Proof state after:
case inr.inl
e2 : VExpr
n k j : Nat
h : ¬j < j
⊢ liftN n (liftN j e2) (k + j) =
    if liftVar n j (k + j + 1) < j then bvar (liftVar n j (k + j + 1))
    else if liftVar n j (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n j (k + j + 1) - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_hi
Proof state before:
case inr.inl
e2 : VExpr
n k j : Nat
h : ¬j < j
⊢ liftN n (liftN j e2) (k + j) =
    if liftVar n j (k + j + 1) < j then bvar (liftVar n j (k + j + 1))
    else if liftVar n j (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n j (k + j + 1) - 1)
Tactic:
have := Nat.le_add_left j k
Proof state after:
case inr.inl
e2 : VExpr
n k j : Nat
h : ¬j < j
this : j ≤ k + j
⊢ liftN n (liftN j e2) (k + j) =
    if liftVar n j (k + j + 1) < j then bvar (liftVar n j (k + j + 1))
    else if liftVar n j (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n j (k + j + 1) - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_hi
Proof state before:
case inr.inl
e2 : VExpr
n k j : Nat
h : ¬j < j
this : j ≤ k + j
⊢ liftN n (liftN j e2) (k + j) =
    if liftVar n j (k + j + 1) < j then bvar (liftVar n j (k + j + 1))
    else if liftVar n j (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n j (k + j + 1) - 1)
Tactic:
simp [liftVar_lt (by exact Nat.lt_succ_of_le this)]
Proof state after:
case inr.inl
e2 : VExpr
n k j : Nat
h : ¬j < j
this : j ≤ k + j
⊢ liftN n (liftN j e2) (k + j) = liftN j (liftN n e2 k)
Theorem: Lean4Lean.VExpr.liftN_instVar_hi
Proof state before:
case inr.inl
e2 : VExpr
n k j : Nat
h : ¬j < j
this : j ≤ k + j
⊢ liftN n (liftN j e2) (k + j) = liftN j (liftN n e2 k)
Tactic:
rw [liftN'_comm (h := Nat.zero_le _), Nat.add_comm]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_instVar_hi
Proof state before:
e2 : VExpr
n k j : Nat
h : ¬j < j
this : j ≤ k + j
⊢ ?m.56873 < ?m.56874
Tactic:
exact Nat.lt_succ_of_le this
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_instVar_hi
Proof state before:
case inr.inr
i : Nat
e2 : VExpr
n k j : Nat
h : ¬i < j
h' : ¬i = j
⊢ liftN n (bvar (i - 1)) (k + j) =
    if liftVar n i (k + j + 1) < j then bvar (liftVar n i (k + j + 1))
    else if liftVar n i (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n i (k + j + 1) - 1)
Tactic:
have hk := Nat.lt_of_le_of_ne (Nat.not_lt.1 h) (Ne.symm h')
Proof state after:
case inr.inr
i : Nat
e2 : VExpr
n k j : Nat
h : ¬i < j
h' : ¬i = j
hk : j < i
⊢ liftN n (bvar (i - 1)) (k + j) =
    if liftVar n i (k + j + 1) < j then bvar (liftVar n i (k + j + 1))
    else if liftVar n i (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n i (k + j + 1) - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_hi
Proof state before:
case inr.inr
i : Nat
e2 : VExpr
n k j : Nat
h : ¬i < j
h' : ¬i = j
hk : j < i
⊢ liftN n (bvar (i - 1)) (k + j) =
    if liftVar n i (k + j + 1) < j then bvar (liftVar n i (k + j + 1))
    else if liftVar n i (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n i (k + j + 1) - 1)
Tactic:
let i+1 := i
Proof state after:
case inr.inr
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
⊢ liftN n (bvar (i + 1 - 1)) (k + j) =
    if liftVar n (i + 1) (k + j + 1) < j then bvar (liftVar n (i + 1) (k + j + 1))
    else if liftVar n (i + 1) (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n (i + 1) (k + j + 1) - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_hi
Proof state before:
case inr.inr
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
⊢ liftN n (bvar (i + 1 - 1)) (k + j) =
    if liftVar n (i + 1) (k + j + 1) < j then bvar (liftVar n (i + 1) (k + j + 1))
    else if liftVar n (i + 1) (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n (i + 1) (k + j + 1) - 1)
Tactic:
simp [liftVar, h, Nat.succ_lt_succ_iff]
Proof state after:
case inr.inr
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
⊢ liftN n (bvar i) (k + j) =
    if (if i < k + j then i + 1 else n + (i + 1)) < j then bvar (if i < k + j then i + 1 else n + (i + 1))
    else
      if (if i < k + j then i + 1 else n + (i + 1)) = j then liftN j (liftN n e2 k)
      else bvar ((if i < k + j then i + 1 else n + (i + 1)) - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_hi
Proof state before:
case inr.inr
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
⊢ liftN n (bvar i) (k + j) =
    if (if i < k + j then i + 1 else n + (i + 1)) < j then bvar (if i < k + j then i + 1 else n + (i + 1))
    else
      if (if i < k + j then i + 1 else n + (i + 1)) = j then liftN j (liftN n e2 k)
      else bvar ((if i < k + j then i + 1 else n + (i + 1)) - 1)
Tactic:
split <;> rename_i hi
Proof state after:
case inr.inr.inl
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
hi : i < k + j
⊢ liftN n (bvar i) (k + j) = bvar (i + 1 - 1)

case inr.inr.inr
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
hi : ¬i < k + j
⊢ liftN n (bvar i) (k + j) =
    if n + (i + 1) < j then bvar (n + (i + 1))
    else if n + (i + 1) = j then liftN j (liftN n e2 k) else bvar (n + (i + 1) - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_hi
Proof state before:
case inr.inr.inl
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
hi : i < k + j
⊢ liftN n (bvar i) (k + j) = bvar (i + 1 - 1)
Tactic:
simp [liftN, liftVar_lt hi]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_instVar_hi
Proof state before:
case inr.inr.inr
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
hi : ¬i < k + j
⊢ liftN n (bvar i) (k + j) =
    if n + (i + 1) < j then bvar (n + (i + 1))
    else if n + (i + 1) = j then liftN j (liftN n e2 k) else bvar (n + (i + 1) - 1)
Tactic:
have := Nat.lt_add_left n hk
Proof state after:
case inr.inr.inr
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
hi : ¬i < k + j
this : j < n + (i + 1)
⊢ liftN n (bvar i) (k + j) =
    if n + (i + 1) < j then bvar (n + (i + 1))
    else if n + (i + 1) = j then liftN j (liftN n e2 k) else bvar (n + (i + 1) - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_hi
Proof state before:
case inr.inr.inr
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
hi : ¬i < k + j
this : j < n + (i + 1)
⊢ liftN n (bvar i) (k + j) =
    if n + (i + 1) < j then bvar (n + (i + 1))
    else if n + (i + 1) = j then liftN j (liftN n e2 k) else bvar (n + (i + 1) - 1)
Tactic:
rw [if_neg (Nat.lt_asymm this), if_neg (Nat.ne_of_gt this)]
Proof state after:
case inr.inr.inr
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
hi : ¬i < k + j
this : j < n + (i + 1)
⊢ liftN n (bvar i) (k + j) = bvar (n + (i + 1) - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_hi
Proof state before:
case inr.inr.inr
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
hi : ¬i < k + j
this : j < n + (i + 1)
⊢ liftN n (bvar i) (k + j) = bvar (n + (i + 1) - 1)
Tactic:
simp [liftN]
Proof state after:
case inr.inr.inr
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
hi : ¬i < k + j
this : j < n + (i + 1)
⊢ liftVar n i (k + j) = n + (i + 1) - 1
Theorem: Lean4Lean.VExpr.liftN_instVar_hi
Proof state before:
case inr.inr.inr
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
hi : ¬i < k + j
this : j < n + (i + 1)
⊢ liftVar n i (k + j) = n + (i + 1) - 1
Tactic:
rw [liftVar_le (Nat.not_lt.1 hi)]
Proof state after:
case inr.inr.inr
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
hi : ¬i < k + j
this : j < n + (i + 1)
⊢ n + i = n + (i + 1) - 1
Theorem: Lean4Lean.VExpr.liftN_instVar_hi
Proof state before:
case inr.inr.inr
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
hi : ¬i < k + j
this : j < n + (i + 1)
⊢ n + i = n + (i + 1) - 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.instL_instVar
Proof state before:
i : Nat
e : VExpr
k : Nat
ls : List VLevel
⊢ instL ls (instVar i e k) = instVar i (instL ls e) k
Tactic:
simp [instVar]
Proof state after:
i : Nat
e : VExpr
k : Nat
ls : List VLevel
⊢ instL ls (if i < k then bvar i else if i = k then liftN k e else bvar (i - 1)) =
    if i < k then bvar i else if i = k then liftN k (instL ls e) else bvar (i - 1)
Theorem: Lean4Lean.VExpr.instL_instVar
Proof state before:
i : Nat
e : VExpr
k : Nat
ls : List VLevel
⊢ instL ls (if i < k then bvar i else if i = k then liftN k e else bvar (i - 1)) =
    if i < k then bvar i else if i = k then liftN k (instL ls e) else bvar (i - 1)
Tactic:
split <;> [skip; split] <;> simp [instL, instL_liftN]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_instN_lo
Proof state before:
n : Nat
e1 e2 : VExpr
j k : Nat
hj : k ≤ j
⊢ liftN n (inst e1 e2 j) k = inst (liftN n e1 k) e2 (n + j)
Tactic:
induction e1 generalizing k j with
  simp [liftN, inst, instVar, Nat.add_le_add_iff_right, *]
| bvar i => apply liftN_instVar_lo (hj := hj)
| _ => rfl
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_instN_lo
Proof state before:
case bvar
n : Nat
e2 : VExpr
i j k : Nat
hj : k ≤ j
⊢ liftN n (if i < j then bvar i else if i = j then liftN j e2 else bvar (i - 1)) k =
    if liftVar n i k < n + j then bvar (liftVar n i k)
    else if liftVar n i k = n + j then liftN (n + j) e2 else bvar (liftVar n i k - 1)
Tactic:
apply liftN_instVar_lo (hj := hj)
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_instN_lo
Proof state before:
case forallE
n : Nat
e2 binderType✝ body✝ : VExpr
binderType_ih✝ : ∀ (j k : Nat), k ≤ j → liftN n (inst binderType✝ e2 j) k = inst (liftN n binderType✝ k) e2 (n + j)
body_ih✝ : ∀ (j k : Nat), k ≤ j → liftN n (inst body✝ e2 j) k = inst (liftN n body✝ k) e2 (n + j)
j k : Nat
hj : k ≤ j
⊢ inst (liftN n body✝ (k + 1)) e2 (n + (j + 1)) = inst (liftN n body✝ (k + 1)) e2 (n + j + 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_instN_hi
Proof state before:
e1 e2 : VExpr
n k j : Nat
⊢ liftN n (inst e1 e2 j) (k + j) = inst (liftN n e1 (k + j + 1)) (liftN n e2 k) j
Tactic:
induction e1 generalizing j with simp [liftN, inst, instVar, *]
| bvar i => apply liftN_instVar_hi
| _ => rename_i IH; apply IH
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_instN_hi
Proof state before:
case bvar
e2 : VExpr
n k i j : Nat
⊢ liftN n (if i < j then bvar i else if i = j then liftN j e2 else bvar (i - 1)) (k + j) =
    if liftVar n i (k + j + 1) < j then bvar (liftVar n i (k + j + 1))
    else if liftVar n i (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n i (k + j + 1) - 1)
Tactic:
apply liftN_instVar_hi
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_instN_hi
Proof state before:
case forallE
e2 : VExpr
n k : Nat
binderType✝ body✝ : VExpr
binderType_ih✝ :
  ∀ (j : Nat), liftN n (inst binderType✝ e2 j) (k + j) = inst (liftN n binderType✝ (k + j + 1)) (liftN n e2 k) j
body_ih✝ : ∀ (j : Nat), liftN n (inst body✝ e2 j) (k + j) = inst (liftN n body✝ (k + j + 1)) (liftN n e2 k) j
j : Nat
⊢ liftN n (inst body✝ e2 (j + 1)) (k + j + 1) = inst (liftN n body✝ (k + j + 1 + 1)) (liftN n e2 k) (j + 1)
Tactic:
rename_i IH
Proof state after:
case forallE
e2 : VExpr
n k : Nat
binderType✝ body✝ : VExpr
binderType_ih✝ :
  ∀ (j : Nat), liftN n (inst binderType✝ e2 j) (k + j) = inst (liftN n binderType✝ (k + j + 1)) (liftN n e2 k) j
IH : ∀ (j : Nat), liftN n (inst body✝ e2 j) (k + j) = inst (liftN n body✝ (k + j + 1)) (liftN n e2 k) j
j : Nat
⊢ liftN n (inst body✝ e2 (j + 1)) (k + j + 1) = inst (liftN n body✝ (k + j + 1 + 1)) (liftN n e2 k) (j + 1)