case nil
α : Type u_1
β : Type ?u.8051
L : List α
i✝ : ℕ
hi✝ : i✝ < length L
i : ℕ
hi : i < length []
⊢ drop i (take (i + 1) []) = [nthLe [] i hi]

case cons
α : Type u_1
β : Type ?u.8051
L : List α
i✝ : ℕ
hi✝ : i✝ < length L
head : α
tail : List α
tail_ih✝ : ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]
i : ℕ
hi : i < length (head :: tail)
⊢ drop i (take (i + 1) (head :: tail)) = [nthLe (head :: tail) i hi]
α : Type u_1
β : Type ?u.8051
L : List α
i : ℕ
hi : i < length L
⊢ drop i (take (i + 1) L) = [nthLe L i hi]
induction' L with head tail generalizing i
case cons.zero
α : Type u_1
β : Type ?u.8051
L : List α
i : ℕ
hi✝ : i < length L
head : α
tail : List α
tail_ih✝ : ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]
hi : Nat.zero < length (head :: tail)
⊢ drop Nat.zero (take (Nat.zero + 1) (head :: tail)) = [nthLe (head :: tail) Nat.zero hi]

case cons.succ
α : Type u_1
β : Type ?u.8051
L : List α
i✝ : ℕ
hi✝ : i✝ < length L
head : α
tail : List α
tail_ih✝ : ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]
i : ℕ
hi : Nat.succ i < length (head :: tail)
⊢ drop (Nat.succ i) (take (Nat.succ i + 1) (head :: tail)) = [nthLe (head :: tail) (Nat.succ i) hi]
case cons
α : Type u_1
β : Type ?u.8051
L : List α
i✝ : ℕ
hi✝ : i✝ < length L
head : α
tail : List α
tail_ih✝ : ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]
i : ℕ
hi : i < length (head :: tail)
⊢ drop i (take (i + 1) (head :: tail)) = [nthLe (head :: tail) i hi]
cases' i with i hi
case cons.succ
α : Type u_1
β : Type ?u.8051
L : List α
i✝ : ℕ
hi✝ : i✝ < length L
head : α
tail : List α
tail_ih✝ : ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]
i : ℕ
hi : Nat.succ i < length (head :: tail)
this : i < length tail
⊢ drop (Nat.succ i) (take (Nat.succ i + 1) (head :: tail)) = [nthLe (head :: tail) (Nat.succ i) hi]
case cons.succ
α : Type u_1
β : Type ?u.8051
L : List α
i✝ : ℕ
hi✝ : i✝ < length L
head : α
tail : List α
tail_ih✝ : ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]
i : ℕ
hi : Nat.succ i < length (head :: tail)
⊢ drop (Nat.succ i) (take (Nat.succ i + 1) (head :: tail)) = [nthLe (head :: tail) (Nat.succ i) hi]
have : i < tail.length := by
  simp at hi
  exact Nat.lt_of_succ_lt_succ hi
case cons.succ
α : Type u_1
β : Type ?u.8051
L : List α
i✝ : ℕ
hi✝ : i✝ < length L
head : α
tail : List α
tail_ih✝ : ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]
i : ℕ
hi : Nat.succ i < length (head :: tail)
this : i < length tail
⊢ nthLe tail i (_ : i < length tail) = nthLe (head :: tail) (Nat.succ i) hi
case cons.succ
α : Type u_1
β : Type ?u.8051
L : List α
i✝ : ℕ
hi✝ : i✝ < length L
head : α
tail : List α
tail_ih✝ : ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]
i : ℕ
hi : Nat.succ i < length (head :: tail)
this : i < length tail
⊢ drop (Nat.succ i) (take (Nat.succ i + 1) (head :: tail)) = [nthLe (head :: tail) (Nat.succ i) hi]
simp [*]
no goals
case cons.succ
α : Type u_1
β : Type ?u.8051
L : List α
i✝ : ℕ
hi✝ : i✝ < length L
head : α
tail : List α
tail_ih✝ : ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]
i : ℕ
hi : Nat.succ i < length (head :: tail)
this : i < length tail
⊢ nthLe tail i (_ : i < length tail) = nthLe (head :: tail) (Nat.succ i) hi
rfl
case nil
α : Type u_1
β : Type ?u.8051
L : List α
i✝ : ℕ
hi✝ : i✝ < length L
i : ℕ
hi : i < 0
⊢ drop i (take (i + 1) []) = [nthLe [] i hi]
case nil
α : Type u_1
β : Type ?u.8051
L : List α
i✝ : ℕ
hi✝ : i✝ < length L
i : ℕ
hi : i < length []
⊢ drop i (take (i + 1) []) = [nthLe [] i hi]
simp only [length] at hi
no goals
case nil
α : Type u_1
β : Type ?u.8051
L : List α
i✝ : ℕ
hi✝ : i✝ < length L
i : ℕ
hi : i < 0
⊢ drop i (take (i + 1) []) = [nthLe [] i hi]
exact (Nat.not_succ_le_zero i hi).elim
case cons.zero
α : Type u_1
β : Type ?u.8051
L : List α
i : ℕ
hi✝ : i < length L
head : α
tail : List α
tail_ih✝ : ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]
hi : Nat.zero < length (head :: tail)
⊢ head = nthLe (head :: tail) 0 hi
case cons.zero
α : Type u_1
β : Type ?u.8051
L : List α
i : ℕ
hi✝ : i < length L
head : α
tail : List α
tail_ih✝ : ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]
hi : Nat.zero < length (head :: tail)
⊢ drop Nat.zero (take (Nat.zero + 1) (head :: tail)) = [nthLe (head :: tail) Nat.zero hi]
simp
no goals
case cons.zero
α : Type u_1
β : Type ?u.8051
L : List α
i : ℕ
hi✝ : i < length L
head : α
tail : List α
tail_ih✝ : ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]
hi : Nat.zero < length (head :: tail)
⊢ head = nthLe (head :: tail) 0 hi
rfl
α : Type u_1
β : Type ?u.8051
L : List α
i✝ : ℕ
hi✝ : i✝ < length L
head : α
tail : List α
tail_ih✝ : ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]
i : ℕ
hi : Nat.succ i < Nat.succ (length tail)
⊢ i < length tail
α : Type u_1
β : Type ?u.8051
L : List α
i✝ : ℕ
hi✝ : i✝ < length L
head : α
tail : List α
tail_ih✝ : ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]
i : ℕ
hi : Nat.succ i < length (head :: tail)
⊢ i < length tail
simp at hi
no goals
α : Type u_1
β : Type ?u.8051
L : List α
i✝ : ℕ
hi✝ : i✝ < length L
head : α
tail : List α
tail_ih✝ : ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]
i : ℕ
hi : Nat.succ i < Nat.succ (length tail)
⊢ i < length tail
exact Nat.lt_of_succ_lt_succ hi