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

State before:
ls : List VLevel
e : VExpr
n k : Nat
⊢ instL ls (unliftN e n k) = unliftN (instL ls e) n k
Tactic:
induction n generalizing e with simp [unliftN]
| succ _ ih => rw [ih, instL_instN]; rfl
State after:
no goals

State before:
case succ
ls : List VLevel
k n✝ : Nat
ih : ∀ {e : VExpr}, instL ls (unliftN e n✝ k) = unliftN (instL ls e) n✝ k
e : VExpr
⊢ instL ls (unliftN (inst e default k) n✝ k) = unliftN (inst (instL ls e) default k) n✝ k
Tactic:
rw [ih, instL_instN]
State after:
case succ
ls : List VLevel
k n✝ : Nat
ih : ∀ {e : VExpr}, instL ls (unliftN e n✝ k) = unliftN (instL ls e) n✝ k
e : VExpr
⊢ unliftN (inst (instL ls e) (instL ls default) k) n✝ k = unliftN (inst (instL ls e) default k) n✝ k

State before:
case succ
ls : List VLevel
k n✝ : Nat
ih : ∀ {e : VExpr}, instL ls (unliftN e n✝ k) = unliftN (instL ls e) n✝ k
e : VExpr
⊢ unliftN (inst (instL ls e) (instL ls default) k) n✝ k = unliftN (inst (instL ls e) default k) n✝ k
Tactic:
rfl
State after:
no goals