Theorem: Lean4Lean.VLevel.WF.inst (Lean4Lean/Theory/VLevel.lean)

State before:
ls : List VLevel
n : Nat
l : VLevel
H : ∀ (l : VLevel), l ∈ ls → WF n l
⊢ WF n (VLevel.inst ls l)
Tactic:
induction l with
| zero => trivial
| succ _ ih => exact ih
| max _ _ ih1 ih2 | imax _ _ ih1 ih2 => exact ⟨ih1, ih2⟩
| param i =>
  simp [VLevel.inst, List.getD_eq_get?]
  cases e : ls.get? i with
  | none => trivial
  | some => exact H _ (List.get?_mem e)
State after:
no goals

State before:
case zero
ls : List VLevel
n : Nat
H : ∀ (l : VLevel), l ∈ ls → WF n l
⊢ WF n (VLevel.inst ls zero)
Tactic:
trivial
State after:
no goals

State before:
case succ
ls : List VLevel
n : Nat
H : ∀ (l : VLevel), l ∈ ls → WF n l
a✝ : VLevel
ih : WF n (VLevel.inst ls a✝)
⊢ WF n (VLevel.inst ls (succ a✝))
Tactic:
exact ih
State after:
no goals

State before:
case imax
ls : List VLevel
n : Nat
H : ∀ (l : VLevel), l ∈ ls → WF n l
a✝¹ a✝ : VLevel
ih1 : WF n (VLevel.inst ls a✝¹)
ih2 : WF n (VLevel.inst ls a✝)
⊢ WF n (VLevel.inst ls (imax a✝¹ a✝))
Tactic:
exact ⟨ih1, ih2⟩
State after:
no goals

State before:
case param
ls : List VLevel
n : Nat
H : ∀ (l : VLevel), l ∈ ls → WF n l
i : Nat
⊢ WF n (VLevel.inst ls (param i))
Tactic:
simp [VLevel.inst, List.getD_eq_get?]
State after:
case param
ls : List VLevel
n : Nat
H : ∀ (l : VLevel), l ∈ ls → WF n l
i : Nat
⊢ WF n (Option.getD (List.get? ls i) zero)

State before:
case param
ls : List VLevel
n : Nat
H : ∀ (l : VLevel), l ∈ ls → WF n l
i : Nat
⊢ WF n (Option.getD (List.get? ls i) zero)
Tactic:
cases e : ls.get? i with
| none => trivial
| some => exact H _ (List.get?_mem e)
State after:
no goals

State before:
case param.none
ls : List VLevel
n : Nat
H : ∀ (l : VLevel), l ∈ ls → WF n l
i : Nat
e : List.get? ls i = none
⊢ WF n (Option.getD none zero)
Tactic:
trivial
State after:
no goals

State before:
case param.some
ls : List VLevel
n : Nat
H : ∀ (l : VLevel), l ∈ ls → WF n l
i : Nat
val✝ : VLevel
e : List.get? ls i = some val✝
⊢ WF n (Option.getD (some val✝) zero)
Tactic:
exact H _ (List.get?_mem e)
State after:
no goals