Theorem: Lean4Lean.VExpr.ClosedN.liftN (Lean4Lean/Theory/VExpr.lean)

State before:
e : VExpr
k n j : Nat
self : ClosedN e k
⊢ ClosedN (liftN n e j) (k + n)
Tactic:
induction e generalizing k j with
  (simp [ClosedN] at self; simp [self, VExpr.liftN, ClosedN, *])
| bvar i => exact liftVar_lt_add self
| lam _ _ _ ih2 | forallE _ _ _ ih2 => exact Nat.add_right_comm .. ▸ ih2 self.2
State after:
no goals

State before:
case app
n : Nat
fn✝ arg✝ : VExpr
fn_ih✝ : ∀ {k j : Nat}, ClosedN fn✝ k → ClosedN (liftN n fn✝ j) (k + n)
arg_ih✝ : ∀ {k j : Nat}, ClosedN arg✝ k → ClosedN (liftN n arg✝ j) (k + n)
k j : Nat
self : ClosedN (app fn✝ arg✝) k
⊢ ClosedN (liftN n (app fn✝ arg✝) j) (k + n)
Tactic:
simp [ClosedN] at self
State after:
case app
n : Nat
fn✝ arg✝ : VExpr
fn_ih✝ : ∀ {k j : Nat}, ClosedN fn✝ k → ClosedN (liftN n fn✝ j) (k + n)
arg_ih✝ : ∀ {k j : Nat}, ClosedN arg✝ k → ClosedN (liftN n arg✝ j) (k + n)
k j : Nat
self : ClosedN fn✝ k ∧ ClosedN arg✝ k
⊢ ClosedN (liftN n (app fn✝ arg✝) j) (k + n)

State before:
case app
n : Nat
fn✝ arg✝ : VExpr
fn_ih✝ : ∀ {k j : Nat}, ClosedN fn✝ k → ClosedN (liftN n fn✝ j) (k + n)
arg_ih✝ : ∀ {k j : Nat}, ClosedN arg✝ k → ClosedN (liftN n arg✝ j) (k + n)
k j : Nat
self : ClosedN fn✝ k ∧ ClosedN arg✝ k
⊢ ClosedN (liftN n (app fn✝ arg✝) j) (k + n)
Tactic:
simp [self, VExpr.liftN, ClosedN, *]
State after:
no goals

State before:
case bvar
n i k j : Nat
self : i < k
⊢ liftVar n i j < k + n
Tactic:
exact liftVar_lt_add self
State after:
no goals

State before:
case forallE
n : Nat
binderType✝ body✝ : VExpr
binderType_ih✝ : ∀ {k j : Nat}, ClosedN binderType✝ k → ClosedN (liftN n binderType✝ j) (k + n)
ih2 : ∀ {k j : Nat}, ClosedN body✝ k → ClosedN (liftN n body✝ j) (k + n)
k j : Nat
self : ClosedN binderType✝ k ∧ ClosedN body✝ (k + 1)
⊢ ClosedN (liftN n body✝ (j + 1)) (k + n + 1)
Tactic:
exact Nat.add_right_comm .. ▸ ih2 self.2
State after:
no goals