no goals
α : Type u_1
β : Type u_2
γ : Type ?u.15034
r : α → α → Prop
s✝ t✝ : Multiset α
a : α
s : Multiset α
t : α → Multiset β
h₁ : ∀ (a : α), ∃ l, t a = ↑l
t' : α → List β
h' : ∀ (x : α), t x = ↑(t' x)
this : t = fun a => ↑(t' a)
hd : Symmetric fun a b => List.Disjoint (t' a) (t' b)
⊢ ∀ (a : List α),
    Nodup (bind (Quot.mk Setoid.r a) t) ↔
      (∀ (a_1 : α), a_1 ∈ Quot.mk Setoid.r a → Nodup (t a_1)) ∧
        Pairwise (fun a b => Disjoint (t a) (t b)) (Quot.mk Setoid.r a)
simp [this, List.nodup_bind, pairwise_coe_iff_pairwise hd]