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

State before:
n i : Nat
⊢ Lift.liftVar (Lift.skipN n) i = i + n
Tactic:
induction n generalizing i with
| zero => rfl
| succ _ ih => simp [ih, Nat.add_right_comm]; rfl
State after:
no goals

State before:
case zero
i : Nat
⊢ Lift.liftVar (Lift.skipN Nat.zero) i = i + Nat.zero
Tactic:
rfl
State after:
no goals

State before:
case succ
n✝ : Nat
ih : ∀ {i : Nat}, Lift.liftVar (Lift.skipN n✝) i = i + n✝
i : Nat
⊢ Lift.liftVar (Lift.skipN (Nat.succ n✝)) i = i + Nat.succ n✝
Tactic:
simp [ih, Nat.add_right_comm]
State after:
case succ
n✝ : Nat
ih : ∀ {i : Nat}, Lift.liftVar (Lift.skipN n✝) i = i + n✝
i : Nat
⊢ i + n✝ + 1 = i + Nat.succ n✝

State before:
case succ
n✝ : Nat
ih : ∀ {i : Nat}, Lift.liftVar (Lift.skipN n✝) i = i + n✝
i : Nat
⊢ i + n✝ + 1 = i + Nat.succ n✝
Tactic:
rfl
State after:
no goals