theorem List.nodup_map_on {α β : Type} {xs : List α} {f : α → β} (hxs : xs.Nodup) (hinj : ∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → f a = f b → a = b) : (map f xs).Nodup

Mapping a list without duplicates by a function injective on that list preserves the absence of duplicates.

theorem List.nodup_flatMap_of_disjoint {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → List β} (hxs : xs.Nodup) (hrow : ∀ (x : α), x ∈ xs → (f x).Nodup) (hdisj : ∀ (x : α), x ∈ xs → ∀ (y : α), y ∈ xs → x ≠ y → ∀ (z : β), z ∈ f x → z ∈ f y → False) : (flatMap f xs).Nodup

A flat map is duplicate-free when every row is duplicate-free and rows coming from distinct source elements are disjoint.

theorem List.compareLex_zipWith {α : Type u_1} {β : Type u_2} (cmp : α → α → Ordering) (f : α → β → α) (hcmp : ∀ (a b : α) (c : β), cmp a b = cmp (f a c) (f b c)) (as bs : List α) (cs : List β) : as.length = bs.length → as.length = cs.length → List.compareLex cmp as bs = List.compareLex cmp (zipWith f as cs) (zipWith f bs cs)

Lexicographic comparison is unchanged by pointwise combining both lists with the same third list when the element comparison has the corresponding invariance. The length hypotheses ensure zipWith does not truncate.