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

State before:
n : Nat
e : VExpr
j k : Nat
self : ClosedN (liftN n e j) 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 =>
  refine liftVar_lt (Nat.lt_of_lt_of_le ?_ h)
  unfold liftVar at self; split at self <;>
    [exact self; exact Nat.lt_of_le_of_lt (Nat.le_add_left ..) self]
| 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
j k : Nat
self : ClosedN (liftN n (const declName✝ us✝) j) 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
j k : 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
j k : 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 j k : Nat
self : liftVar n i j < k
h : k ≤ j
⊢ liftVar n i j = i
Tactic:
refine liftVar_lt (Nat.lt_of_lt_of_le ?_ h)
State after:
case bvar
n i j k : Nat
self : liftVar n i j < k
h : k ≤ j
⊢ i < k

State before:
case bvar
n i j k : Nat
self : liftVar n i j < k
h : k ≤ j
⊢ i < k
Tactic:
unfold liftVar at self
State after:
case bvar
n i j k : Nat
self : (if i < j then i else n + i) < k
h : k ≤ j
⊢ i < k

State before:
case bvar
n i j k : Nat
self : (if i < j then i else n + i) < k
h : k ≤ j
⊢ i < k
Tactic:
split at self <;>
[exact self; exact Nat.lt_of_le_of_lt (Nat.le_add_left ..) self]
State after:
no goals

State before:
case app
n : Nat
fn✝ arg✝ : VExpr
ih1 : ∀ {j k : Nat}, ClosedN (liftN n fn✝ j) k → k ≤ j → liftN n fn✝ j = fn✝
ih2 : ∀ {j k : Nat}, ClosedN (liftN n arg✝ j) k → k ≤ j → liftN n arg✝ j = arg✝
j k : Nat
self : ClosedN (liftN n fn✝ j) k ∧ ClosedN (liftN n arg✝ j) 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 : ∀ {j k : Nat}, ClosedN (liftN n binderType✝ j) k → k ≤ j → liftN n binderType✝ j = binderType✝
ih2 : ∀ {j k : Nat}, ClosedN (liftN n body✝ j) k → k ≤ j → liftN n body✝ j = body✝
j k : Nat
self : ClosedN (liftN n binderType✝ j) k ∧ ClosedN (liftN n body✝ (j + 1)) (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