case nil
ι : Type ?u.87426
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : Inhabited α
h : 0 < length []
⊢ nthLe [] 0 h = head! []

case cons
ι : Type ?u.87426
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : Inhabited α
head✝ : α
tail✝ : List α
h : 0 < length (head✝ :: tail✝)
⊢ nthLe (head✝ :: tail✝) 0 h = head! (head✝ :: tail✝)
ι : Type ?u.87426
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : Inhabited α
L : List α
h : 0 < length L
⊢ nthLe L 0 h = head! L
cases L
case cons
ι : Type ?u.87426
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : Inhabited α
head✝ : α
tail✝ : List α
h : 0 < length (head✝ :: tail✝)
⊢ nthLe (head✝ :: tail✝) 0 h = head! (head✝ :: tail✝)
case nil
ι : Type ?u.87426
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : Inhabited α
h : 0 < length []
⊢ nthLe [] 0 h = head! []

case cons
ι : Type ?u.87426
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : Inhabited α
head✝ : α
tail✝ : List α
h : 0 < length (head✝ :: tail✝)
⊢ nthLe (head✝ :: tail✝) 0 h = head! (head✝ :: tail✝)
cases h
no goals
case cons
ι : Type ?u.87426
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : Inhabited α
head✝ : α
tail✝ : List α
h : 0 < length (head✝ :: tail✝)
⊢ nthLe (head✝ :: tail✝) 0 h = head! (head✝ :: tail✝)
simp [nthLe]