English
If a function sel nearly lists elements uniquely via enumerate, then two different indices cannot yield the same element.
Русский
Если функция перечисления через enumerate выдаёт уникальные элементы, то два разных индекса не дают один и тот же элемент.
LaTeX
$$$\forall n_1,n_2,a,s,\big(\forall s,a,\ sel(s) = \mathrm{some} a \Rightarrow a \in s\big) \land \\ enumerate sel s n_1 = \mathrm{some} a \land enumerate sel s n_2 = \mathrm{some} a \Rightarrow n_1 = n_2$$$
Lean4
theorem enumerate_inj {n₁ n₂ : ℕ} {a : α} {s : Set α} (h_sel : ∀ s a, sel s = some a → a ∈ s)
(h₁ : enumerate sel s n₁ = some a) (h₂ : enumerate sel s n₂ = some a) : n₁ = n₂ :=
by
wlog hn : n₁ ≤ n₂ generalizing n₁ n₂
· exact (this h₂ h₁ (lt_of_not_ge hn).le).symm
rcases Nat.le.dest hn with ⟨m, rfl⟩
clear hn
induction n₁ generalizing s with
| zero =>
cases m with
| zero => rfl
| succ
m =>
have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.add_eq, zero_add]; exact h₂
have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
simp_all
| succ k ih =>
rw [show k + 1 + m = (k + m) + 1 by cutsat] at h₂
cases h : sel s <;> simp_all [enumerate]; tauto
