Remove classical from SetTheory.Set.finite_choice proof

[gaearon]

I had some help from Claude on this one. I think it works. Not sure if you'd consider this cleaner but it avoids the need for decEq by going through lemmas about ℕ.

[gaearon]

For what it's worth, this also seems to work:

  set x : ∀ i, X i := by
    intro i
    if heq : i = last then
      rw [heq]; exact ⟨ a, ha ⟩
    else
      have : ∃ m, ∃ h: m < n, X i = X' (Fin_mk n m h) := by
          obtain ⟨ m, h, this ⟩ := mem_Fin' i
          have h' : m ≠ n := by contrapose! heq; simp [this, last, heq]
          replace h' : m < n := by contrapose! h'; linarith
          use m, h'; simp [X']; congr
      rw [this.choose_spec.choose_spec]; exact x' _

So I'm not sure why the original code snippet used cases decEq i last.

This PR still seems a bit cleaner to me though.