no goals
ι : Type ?u.165438
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ l₁ l₂ : List α
i : ℕ
⊢ take (length l₁ + i) (l₁ ++ l₂) = l₁ ++ take i l₂
simp [take_append_eq_append_take, take_all_of_le le_self_add]