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