Theorem: Lean4Lean.VLevel.eval_inst (Lean4Lean/Theory/VLevel.lean)

State before:
ls : List VLevel
ns : List Nat
l : VLevel
⊢ eval ns (inst ls l) = eval (List.map (eval ns) ls) l
Tactic:
induction l <;> simp [eval, inst, *, List.getD_eq_get?]
State after:
case param
ls : List VLevel
ns : List Nat
a✝ : Nat
⊢ eval ns (Option.getD (List.get? ls a✝) zero) = Option.getD (Option.map (eval ns) (List.get? ls a✝)) 0

State before:
ls : List VLevel
ns : List Nat
n : Nat
⊢ eval ns (Option.getD (List.get? ls n) zero) = Option.getD (Option.map (eval ns) (List.get? ls n)) 0
Tactic:
case param n => cases ls.get? n <;> simp [eval]
State after:
no goals

State before:
ls : List VLevel
ns : List Nat
n : Nat
⊢ eval ns (Option.getD (List.get? ls n) zero) = Option.getD (Option.map (eval ns) (List.get? ls n)) 0
Tactic:
cases ls.get? n <;> simp [eval]
State after:
no goals