diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
index ce01b13f9e..66448f94ed 100644
--- a/Batteries/Data/List/Lemmas.lean
+++ b/Batteries/Data/List/Lemmas.lean
@@ -520,7 +520,7 @@ theorem commonPrefix_prefix_left (l₁ l₂ : List α) : commonPrefix l₁ l₂
   | _::_, [] => simp [commonPrefix]
   | a₁::l₁, a₂::l₂ =>
     simp only [commonPrefix]
-    cases Decidable.em (a₁ = a₂)
+    split
     · next h =>
       simp only [h, ↓reduceIte, cons_prefix_cons, true_and]
       apply commonPrefix_prefix_left