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

State before:
i k n j : Nat
self : i < k
⊢ liftVar n i j < k + n
Tactic:
simp [liftVar]
State after:
i k n j : Nat
self : i < k
⊢ (if i < j then i else n + i) < k + n

State before:
i k n j : Nat
self : i < k
⊢ (if i < j then i else n + i) < k + n
Tactic:
split <;> rename_i h
State after:
case inl
i k n j : Nat
self : i < k
h : i < j
⊢ i < k + n

case inr
i k n j : Nat
self : i < k
h : ¬i < j
⊢ n + i < k + n

State before:
case inl
i k n j : Nat
self : i < k
h : i < j
⊢ i < k + n
Tactic:
exact Nat.lt_of_lt_of_le self (Nat.le_add_right ..)
State after:
no goals

State before:
case inr
i k n j : Nat
self : i < k
h : ¬i < j
⊢ n + i < k + n
Tactic:
rw [Nat.add_comm]
State after:
case inr
i k n j : Nat
self : i < k
h : ¬i < j
⊢ i + n < k + n

State before:
case inr
i k n j : Nat
self : i < k
h : ¬i < j
⊢ i + n < k + n
Tactic:
exact Nat.add_lt_add_right self _
State after:
no goals