case nil
ι : Type ?u.163016
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
n : ℕ
⊢ take n ([] ++ l₂) = take n [] ++ take (n - length []) l₂

case cons
ι : Type ?u.163016
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {n : ℕ}, take n (tail✝ ++ l₂) = take n tail✝ ++ take (n - length tail✝) l₂
n : ℕ
⊢ take n (head✝ :: tail✝ ++ l₂) = take n (head✝ :: tail✝) ++ take (n - length (head✝ :: tail✝)) l₂
ι : Type ?u.163016
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ l₁ l₂ : List α
n : ℕ
⊢ take n (l₁ ++ l₂) = take n l₁ ++ take (n - length l₁) l₂
induction l₁ generalizing n
case cons
ι : Type ?u.163016
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {n : ℕ}, take n (tail✝ ++ l₂) = take n tail✝ ++ take (n - length tail✝) l₂
n : ℕ
⊢ take n (head✝ :: tail✝ ++ l₂) = take n (head✝ :: tail✝) ++ take (n - length (head✝ :: tail✝)) l₂
case nil
ι : Type ?u.163016
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
n : ℕ
⊢ take n ([] ++ l₂) = take n [] ++ take (n - length []) l₂

case cons
ι : Type ?u.163016
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {n : ℕ}, take n (tail✝ ++ l₂) = take n tail✝ ++ take (n - length tail✝) l₂
n : ℕ
⊢ take n (head✝ :: tail✝ ++ l₂) = take n (head✝ :: tail✝) ++ take (n - length (head✝ :: tail✝)) l₂
{simp}
no goals
case cons
ι : Type ?u.163016
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {n : ℕ}, take n (tail✝ ++ l₂) = take n tail✝ ++ take (n - length tail✝) l₂
n : ℕ
⊢ take n (head✝ :: tail✝ ++ l₂) = take n (head✝ :: tail✝) ++ take (n - length (head✝ :: tail✝)) l₂
cases n <;> simp [*]