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

State before:
e : VExpr
k j n : Nat
self : ClosedN e k
h : k ≤ j
⊢ liftN n e j = e
Tactic:
induction e generalizing k j with
  (simp [ClosedN] at self; simp [self, liftN, *])
| bvar i => exact liftVar_lt (Nat.lt_of_lt_of_le self h)
| app _ _ ih1 ih2 => exact ⟨ih1 self.1 h, ih2 self.2 h⟩
| lam _ _ ih1 ih2 | forallE _ _ ih1 ih2 =>
  exact ⟨ih1 self.1 h, ih2 self.2 (Nat.succ_le_succ h)⟩
State after:
no goals

State before:
case const
n : Nat
declName✝ : Name
us✝ : List VLevel
k j : Nat
self : ClosedN (const declName✝ us✝) k
h : k ≤ j
⊢ liftN n (const declName✝ us✝) j = const declName✝ us✝
Tactic:
simp [ClosedN] at self
State after:
case const
n : Nat
declName✝ : Name
us✝ : List VLevel
k j : Nat
self : True
h : k ≤ j
⊢ liftN n (const declName✝ us✝) j = const declName✝ us✝

State before:
case const
n : Nat
declName✝ : Name
us✝ : List VLevel
k j : Nat
self : True
h : k ≤ j
⊢ liftN n (const declName✝ us✝) j = const declName✝ us✝
Tactic:
simp [self, liftN, *]
State after:
no goals

State before:
case bvar
n i k j : Nat
self : i < k
h : k ≤ j
⊢ liftVar n i j = i
Tactic:
exact liftVar_lt (Nat.lt_of_lt_of_le self h)
State after:
no goals

State before:
case app
n : Nat
fn✝ arg✝ : VExpr
ih1 : ∀ {k j : Nat}, ClosedN fn✝ k → k ≤ j → liftN n fn✝ j = fn✝
ih2 : ∀ {k j : Nat}, ClosedN arg✝ k → k ≤ j → liftN n arg✝ j = arg✝
k j : Nat
self : ClosedN fn✝ k ∧ ClosedN arg✝ k
h : k ≤ j
⊢ liftN n fn✝ j = fn✝ ∧ liftN n arg✝ j = arg✝
Tactic:
exact ⟨ih1 self.1 h, ih2 self.2 h⟩
State after:
no goals

State before:
case forallE
n : Nat
binderType✝ body✝ : VExpr
ih1 : ∀ {k j : Nat}, ClosedN binderType✝ k → k ≤ j → liftN n binderType✝ j = binderType✝
ih2 : ∀ {k j : Nat}, ClosedN body✝ k → k ≤ j → liftN n body✝ j = body✝
k j : Nat
self : ClosedN binderType✝ k ∧ ClosedN body✝ (k + 1)
h : k ≤ j
⊢ liftN n binderType✝ j = binderType✝ ∧ liftN n body✝ (j + 1) = body✝
Tactic:
exact ⟨ih1 self.1 h, ih2 self.2 (Nat.succ_le_succ h)⟩
State after:
no goals