no goals
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
hs : Set.IsPwo s
ht : Set.IsPwo t
a : α
u : Set α
hu : Set.IsPwo u
x : α × α
⊢ Prod.swap x ∈ mulAntidiagonal hs ht a ↔ x ∈ mulAntidiagonal ht hs a
simp only [mem_mulAntidiagonal, Prod.fst_swap, Prod.snd_swap, Set.swap_mem_mulAntidiagonal_aux,
           Set.mem_mulAntidiagonal]