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

State before:
i : Nat
e : VExpr
k : Nat
⊢ instVar (i + 1) e (k + 1) = lift (instVar i e k)
Tactic:
simp [instVar, Nat.succ_lt_succ_iff]
State after:
i : Nat
e : VExpr
k : Nat
⊢ (if i < k then bvar (i + 1) else if i = k then liftN (k + 1) e else bvar i) =
    lift (if i < k then bvar i else if i = k then liftN k e else bvar (i - 1))

State before:
i : Nat
e : VExpr
k : Nat
⊢ (if i < k then bvar (i + 1) else if i = k then liftN (k + 1) e else bvar i) =
    lift (if i < k then bvar i else if i = k then liftN k e else bvar (i - 1))
Tactic:
split <;> simp [lift, liftN]
State after:
case inr
i : Nat
e : VExpr
k : Nat
h✝ : ¬i < k
⊢ (if i = k then liftN (k + 1) e else bvar i) = liftN 1 (if i = k then liftN k e else bvar (i - 1))

State before:
case inr
i : Nat
e : VExpr
k : Nat
h✝ : ¬i < k
⊢ (if i = k then liftN (k + 1) e else bvar i) = liftN 1 (if i = k then liftN k e else bvar (i - 1))
Tactic:
split <;> simp [liftN_liftN, liftN]
State after:
case inr.inr
i : Nat
e : VExpr
k : Nat
h✝¹ : ¬i < k
h✝ : ¬i = k
⊢ i = i - 1 + 1

State before:
case inr.inr
i : Nat
e : VExpr
k : Nat
h✝¹ : ¬i < k
h✝ : ¬i = k
⊢ i = i - 1 + 1
Tactic:
have := Nat.lt_of_le_of_ne (Nat.not_lt.1 ‹_›) (Ne.symm ‹_›)
State after:
case inr.inr
i : Nat
e : VExpr
k : Nat
h✝¹ : ¬i < k
h✝ : ¬i = k
this : k < i
⊢ i = i - 1 + 1

State before:
case inr.inr
i : Nat
e : VExpr
k : Nat
h✝¹ : ¬i < k
h✝ : ¬i = k
this : k < i
⊢ i = i - 1 + 1
Tactic:
let i+1 := i
State after:
case inr.inr
i✝ : Nat
e : VExpr
k i : Nat
h✝¹ : ¬i + 1 < k
h✝ : ¬i + 1 = k
this : k < i + 1
⊢ i + 1 = i + 1 - 1 + 1

State before:
case inr.inr
i✝ : Nat
e : VExpr
k i : Nat
h✝¹ : ¬i + 1 < k
h✝ : ¬i + 1 = k
this : k < i + 1
⊢ i + 1 = i + 1 - 1 + 1
Tactic:
rfl
State after:
no goals