Build some sequence inductively using all previous terms

Stream: Is there code for X?

[Frédéric Le Roux]

What is the way to build a sequence inductively using all previous term? My secrete goal is to build a sequence with no converging subsequence in a metric space which is not precompact. But here is an easier minimal example (in Lean 3...):

lemma example1 (X: Type) (H: (∀ A: finset X, ∃ x: X, x ∉ A)):
(∃ u: ℕ → X, ∀k l, k<l → (u k ≠ u l)) :=
begin
    sorry
end

How do I build the witness sequence u in this context?

[Kyle Miller]

Here's an option, using a recursive definition:

import data.finset.basic

noncomputable def sets (X: Type) (H: (∀ A: finset X, ∃ x: X, x ∉ A)) : ℕ → finset X
| 0 := ∅
| (n+1) := let s := sets n in s.cons (H s).some (Exists.some_spec (H s))

noncomputable def u (X: Type) (H: (∀ A: finset X, ∃ x: X, x ∉ A)) : ℕ → X
| n := (H (sets X H n)).some

lemma example1 (X: Type) (H: (∀ A: finset X, ∃ x: X, x ∉ A)):
(∃ u: ℕ → X, ∀k l, k<l → (u k ≠ u l)) :=
begin
  existsi (u X H),
  sorry,
end

[Kyle Miller]

Here's a lemma to help work with sets:

lemma sets_succ (X: Type) (H: (∀ A: finset X, ∃ x: X, x ∉ A)) (n : ℕ) :
  sets X H (n + 1) = (sets X H n).cons (u X H n) (Exists.some_spec (H (sets X H n))) :=
begin
  simp only [sets, u],
  refl,
end

[Kyle Miller]

This might work, if you want to avoid making an auxiliary definition like that:

lemma example1 (X: Type) (H: (∀ A: finset X, ∃ x: X, x ∉ A)):
  (∃ u: ℕ → X, ∀k l, k<l → (u k ≠ u l)) :=
begin
  classical,
  choose next hnext using H,
  let f := λ (s : finset X), insert (next s) s,
  let sets := λ n, nat.iterate f n ∅,
  existsi next ∘ sets,
  sorry
end

[Frédéric Le Roux]

Many thanks!!