∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α] {s t : Set α}
  {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {x : α × α},
  (x ∈ Finset.addAntidiagonal hs ht a) = (x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 + x.2 = a)