no goals
ι : Type ?u.164866
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ l₁ l₂ : List α
n : ℕ
h : n ≤ length l₁
⊢ take n (l₁ ++ l₂) = take n l₁
simp [take_append_eq_append_take, tsub_eq_zero_iff_le.mpr h]