rw [length_take]
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ (take a.length (a ++ b)).length = a.length
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ a.length ≤ (a ++ b).length