case inl
ι : Type ?u.48326
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
a : α
n : ℕ
hl : n < length (a :: l)
h : n = 0
⊢ nthLe (a :: l) n hl = a

case inr
ι : Type ?u.48326
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
a : α
n : ℕ
hl : n < length (a :: l)
h : ¬n = 0
⊢ nthLe (a :: l) n hl = nthLe l (n - 1) (_ : n - 1 < length l)
ι : Type ?u.48326
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
a : α
n : ℕ
hl : n < length (a :: l)
⊢ nthLe (a :: l) n hl = if hn : n = 0 then a else nthLe l (n - 1) (_ : n - 1 < length l)
split_ifs with h
case inr.nil
ι : Type ?u.48326
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
n : ℕ
h : ¬n = 0
hl : n < length [a]
⊢ nthLe [a] n hl = nthLe [] (n - 1) (_ : n - 1 < length [])

case inr.cons
ι : Type ?u.48326
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
n : ℕ
h : ¬n = 0
head✝ : α
tail✝ : List α
hl : n < length (a :: head✝ :: tail✝)
⊢ nthLe (a :: head✝ :: tail✝) n hl = nthLe (head✝ :: tail✝) (n - 1) (_ : n - 1 < length (head✝ :: tail✝))
case inr
ι : Type ?u.48326
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
a : α
n : ℕ
hl : n < length (a :: l)
h : ¬n = 0
⊢ nthLe (a :: l) n hl = nthLe l (n - 1) (_ : n - 1 < length l)
cases l
case inr.cons.zero
ι : Type ?u.48326
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a head✝ : α
tail✝ : List α
h : ¬zero = 0
hl : zero < length (a :: head✝ :: tail✝)
⊢ nthLe (a :: head✝ :: tail✝) zero hl = nthLe (head✝ :: tail✝) (zero - 1) (_ : zero - 1 < length (head✝ :: tail✝))

case inr.cons.succ
ι : Type ?u.48326
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a head✝ : α
tail✝ : List α
n✝ : ℕ
h : ¬succ n✝ = 0
hl : succ n✝ < length (a :: head✝ :: tail✝)
⊢ nthLe (a :: head✝ :: tail✝) (succ n✝) hl =
    nthLe (head✝ :: tail✝) (succ n✝ - 1) (_ : succ n✝ - 1 < length (head✝ :: tail✝))
case inr.cons
ι : Type ?u.48326
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
n : ℕ
h : ¬n = 0
head✝ : α
tail✝ : List α
hl : n < length (a :: head✝ :: tail✝)
⊢ nthLe (a :: head✝ :: tail✝) n hl = nthLe (head✝ :: tail✝) (n - 1) (_ : n - 1 < length (head✝ :: tail✝))
cases n
no goals
case inr.cons.succ
ι : Type ?u.48326
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a head✝ : α
tail✝ : List α
n✝ : ℕ
h : ¬succ n✝ = 0
hl : succ n✝ < length (a :: head✝ :: tail✝)
⊢ nthLe (a :: head✝ :: tail✝) (succ n✝) hl =
    nthLe (head✝ :: tail✝) (succ n✝ - 1) (_ : succ n✝ - 1 < length (head✝ :: tail✝))
rfl
no goals
case inl
ι : Type ?u.48326
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
a : α
n : ℕ
hl : n < length (a :: l)
h : n = 0
⊢ nthLe (a :: l) n hl = a
simp [nthLe, h]
case inr.nil
ι : Type ?u.48326
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
n : ℕ
h : ¬n = 0
hl✝ : n < length [a]
hl : n = 0
⊢ nthLe [a] n hl✝ = nthLe [] (n - 1) (_ : n - 1 < length [])
case inr.nil
ι : Type ?u.48326
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
n : ℕ
h : ¬n = 0
hl : n < length [a]
⊢ nthLe [a] n hl = nthLe [] (n - 1) (_ : n - 1 < length [])
rw [length_singleton, lt_succ_iff, nonpos_iff_eq_zero] at hl
no goals
case inr.nil
ι : Type ?u.48326
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
n : ℕ
h : ¬n = 0
hl✝ : n < length [a]
hl : n = 0
⊢ nthLe [a] n hl✝ = nthLe [] (n - 1) (_ : n - 1 < length [])
contradiction
no goals
case inr.cons.zero
ι : Type ?u.48326
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a head✝ : α
tail✝ : List α
h : ¬zero = 0
hl : zero < length (a :: head✝ :: tail✝)
⊢ nthLe (a :: head✝ :: tail✝) zero hl = nthLe (head✝ :: tail✝) (zero - 1) (_ : zero - 1 < length (head✝ :: tail✝))
contradiction