List.append can equal the lhs (or rhs) only if rhs = []

Stream: Is there code for X?

[Andrew Carter]

Its easy to write the proof for, but I was surprised that I couldn't find it on either loogle or exact?. In fact I kind of would expect it to be a simp lemma since it seems simplifying to me.

def List.append_self_iff_eq_nil {α: Type _} {x y: List α}: (x = y ++ x) ↔ (y = []) :=
  ⟨ λ h ↦ List.eq_nil_of_length_eq_zero
    (Nat.add_right_cancel (m := List.length x) (Nat.zero_add _ ▸ List.length_append _ _ ▸ congrArg List.length h)).symm,
  λ h ↦ h ▸ rfl ⟩

[Yaël Dillies]

That should be a simp lemma, although it would rather be stated as lemma append_eq_left : x ++ y = x ↔ y = [] and lemma append_eq_right : x ++ y = y ↔ x = []