Theorem: Lean4Lean.VExpr.liftN_instN_hi (Lean4Lean/Theory/VExpr.lean)

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
State after:
no goals

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
State after:
no goals

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
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)

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
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:
apply IH
State after:
no goals