∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] (j j_1 : C),
  j = j_1 → ∀ (j' j'_1 : C), j' = j'_1 → CategoryTheory.IsCofiltered.min j j' = CategoryTheory.IsCofiltered.min j_1 j'_1