appended lists equal of length equal

Stream: Is there code for X?

[Joseph Hua]

Does this exist? I want this and the other case too, when the lengths all of them are equal

lemma list.eq_of_eq_append_left {α} (l1 l2 l3 l4: list α) (h12 : l1.length = l2.length)
  (heq : l1.append l3 = l2.append l4) : l1 = l2 := sorry

[Yaël Dillies]

docs#list.append_right_cancel should help.

[Eric Wieser]

Something like docs#list.append_inj?

[Eric Wieser]

Wow, naming convention really pulled through there

[Eric Wieser]

docs#list.append_inj_left is precisely your statement, but the one I mention above might be what you actually want

[Joseph Hua]

ah perfect, thanks yall

[Eric Wieser]

Out of curiosity; would library_search have found this?

[Joseph Hua]

library_search timed out on what I wrote

[Eric Wieser]

With what imports?

[Eric Wieser]

Library search is faster (but less successful) the fewer imports you have

[Joseph Hua]

ah makes sense, yeah I have tons of imports and my computer is slowing down even without library search