feat: more lemmas about List.append (#5131)

src/Init/Data/List/Lemmas.lean

@@ -1430,6 +1430,18 @@ theorem append_right_inj {t₁ t₂ : List α} (s) : s ++ t₁ = s ++ t₂ ↔ t
 theorem append_left_inj {s₁ s₂ : List α} (t) : s₁ ++ t = s₂ ++ t ↔ s₁ = s₂ :=
   ⟨fun h => append_inj_left' h rfl, congrArg (· ++ _)⟩
 
+@[simp] theorem append_left_eq_self {x y : List α} : x ++ y = y ↔ x = [] := by
+  rw [← append_left_inj (s₁ := x), nil_append]
+
+@[simp] theorem self_eq_append_left {x y : List α} : y = x ++ y ↔ x = [] := by
+  rw [eq_comm, append_left_eq_self]
+
+@[simp] theorem append_right_eq_self {x y : List α} : x ++ y = x ↔ y = [] := by
+  rw [← append_right_inj (t₁ := y), append_nil]
+
+@[simp] theorem self_eq_append_right {x y : List α} : x = x ++ y ↔ y = [] := by
+  rw [eq_comm, append_right_eq_self]
+
 @[simp] theorem append_eq_nil : p ++ q = [] ↔ p = [] ∧ q = [] := by
   cases p <;> simp
 

src/Init/Data/List/Nat/Sublist.lean

@@ -126,4 +126,49 @@ theorem prefix_take_le_iff {L : List α} (hm : m < L.length) :
         simp only [length_cons, Nat.succ_eq_add_one, Nat.add_lt_add_iff_right] at hm
         simp [← @IH n ls hm, Nat.min_eq_left, Nat.le_of_lt hm]
 
+@[simp] theorem append_left_sublist_self (xs ys : List α) : xs ++ ys <+ ys ↔ xs = [] := by
+  constructor
+  · intro h
+    replace h := h.length_le
+    simp only [length_append] at h
+    have : xs.length = 0 := by omega
+    simp_all
+  · rintro rfl
+    simp
+@[simp] theorem append_right_sublist_self (xs ys : List α) : xs ++ ys <+ xs ↔ ys = [] := by
+  constructor
+  · intro h
+    replace h := h.length_le
+    simp only [length_append] at h
+    have : ys.length = 0 := by omega
+    simp_all
+  · rintro rfl
+    simp
+
+theorem append_sublist_of_sublist_left (xs ys zs : List α) (h : zs <+ xs) :
+    xs ++ ys <+ zs ↔ ys = [] ∧ xs = zs := by
+  constructor
+  · intro h'
+    have hl := h.length_le
+    have hl' := h'.length_le
+    simp only [length_append] at hl'
+    have : ys.length = 0 := by omega
+    simp_all only [Nat.add_zero, length_eq_zero, true_and, append_nil]
+    exact Sublist.eq_of_length_le h' hl
+  · rintro ⟨rfl, rfl⟩
+    simp
+
+theorem append_sublist_of_sublist_right (xs ys zs : List α) (h : zs <+ ys) :
+    xs ++ ys <+ zs ↔ xs = [] ∧ ys = zs := by
+  constructor
+  · intro h'
+    have hl := h.length_le
+    have hl' := h'.length_le
+    simp only [length_append] at hl'
+    have : xs.length = 0 := by omega
+    simp_all only [Nat.zero_add, length_eq_zero, true_and, append_nil]
+    exact Sublist.eq_of_length_le h' hl
+  · rintro ⟨rfl, rfl⟩
+    simp
+
 end List