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

State before:
k : Nat
e1 e2 : VExpr
⊢ inst (liftN 1 e1 k) e2 k = e1
Tactic:
induction e1 generalizing k with simp [liftN, inst, *]
| bvar i =>
  simp only [liftVar, instVar, Nat.add_comm 1]; split <;> [rfl; rename_i h]
  rw [if_neg (mt (Nat.lt_of_le_of_lt (Nat.le_succ _)) h),
    if_neg (mt (by rintro rfl; apply Nat.lt_succ_self) h)]; rfl
State after:
no goals

State before:
case bvar
e2 : VExpr
i k : Nat
⊢ instVar (liftVar 1 i k) e2 k = bvar i
Tactic:
simp only [liftVar, instVar, Nat.add_comm 1]
State after:
case bvar
e2 : VExpr
i k : Nat
⊢ (if (if i < k then i else i + 1) < k then bvar (if i < k then i else i + 1)
    else if (if i < k then i else i + 1) = k then liftN k e2 else bvar ((if i < k then i else i + 1) - 1)) =
    bvar i

State before:
case bvar
e2 : VExpr
i k : Nat
⊢ (if (if i < k then i else i + 1) < k then bvar (if i < k then i else i + 1)
    else if (if i < k then i else i + 1) = k then liftN k e2 else bvar ((if i < k then i else i + 1) - 1)) =
    bvar i
Tactic:
split <;> [rfl; rename_i h]
State after:
case bvar.inr
e2 : VExpr
i k : Nat
h : ¬i < k
⊢ (if i + 1 < k then bvar (i + 1) else if i + 1 = k then liftN k e2 else bvar (i + 1 - 1)) = bvar i

State before:
case bvar.inr
e2 : VExpr
i k : Nat
h : ¬i < k
⊢ (if i + 1 < k then bvar (i + 1) else if i + 1 = k then liftN k e2 else bvar (i + 1 - 1)) = bvar i
Tactic:
rw [if_neg (mt (Nat.lt_of_le_of_lt (Nat.le_succ _)) h),
  if_neg (mt (by rintro rfl; apply Nat.lt_succ_self) h)]
State after:
case bvar.inr
e2 : VExpr
i k : Nat
h : ¬i < k
⊢ bvar (i + 1 - 1) = bvar i

State before:
case bvar.inr
e2 : VExpr
i k : Nat
h : ¬i < k
⊢ bvar (i + 1 - 1) = bvar i
Tactic:
rfl
State after:
no goals

State before:
e2 : VExpr
i k : Nat
h : ¬i < k
⊢ i + 1 = k → i < k
Tactic:
rintro rfl
State after:
e2 : VExpr
i : Nat
h : ¬i < i + 1
⊢ i < i + 1

State before:
e2 : VExpr
i : Nat
h : ¬i < i + 1
⊢ i < i + 1
Tactic:
apply Nat.lt_succ_self
State after:
no goals