why is this here

Author: vihdzp

Mathlib/Order/Interval/Set/Basic.lean

@@ -472,7 +472,7 @@ variable [PartialOrder α] {a b c : α}
 
 @[simp]
 theorem Icc_self (a : α) : Icc a a = {a} :=
-  ext <| by simp [Icc, le_antisymm_iff, and_comm]
+  Set.ext <| by simp [Icc, le_antisymm_iff, and_comm]
 
 instance instIccUnique : Unique (Icc a a) where
   default := ⟨a, by simp⟩