α : Type u
β : Type v
l l₁✝ l₂ : List α
r : α → α → Prop
a b : α
l₁ : List α
f : α → List β
⊢ (Pairwise (fun a b => Disjoint (f a) (f b)) l₁ ∧ ∀ (l : List β) (x : α), f x = l → x ∈ l₁ → Nodup l) ↔
    Pairwise (fun a b => Disjoint (f a) (f b)) l₁ ∧ ∀ (x : α), x ∈ l₁ → Nodup (f x)
α : Type u
β : Type v
l l₁✝ l₂ : List α
r : α → α → Prop
a b : α
l₁ : List α
f : α → List β
⊢ Nodup (List.bind l₁ f) ↔ (∀ (x : α), x ∈ l₁ → Nodup (f x)) ∧ Pairwise (fun a b => Disjoint (f a) (f b)) l₁
simp only [List.bind, nodup_join, pairwise_map, and_comm, and_left_comm, mem_map, exists_imp,
    and_imp]
no goals
α : Type u
β : Type v
l l₁✝ l₂ : List α
r : α → α → Prop
a b : α
l₁ : List α
f : α → List β
⊢ (Pairwise (fun a b => Disjoint (f a) (f b)) l₁ ∧ ∀ (l : List β) (x : α), f x = l → x ∈ l₁ → Nodup l) ↔
    Pairwise (fun a b => Disjoint (f a) (f b)) l₁ ∧ ∀ (x : α), x ∈ l₁ → Nodup (f x)
rw [show (∀ (l : List β) (x : α), f x = l → x ∈ l₁ → Nodup l) ↔ ∀ x : α, x ∈ l₁ → Nodup (f x)
    from forall_swap.trans <| forall_congr' fun _ => forall_eq']