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

State before:
n k i : Nat
⊢ Lift.liftVar (Lift.consN (Lift.skipN n) k) i = liftVar n i k
Tactic:
induction k generalizing i with
| zero => simp [liftVar_skipN]
| succ k ih =>
  cases i with simp [liftVar, Nat.succ_lt_succ_iff, ih]
  | succ i => split <;> rfl
State after:
no goals

State before:
case zero
n i : Nat
⊢ Lift.liftVar (Lift.consN (Lift.skipN n) Nat.zero) i = liftVar n i Nat.zero
Tactic:
simp [liftVar_skipN]
State after:
no goals

State before:
case succ
n k : Nat
ih : ∀ {i : Nat}, Lift.liftVar (Lift.consN (Lift.skipN n) k) i = liftVar n i k
i : Nat
⊢ Lift.liftVar (Lift.consN (Lift.skipN n) (Nat.succ k)) i = liftVar n i (Nat.succ k)
Tactic:
cases i with simp [liftVar, Nat.succ_lt_succ_iff, ih]
| succ i => split <;> rfl
State after:
no goals

State before:
case succ.succ
n k : Nat
ih : ∀ {i : Nat}, Lift.liftVar (Lift.consN (Lift.skipN n) k) i = liftVar n i k
i : Nat
⊢ (if i < k then i else n + i) + 1 = if i < k then Nat.succ i else n + Nat.succ i
Tactic:
split <;> rfl
State after:
no goals