feat(Data/List/Dedup): dedup and Nodup lemmas

Mathlib/Data/Finset/Card.lean

@@ -203,6 +203,9 @@ theorem Multiset.dedup_card_eq_card_iff_nodup {m : Multiset α} :
 theorem Multiset.toFinset_card_eq_card_iff_nodup {m : Multiset α} :
     #m.toFinset = card m ↔ m.Nodup := dedup_card_eq_card_iff_nodup
 
+theorem nodup_iff_le_length_dedup : m.Nodup ↔ m.card ≤ m.dedup.card := by
+  rw [← dedup_card_eq_card_iff_nodup, card_le_card m.dedup_le |>.ge_iff_eq]
+
 theorem List.card_toFinset : #l.toFinset = l.dedup.length :=
   rfl
 

Mathlib/Data/Finset/Dedup.lean

@@ -124,6 +124,10 @@ theorem mem_toFinset : a ∈ l.toFinset ↔ a ∈ l :=
 theorem coe_toFinset (l : List α) : (l.toFinset : Set α) = { a | a ∈ l } :=
   Set.ext fun _ => List.mem_toFinset
 
+@[simp]
+theorem toFinset_dedup : l.dedup.toFinset = l.toFinset :=
+  Finset.eq_of_veq <| by simp
+
 theorem toFinset_surj_on : Set.SurjOn toFinset { l : List α | l.Nodup } Set.univ := by
   rintro ⟨⟨l⟩, hl⟩ _
   exact ⟨l, hl, (toFinset_eq hl).symm⟩

Mathlib/Data/List/Dedup.lean

@@ -90,6 +90,15 @@ theorem tail_dedup [Inhabited α] (l : List α) :
 theorem dedup_eq_self {l : List α} : dedup l = l ↔ Nodup l :=
   pwFilter_eq_self
 
+theorem nodup_iff_sublist_dedup {l : List α} : l.Nodup ↔ l <+ l.dedup :=
+  dedup_eq_self.symm.trans ⟨(·.symm ▸ .refl l), l.dedup_sublist.antisymm⟩
+
+theorem nodup_iff_length_dedup_eq {l : List α} : l.Nodup ↔ l.dedup.length = l.length := by
+  rw [← dedup_eq_self, l.dedup_sublist.length_eq]
+
+theorem nodup_iff_le_length_dedup {l : List α} : l.Nodup ↔ l.length ≤ l.dedup.length :=
+  nodup_iff_length_dedup_eq.trans ⟨Nat.le_of_eq ∘ symm, antisymm l.dedup_sublist.length_le⟩
+
 theorem dedup_eq_cons (l : List α) (a : α) (l' : List α) :
     l.dedup = a :: l' ↔ a ∈ l ∧ a ∉ l' ∧ l.dedup.tail = l' := by
   refine ⟨fun h => ?_, fun h => ?_⟩