case nil
α : Type u_1
β : Type ?u.7170
L : List α
i✝ : Fin (length L)
i : Fin (length [])
⊢ drop (↑i) (take (↑i + 1) []) = [get [] i]

case cons
α : Type u_1
β : Type ?u.7170
L : List α
i✝ : Fin (length L)
head : α
tail : List α
ih : ∀ (i : Fin (length tail)), drop (↑i) (take (↑i + 1) tail) = [get tail i]
i : Fin (length (head :: tail))
⊢ drop (↑i) (take (↑i + 1) (head :: tail)) = [get (head :: tail) i]
α : Type u_1
β : Type ?u.7170
L : List α
i : Fin (length L)
⊢ drop (↑i) (take (↑i + 1) L) = [get L i]
induction' L with head tail ih
case cons.mk.zero
α : Type u_1
β : Type ?u.7170
L : List α
i : Fin (length L)
head : α
tail : List α
ih : ∀ (i : Fin (length tail)), drop (↑i) (take (↑i + 1) tail) = [get tail i]
hi : Nat.zero < length (head :: tail)
⊢ drop (↑{ val := Nat.zero, isLt := hi }) (take (↑{ val := Nat.zero, isLt := hi } + 1) (head :: tail)) =
    [get (head :: tail) { val := Nat.zero, isLt := hi }]

case cons.mk.succ
α : Type u_1
β : Type ?u.7170
L : List α
i✝ : Fin (length L)
head : α
tail : List α
ih : ∀ (i : Fin (length tail)), drop (↑i) (take (↑i + 1) tail) = [get tail i]
i : ℕ
hi : Nat.succ i < length (head :: tail)
⊢ drop (↑{ val := Nat.succ i, isLt := hi }) (take (↑{ val := Nat.succ i, isLt := hi } + 1) (head :: tail)) =
    [get (head :: tail) { val := Nat.succ i, isLt := hi }]
case cons
α : Type u_1
β : Type ?u.7170
L : List α
i✝ : Fin (length L)
head : α
tail : List α
ih : ∀ (i : Fin (length tail)), drop (↑i) (take (↑i + 1) tail) = [get tail i]
i : Fin (length (head :: tail))
⊢ drop (↑i) (take (↑i + 1) (head :: tail)) = [get (head :: tail) i]
rcases i with ⟨_ | i, hi⟩
no goals
case nil
α : Type u_1
β : Type ?u.7170
L : List α
i✝ : Fin (length L)
i : Fin (length [])
⊢ drop (↑i) (take (↑i + 1) []) = [get [] i]
exact (Nat.not_succ_le_zero i i.isLt).elim
no goals
case cons.mk.zero
α : Type u_1
β : Type ?u.7170
L : List α
i : Fin (length L)
head : α
tail : List α
ih : ∀ (i : Fin (length tail)), drop (↑i) (take (↑i + 1) tail) = [get tail i]
hi : Nat.zero < length (head :: tail)
⊢ drop (↑{ val := Nat.zero, isLt := hi }) (take (↑{ val := Nat.zero, isLt := hi } + 1) (head :: tail)) =
    [get (head :: tail) { val := Nat.zero, isLt := hi }]
simp
no goals
case cons.mk.succ
α : Type u_1
β : Type ?u.7170
L : List α
i✝ : Fin (length L)
head : α
tail : List α
ih : ∀ (i : Fin (length tail)), drop (↑i) (take (↑i + 1) tail) = [get tail i]
i : ℕ
hi : Nat.succ i < length (head :: tail)
⊢ drop (↑{ val := Nat.succ i, isLt := hi }) (take (↑{ val := Nat.succ i, isLt := hi } + 1) (head :: tail)) =
    [get (head :: tail) { val := Nat.succ i, isLt := hi }]
simpa using ih ⟨i, Nat.lt_of_succ_lt_succ hi⟩