English
An element x of l is a duplicate iff there exist two distinct indices n ≺ m in Fin(length l) such that l.get n = x = l.get m.
Русский
Элемент x списка l повторяется (является дублем), если существуют два различных индекса n и m в Fin(|l|) такие, что l.get n = x = l.get m.
LaTeX
$$$ l.Duplicate\\ x \\iff \\exists n,m:\\, Fin(l.length), n < m \\wedge x = l.get n \\wedge x = l.get m. $$$
Lean4
/-- An element `x : α` of `l : List α` is a duplicate iff it can be found
at two distinct indices `n m : ℕ` inside the list `l`.
-/
theorem duplicate_iff_exists_distinct_get {l : List α} {x : α} :
l.Duplicate x ↔ ∃ (n m : Fin l.length) (_ : n < m), x = l.get n ∧ x = l.get m := by
classical
rw [duplicate_iff_two_le_count, ← replicate_sublist_iff, sublist_iff_exists_fin_orderEmbedding_get_eq]
constructor
· rintro ⟨f, hf⟩
refine ⟨f ⟨0, by simp⟩, f ⟨1, by simp⟩, f.lt_iff_lt.2 (Nat.zero_lt_one), ?_⟩
rw [← hf, ← hf]; simp
· rintro ⟨n, m, hnm, h, h'⟩
refine ⟨OrderEmbedding.ofStrictMono (fun i => if (i : ℕ) = 0 then n else m) ?_, ?_⟩
· rintro ⟨⟨_ | i⟩, hi⟩ ⟨⟨_ | j⟩, hj⟩
· simp
· simp [hnm]
· simp
· simp only [Nat.lt_succ_iff, Nat.succ_le_succ_iff, replicate, length, Nat.le_zero] at hi hj
simp [hi, hj]
· rintro ⟨⟨_ | i⟩, hi⟩
· simpa using h
· simpa using h'
