case nil
ι : Type ?u.200056
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝ : Fin (length l)
n : Fin (length [])
⊢ get [] n :: drop (↑n + 1) [] = drop ↑n []

case cons
ι : Type ?u.200056
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝ : Fin (length l)
hd : α
tl : List α
hl : ∀ {n : Fin (length tl)}, get tl n :: drop (↑n + 1) tl = drop (↑n) tl
n : Fin (length (hd :: tl))
⊢ get (hd :: tl) n :: drop (↑n + 1) (hd :: tl) = drop (↑n) (hd :: tl)
ι : Type ?u.200056
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n : Fin (length l)
⊢ get l n :: drop (↑n + 1) l = drop (↑n) l
induction' l with hd tl hl
no goals
case nil
ι : Type ?u.200056
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝ : Fin (length l)
n : Fin (length [])
⊢ get [] n :: drop (↑n + 1) [] = drop ↑n []
exact absurd n.1.zero_le (not_le_of_lt (nomatch n))
no goals
case cons
ι : Type ?u.200056
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝ : Fin (length l)
hd : α
tl : List α
hl : ∀ {n : Fin (length tl)}, get tl n :: drop (↑n + 1) tl = drop (↑n) tl
n : Fin (length (hd :: tl))
⊢ get (hd :: tl) n :: drop (↑n + 1) (hd :: tl) = drop (↑n) (hd :: tl)
match n with
| ⟨0, _⟩ => simp [get]
| ⟨n+1, hn⟩ =>
  simp only [Nat.succ_lt_succ_iff, List.length] at hn
  simpa [List.get, List.drop] using hl
no goals
ι : Type ?u.200056
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝ : Fin (length l)
hd : α
tl : List α
hl : ∀ {n : Fin (length tl)}, get tl n :: drop (↑n + 1) tl = drop (↑n) tl
n : Fin (length (hd :: tl))
isLt✝ : 0 < length (hd :: tl)
⊢ get (hd :: tl) { val := 0, isLt := isLt✝ } :: drop (↑{ val := 0, isLt := isLt✝ } + 1) (hd :: tl) =
    drop (↑{ val := 0, isLt := isLt✝ }) (hd :: tl)
simp [get]
ι : Type ?u.200056
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝¹ : Fin (length l)
hd : α
tl : List α
hl : ∀ {n : Fin (length tl)}, get tl n :: drop (↑n + 1) tl = drop (↑n) tl
n✝ : Fin (length (hd :: tl))
n : ℕ
hn✝ : n + 1 < length (hd :: tl)
hn : n < length tl
⊢ get (hd :: tl) { val := n + 1, isLt := hn✝ } :: drop (↑{ val := n + 1, isLt := hn✝ } + 1) (hd :: tl) =
    drop (↑{ val := n + 1, isLt := hn✝ }) (hd :: tl)
ι : Type ?u.200056
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝¹ : Fin (length l)
hd : α
tl : List α
hl : ∀ {n : Fin (length tl)}, get tl n :: drop (↑n + 1) tl = drop (↑n) tl
n✝ : Fin (length (hd :: tl))
n : ℕ
hn : n + 1 < length (hd :: tl)
⊢ get (hd :: tl) { val := n + 1, isLt := hn } :: drop (↑{ val := n + 1, isLt := hn } + 1) (hd :: tl) =
    drop (↑{ val := n + 1, isLt := hn }) (hd :: tl)
simp only [Nat.succ_lt_succ_iff, List.length] at hn
no goals
ι : Type ?u.200056
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝¹ : Fin (length l)
hd : α
tl : List α
hl : ∀ {n : Fin (length tl)}, get tl n :: drop (↑n + 1) tl = drop (↑n) tl
n✝ : Fin (length (hd :: tl))
n : ℕ
hn✝ : n + 1 < length (hd :: tl)
hn : n < length tl
⊢ get (hd :: tl) { val := n + 1, isLt := hn✝ } :: drop (↑{ val := n + 1, isLt := hn✝ } + 1) (hd :: tl) =
    drop (↑{ val := n + 1, isLt := hn✝ }) (hd :: tl)
simpa [List.get, List.drop] using hl