fix: broken proof

leanprover-community · Aug 16, 2023 · d6e285b · d6e285b
1 parent 8bbdc2d
commit d6e285b
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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₂ :=