refactor: golf proof

Co-authored-by: Kyle Miller <[email protected]>
leanprover-community · Oct 16, 2024 · 5afa617 · 5afa617
1 parent 6659801
commit 5afa617
Showing 1 changed file with 2 additions and 11 deletions.
diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
@@ -528,17 +528,8 @@ theorem commonPrefix_prefix_left (l₁ l₂ : List α) : commonPrefix l₁ l₂
       simp [h]
 
 theorem commonPrefix_prefix_right (l₁ l₂ : List α) : commonPrefix l₁ l₂ <+: l₂ := by
-   match l₁, l₂ with
-  | [],   _  => simp [commonPrefix]
-  | _::_, [] => simp [commonPrefix]
-  | a₁::l₁, a₂::l₂ =>
-    simp only [commonPrefix]
-    cases Decidable.em (a₁ = a₂)
-    · next h =>
-      simp only [h, ↓reduceIte, cons_prefix_cons, true_and]
-      apply commonPrefix_prefix_right
-    · next h =>
-      simp [h]
+  rw [commonPrefix_comm]
+  apply commonPrefix_prefix_left
 
 theorem commonPrefix_append_append (p l₁ l₂ : List α) :
     commonPrefix (p ++ l₁) (p ++ l₂) = p ++ commonPrefix l₁ l₂ := by