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

State before:
e1 e2 e3 : VExpr
k j : Nat
⊢ inst (inst e1 e2 k) e3 (j + k) = inst (inst e1 e3 (j + k + 1)) (inst e2 e3 j) k
Tactic:
induction e1 generalizing k with simp [liftN, inst, instVar, *]
| bvar i => apply inst_instVar_hi
| _ => rename_i IH; apply IH
State after:
no goals

State before:
case bvar
e2 e3 : VExpr
j i k : Nat
⊢ inst (if i < k then bvar i else if i = k then liftN k e2 else bvar (i - 1)) e3 (j + k) =
    inst (if i < j + k + 1 then bvar i else if i = j + k + 1 then liftN (j + k + 1) e3 else bvar (i - 1)) (inst e2 e3 j)
      k
Tactic:
apply inst_instVar_hi
State after:
no goals

State before:
case forallE
e2 e3 : VExpr
j : Nat
binderType✝ body✝ : VExpr
binderType_ih✝ :
  ∀ (k : Nat), inst (inst binderType✝ e2 k) e3 (j + k) = inst (inst binderType✝ e3 (j + k + 1)) (inst e2 e3 j) k
body_ih✝ : ∀ (k : Nat), inst (inst body✝ e2 k) e3 (j + k) = inst (inst body✝ e3 (j + k + 1)) (inst e2 e3 j) k
k : Nat
⊢ inst (inst body✝ e2 (k + 1)) e3 (j + k + 1) = inst (inst body✝ e3 (j + k + 1 + 1)) (inst e2 e3 j) (k + 1)
Tactic:
rename_i IH
State after:
case forallE
e2 e3 : VExpr
j : Nat
binderType✝ body✝ : VExpr
binderType_ih✝ :
  ∀ (k : Nat), inst (inst binderType✝ e2 k) e3 (j + k) = inst (inst binderType✝ e3 (j + k + 1)) (inst e2 e3 j) k
IH : ∀ (k : Nat), inst (inst body✝ e2 k) e3 (j + k) = inst (inst body✝ e3 (j + k + 1)) (inst e2 e3 j) k
k : Nat
⊢ inst (inst body✝ e2 (k + 1)) e3 (j + k + 1) = inst (inst body✝ e3 (j + k + 1 + 1)) (inst e2 e3 j) (k + 1)

State before:
case forallE
e2 e3 : VExpr
j : Nat
binderType✝ body✝ : VExpr
binderType_ih✝ :
  ∀ (k : Nat), inst (inst binderType✝ e2 k) e3 (j + k) = inst (inst binderType✝ e3 (j + k + 1)) (inst e2 e3 j) k
IH : ∀ (k : Nat), inst (inst body✝ e2 k) e3 (j + k) = inst (inst body✝ e3 (j + k + 1)) (inst e2 e3 j) k
k : Nat
⊢ inst (inst body✝ e2 (k + 1)) e3 (j + k + 1) = inst (inst body✝ e3 (j + k + 1 + 1)) (inst e2 e3 j) (k + 1)
Tactic:
apply IH
State after:
no goals