apply (append_inj H3 _).2
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ drop a.length (a ++ b) = b
α : 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