∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedCancelAddMonoid α] {s t : Set α}
  (hs : s.IsWF) (ht : t.IsWF) (hns : s.Nonempty) (hnt : t.Nonempty),
  Finset.addAntidiagonal ⋯ ⋯ (hs.min hns + ht.min hnt) = {(hs.min hns, ht.min hnt)}