From df3a8eb1264cb7e22fb7fe6f98b885bb4ea317ad Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 30 Mar 2022 11:11:03 -0700
Subject: [PATCH] feat: add helper `List.append` `simp` theorems

---
 src/Init/Data/List/BasicAux.lean | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean
index 234a5f94b4..7b4586d80d 100644
--- a/src/Init/Data/List/BasicAux.lean
+++ b/src/Init/Data/List/BasicAux.lean
@@ -121,4 +121,28 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a <
   | head => simp_arith
   | tail _ _ ih => exact Nat.lt_trans ih (by simp_arith)
 
+theorem append_cancel_left {as bs cs : List α} (h : as ++ bs = as ++ cs) : bs = cs := by
+  induction as with
+  | nil => assumption
+  | cons a as ih =>
+    injection h with _ h
+    exact ih h
+
+theorem append_cancel_right {as bs cs : List α} (h : as ++ bs = cs ++ bs) : as = cs := by
+  match as, cs with
+  | [], []       => rfl
+  | [], c::cs    => have aux := congrArg length h; simp_arith at aux
+  | a::as, []    => have aux := congrArg length h; simp_arith at aux
+  | a::as, c::cs => injection h with h₁ h₂; subst h₁; rw [append_cancel_right h₂]
+
+@[simp] theorem append_cancel_left_eq (as bs cs : List α) : (as ++ bs = as ++ cs) = (bs = cs) := by
+  apply propext; apply Iff.intro
+  next => apply append_cancel_left
+  next => intro h; simp [h]
+
+@[simp] theorem append_cancel_right_eq (as bs cs : List α) : (as ++ bs = cs ++ bs) = (as = cs) := by
+  apply propext; apply Iff.intro
+  next => apply append_cancel_right
+  next => intro h; simp [h]
+
 end List