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

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

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

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