no goals
ι : Type ?u.45408
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
i : ℕ
h : i < length (tail l)
⊢ i + 1 < length l
simpa [← lt_tsub_iff_right] using h
case nil
ι : Type ?u.45408
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
i : ℕ
h : i < length (tail [])
h' : optParam (i + 1 < length []) (_ : i + 1 < length [])
⊢ nthLe (tail []) i h = nthLe [] (i + 1) h'

case cons
ι : Type ?u.45408
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
i : ℕ
head✝ : α
tail✝ : List α
h : i < length (tail (head✝ :: tail✝))
h' : optParam (i + 1 < length (head✝ :: tail✝)) (_ : i + 1 < length (head✝ :: tail✝))
⊢ nthLe (tail (head✝ :: tail✝)) i h = nthLe (head✝ :: tail✝) (i + 1) h'
ι : Type ?u.45408
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
i : ℕ
h : i < length (tail l)
h' : optParam (i + 1 < length l) (_ : i + 1 < length l)
⊢ nthLe (tail l) i h = nthLe l (i + 1) h'
cases l
no goals
case nil
ι : Type ?u.45408
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
i : ℕ
h : i < length (tail [])
h' : optParam (i + 1 < length []) (_ : i + 1 < length [])
⊢ nthLe (tail []) i h = nthLe [] (i + 1) h'
cases h
no goals
case cons
ι : Type ?u.45408
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
i : ℕ
head✝ : α
tail✝ : List α
h : i < length (tail (head✝ :: tail✝))
h' : optParam (i + 1 < length (head✝ :: tail✝)) (_ : i + 1 < length (head✝ :: tail✝))
⊢ nthLe (tail (head✝ :: tail✝)) i h = nthLe (head✝ :: tail✝) (i + 1) h'
rfl