case nil
ι : Type ?u.175545
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n✝ n : ℕ
⊢ take (n + 1) [] = take n [] ++ Option.toList (get? [] n)

case cons
ι : Type ?u.175545
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n✝ : ℕ
hd : α
tl : List α
hl : ∀ {n : ℕ}, take (n + 1) tl = take n tl ++ Option.toList (get? tl n)
n : ℕ
⊢ take (n + 1) (hd :: tl) = take n (hd :: tl) ++ Option.toList (get? (hd :: tl) n)
ι : Type ?u.175545
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n : ℕ
⊢ take (n + 1) l = take n l ++ Option.toList (get? l n)
induction' l with hd tl hl generalizing n
no goals
case nil
ι : Type ?u.175545
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n✝ n : ℕ
⊢ take (n + 1) [] = take n [] ++ Option.toList (get? [] n)
simp only [Option.toList, get?, take_nil, append_nil]
case cons.zero
ι : Type ?u.175545
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
hd : α
tl : List α
hl : ∀ {n : ℕ}, take (n + 1) tl = take n tl ++ Option.toList (get? tl n)
⊢ take (zero + 1) (hd :: tl) = take zero (hd :: tl) ++ Option.toList (get? (hd :: tl) zero)

case cons.succ
ι : Type ?u.175545
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
hd : α
tl : List α
hl : ∀ {n : ℕ}, take (n + 1) tl = take n tl ++ Option.toList (get? tl n)
n✝ : ℕ
⊢ take (succ n✝ + 1) (hd :: tl) = take (succ n✝) (hd :: tl) ++ Option.toList (get? (hd :: tl) (succ n✝))
case cons
ι : Type ?u.175545
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n✝ : ℕ
hd : α
tl : List α
hl : ∀ {n : ℕ}, take (n + 1) tl = take n tl ++ Option.toList (get? tl n)
n : ℕ
⊢ take (n + 1) (hd :: tl) = take n (hd :: tl) ++ Option.toList (get? (hd :: tl) n)
cases n
no goals
case cons.zero
ι : Type ?u.175545
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
hd : α
tl : List α
hl : ∀ {n : ℕ}, take (n + 1) tl = take n tl ++ Option.toList (get? tl n)
⊢ take (zero + 1) (hd :: tl) = take zero (hd :: tl) ++ Option.toList (get? (hd :: tl) zero)
simp only [Option.toList, get?, eq_self_iff_true, and_self_iff, take, nil_append]
no goals
case cons.succ
ι : Type ?u.175545
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
hd : α
tl : List α
hl : ∀ {n : ℕ}, take (n + 1) tl = take n tl ++ Option.toList (get? tl n)
n✝ : ℕ
⊢ take (succ n✝ + 1) (hd :: tl) = take (succ n✝) (hd :: tl) ++ Option.toList (get? (hd :: tl) (succ n✝))
simp only [hl, cons_append, get?, eq_self_iff_true, and_self_iff, take]