Theorem: Lean4Lean.VExpr.LevelWF.inst (Lean4Lean/Theory/VExpr.lean)

State before:
e1 e2 : VExpr
k U : Nat
h1 : LevelWF U e1
h2 : LevelWF U e2
⊢ LevelWF U (inst e1 e2 k)
Tactic:
induction e1 generalizing k <;> simp_all [inst, instVar, LevelWF]
State after:
case bvar
e2 : VExpr
U : Nat
h2 : LevelWF U e2
deBruijnIndex✝ k : Nat
⊢ LevelWF U
    (if deBruijnIndex✝ < k then bvar deBruijnIndex✝
    else if deBruijnIndex✝ = k then VExpr.liftN k e2 else bvar (deBruijnIndex✝ - 1))

State before:
e2 : VExpr
U : Nat
h2 : LevelWF U e2
deBruijnIndex✝ k : Nat
⊢ LevelWF U
    (if deBruijnIndex✝ < k then bvar deBruijnIndex✝
    else if deBruijnIndex✝ = k then VExpr.liftN k e2 else bvar (deBruijnIndex✝ - 1))
Tactic:
case bvar => split <;> [trivial; split <;> [exact h2.liftN; trivial]]
State after:
no goals

State before:
e2 : VExpr
U : Nat
h2 : LevelWF U e2
deBruijnIndex✝ k : Nat
⊢ LevelWF U
    (if deBruijnIndex✝ < k then bvar deBruijnIndex✝
    else if deBruijnIndex✝ = k then VExpr.liftN k e2 else bvar (deBruijnIndex✝ - 1))
Tactic:
split <;> [trivial; split <;> [exact h2.liftN; trivial]]
State after:
no goals