From 7311737cb90663ec7a679948cab9ebc38995d405 Mon Sep 17 00:00:00 2001
From: Bulhwi Cha <chabulhwi@semmalgil.com>
Date: Wed, 16 Oct 2024 12:21:29 +0900
Subject: [PATCH] style: avoid using `Decidable.em` directly

Co-authored-by: Kyle Miller <kmill31415@gmail.com>
---
 Batteries/Data/List/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
index 400ca823f7..0064065637 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