ι : Type ?u.158941
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ l₁ l₂ : List α
n : ℕ
h : length l₁ = n
⊢ take (length l₁) (l₁ ++ l₂) = l₁
ι : Type ?u.158941
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ l₁ l₂ : List α
n : ℕ
h : length l₁ = n
⊢ take n (l₁ ++ l₂) = l₁
rw [← h]
no goals
ι : Type ?u.158941
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ l₁ l₂ : List α
n : ℕ
h : length l₁ = n
⊢ take (length l₁) (l₁ ++ l₂) = l₁
apply take_left