Dualize

Mathlib/CategoryTheory/Filtered/Basic.lean

@@ -516,6 +516,8 @@ class IsCofiltered extends IsCofilteredOrEmpty C : Prop where
   [nonempty : Nonempty C]
 #align category_theory.is_cofiltered CategoryTheory.IsCofiltered
 
+attribute [instance 100] IsCofiltered.nonempty
+
 instance (priority := 100) isCofilteredOrEmpty_of_semilatticeInf (α : Type u) [SemilatticeInf α] :
     IsCofilteredOrEmpty α where
   cone_objs X Y := ⟨X ⊓ Y, homOfLE inf_le_left, homOfLE inf_le_right, trivial⟩