We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent a26d7cc commit 7b8f8deCopy full SHA for 7b8f8de
Batteries/Data/List/Lemmas.lean
@@ -282,7 +282,7 @@ theorem diff_erase (l₁ l₂ : List α) (a : α) : (l₁.diff l₂).erase a = (
282
@[simp] theorem nil_diff (l : List α) : [].diff l = [] := by
283
induction l <;> simp [*, erase_of_not_mem]
284
285
-theorem cons_diff [DecidableEq α] (a : α) (l₁ l₂ : List α) :
+theorem cons_diff (a : α) (l₁ l₂ : List α) :
286
(a :: l₁).diff l₂ = if a ∈ l₂ then l₁.diff (l₂.erase a) else a :: l₁.diff l₂ := by
287
induction l₂ generalizing l₁ with
288
| nil => rfl
0 commit comments