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 : α × α
⊢ x ∈ mulAntidiagonal hs ht a ↔ x.fst ∈ s ∧ x.snd ∈ t ∧ x.fst * x.snd = a
simp only [mulAntidiagonal, Set.Finite.mem_toFinset, Set.mem_mulAntidiagonal]