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

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

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

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