case intro
α : Type u_1
β : Type ?u.3302
l l₁ l₃ : List α
a b : α
m n : ℕ
r : List α
⊢ take (length (r ++ l₁) - length l₁) (r ++ l₁) ++ l₁ = r ++ l₁
α : Type u_1
β : Type ?u.3302
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ l₁ <:+ l₂ → take (length l₂ - length l₁) l₂ ++ l₁ = l₂
rintro ⟨r, rfl⟩
no goals
case intro
α : Type u_1
β : Type ?u.3302
l l₁ l₃ : List α
a b : α
m n : ℕ
r : List α
⊢ take (length (r ++ l₁) - length l₁) (r ++ l₁) ++ l₁ = r ++ l₁
simp only [length_append, add_tsub_cancel_right, take_left]