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

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

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

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

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