diff --git a/Mathlib/Data/List/Lattice.lean b/Mathlib/Data/List/Lattice.lean
index 6c7145c64544ad..6639ed1ae11d81 100644
--- a/Mathlib/Data/List/Lattice.lean
+++ b/Mathlib/Data/List/Lattice.lean
@@ -80,8 +80,8 @@ section Union
 @[simp]
 theorem mem_union : a ∈ l₁ ∪ l₂ ↔ a ∈ l₁ ∨ a ∈ l₂ := by
   induction l₁
-  · simp only [not_mem_nil, false_or_iff, instUnionList, nil_union]
-  · simp only [find?, mem_cons, or_assoc, instUnionList, cons_union, mem_union_iff, mem_insert_iff]
+  · simp only [nil_union, find?, not_mem_nil, false_or]
+  · simp only [cons_union, mem_union_iff, mem_insert_iff, find?, mem_cons, or_assoc]
 #align list.mem_union List.mem_union
 
 theorem mem_union_left (h : a ∈ l₁) (l₂ : List α) : a ∈ l₁ ∪ l₂ :=