style: avoid using Decidable.em directly

Co-authored-by: Kyle Miller <[email protected]>
leanprover-community · Oct 16, 2024 · 7311737 · 7311737
1 parent 5afa617
commit 7311737
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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