no goals
α : Type u_2
β : Type u_1
γ : Type ?u.9045
r : α → α → Prop
s t✝ : Multiset α
a : α
t : Multiset β
l₁ : List α
l₂ : List β
d₁ : Nodup (Quotient.mk (isSetoid α) l₁)
d₂ : Nodup (Quotient.mk (isSetoid β) l₂)
⊢ Nodup (Quotient.mk (isSetoid α) l₁ ×ˢ Quotient.mk (isSetoid β) l₂)
simp [List.Nodup.product d₁ d₂]