case intro
α : Type u_1
β : Type ?u.3114
l l₁ l₃ : List α
a b : α
m n : ℕ
r : List α
⊢ l₁ ++ drop (length l₁) (l₁ ++ r) = l₁ ++ r
α : Type u_1
β : Type ?u.3114
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ l₁ <+: l₂ → l₁ ++ drop (length l₁) l₂ = l₂
rintro ⟨r, rfl⟩
no goals
case intro
α : Type u_1
β : Type ?u.3114
l l₁ l₃ : List α
a b : α
m n : ℕ
r : List α
⊢ l₁ ++ drop (length l₁) (l₁ ++ r) = l₁ ++ r
rw [drop_left]