English
Dedup(l) equals a :: l' if and only if a appears in l, a does not appear in l', and the tail of dedup(l) equals l'.
Русский
Dedup(l) = a :: l' тогда и только тогда, когда a встречается в l, a не встречается в l', и хвост dedup(l) равен l'.
LaTeX
$$$\\mathrm{dedup}(l) = a :: l' \\iff a \\in l \\land a \\notin l' \\land \\mathrm{dedup}(l).\\mathrm{tail} = l'$$$
Lean4
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 => ?_⟩
· refine ⟨mem_dedup.1 (h.symm ▸ mem_cons_self), fun ha => ?_, by rw [h, tail_cons]⟩
have := count_pos_iff.2 ha
have : count a l.dedup ≤ 1 := nodup_iff_count_le_one.1 (nodup_dedup l) a
rw [h, count_cons_self] at this
cutsat
· have := @List.cons_head!_tail α ⟨a⟩ _ (ne_nil_of_mem (mem_dedup.2 h.1))
have hal : a ∈ l.dedup := mem_dedup.2 h.1
rw [← this, mem_cons, or_iff_not_imp_right] at hal
exact this ▸ h.2.2.symm ▸ cons_eq_cons.2 ⟨(hal (h.2.2.symm ▸ h.2.1)).symm, rfl⟩
