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

State before:
ls : List Name
l : Lean.Level
l' : VLevel
h : ofLevel ls l = some l'
⊢ WF (List.length ls) l'
Tactic:
induction l generalizing l' with simp [ofLevel, bind, Option.bind_eq_some] at h
| zero => cases h; trivial
| succ _ ih => obtain ⟨l', h, ⟨⟩⟩ := h; exact @ih l' h
| max _ _ ih1 ih2 | imax _ _ ih1 ih2 => obtain ⟨_, h1, _, h2, ⟨⟩⟩ := h; exact ⟨ih1 h1, ih2 h2⟩
| param n => exact h.2 ▸ h.1
State after:
no goals

State before:
case zero
ls : List Name
l' : VLevel
h : zero = l'
⊢ WF (List.length ls) l'
Tactic:
cases h
State after:
case zero.refl
ls : List Name
⊢ WF (List.length ls) zero

State before:
case zero.refl
ls : List Name
⊢ WF (List.length ls) zero
Tactic:
trivial
State after:
no goals

State before:
case succ
ls : List Name
a✝ : Lean.Level
ih : ∀ {l' : VLevel}, ofLevel ls a✝ = some l' → WF (List.length ls) l'
l' : VLevel
h : ∃ a, ofLevel ls a✝ = some a ∧ succ a = l'
⊢ WF (List.length ls) l'
Tactic:
obtain ⟨l', h, ⟨⟩⟩ := h
State after:
case succ.intro.intro.refl
ls : List Name
a✝ : Lean.Level
ih : ∀ {l' : VLevel}, ofLevel ls a✝ = some l' → WF (List.length ls) l'
l' : VLevel
h : ofLevel ls a✝ = some l'
⊢ WF (List.length ls) (succ l')

State before:
case succ.intro.intro.refl
ls : List Name
a✝ : Lean.Level
ih : ∀ {l' : VLevel}, ofLevel ls a✝ = some l' → WF (List.length ls) l'
l' : VLevel
h : ofLevel ls a✝ = some l'
⊢ WF (List.length ls) (succ l')
Tactic:
exact @ih l' h
State after:
no goals

State before:
case imax
ls : List Name
a✝¹ a✝ : Lean.Level
ih1 : ∀ {l' : VLevel}, ofLevel ls a✝¹ = some l' → WF (List.length ls) l'
ih2 : ∀ {l' : VLevel}, ofLevel ls a✝ = some l' → WF (List.length ls) l'
l' : VLevel
h : ∃ a, ofLevel ls a✝¹ = some a ∧ ∃ a_1, ofLevel ls a✝ = some a_1 ∧ imax a a_1 = l'
⊢ WF (List.length ls) l'
Tactic:
obtain ⟨_, h1, _, h2, ⟨⟩⟩ := h
State after:
case imax.intro.intro.intro.intro.refl
ls : List Name
a✝¹ a✝ : Lean.Level
ih1 : ∀ {l' : VLevel}, ofLevel ls a✝¹ = some l' → WF (List.length ls) l'
ih2 : ∀ {l' : VLevel}, ofLevel ls a✝ = some l' → WF (List.length ls) l'
w✝¹ : VLevel
h1 : ofLevel ls a✝¹ = some w✝¹
w✝ : VLevel
h2 : ofLevel ls a✝ = some w✝
⊢ WF (List.length ls) (imax w✝¹ w✝)

State before:
case imax.intro.intro.intro.intro.refl
ls : List Name
a✝¹ a✝ : Lean.Level
ih1 : ∀ {l' : VLevel}, ofLevel ls a✝¹ = some l' → WF (List.length ls) l'
ih2 : ∀ {l' : VLevel}, ofLevel ls a✝ = some l' → WF (List.length ls) l'
w✝¹ : VLevel
h1 : ofLevel ls a✝¹ = some w✝¹
w✝ : VLevel
h2 : ofLevel ls a✝ = some w✝
⊢ WF (List.length ls) (imax w✝¹ w✝)
Tactic:
exact ⟨ih1 h1, ih2 h2⟩
State after:
no goals

State before:
case param
ls : List Name
n : Name
l' : VLevel
h : List.indexOf n ls < List.length ls ∧ param (List.indexOf n ls) = l'
⊢ WF (List.length ls) l'
Tactic:
exact h.2 ▸ h.1
State after:
no goals