no goals
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
L : List (List α)
⊢ Nodup (join L) ↔ (∀ (l : List α), l ∈ L → Nodup l) ∧ Pairwise Disjoint L
simp only [Nodup, pairwise_join, disjoint_left.symm, forall_mem_ne]