-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
have : Nonempty α
have₁ : ∀ (this : Nonempty α), ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have₂ : Nonempty α
have₃ have₄ : ∀ (this : Nonempty α), ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have₅ :
  ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)),
    ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have₆ :
  ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s))
    (h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y),
    ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have₇ :
  ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s))
    (h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y),
    let f := seqOfForallFinsetExistsAux P r h';
    ∀ (hf : f = seqOfForallFinsetExistsAux P r h'),
      ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have₈ :
  ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s))
    (h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y),
    let f := seqOfForallFinsetExistsAux P r h';
    ∀ (hf : f = seqOfForallFinsetExistsAux P r h') (A : ∀ (n : ℕ), P (f n)),
      ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have₉ :
  ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s))
    (h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y),
    let f := seqOfForallFinsetExistsAux P r h';
    ∀ (hf : f = seqOfForallFinsetExistsAux P r h') (A : ∀ (n : ℕ), P (f n)) (m n : ℕ) (hmn : m < n), r (f m) (f n)
have₁₀ :
  ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s))
    (h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y),
    let f := seqOfForallFinsetExistsAux P r h';
    ∀ (hf : f = seqOfForallFinsetExistsAux P r h') (A : ∀ (n : ℕ), P (f n)) (m n : ℕ) (hmn : m < n),
      r (f m) (seqOfForallFinsetExistsAux P r h' n)
have₁₁ :
  ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s))
    (h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y),
    let f := seqOfForallFinsetExistsAux P r h';
    ∀ (hf : f = seqOfForallFinsetExistsAux P r h') (A : ∀ (n : ℕ), P (f n)) (m n : ℕ) (hmn : m < n),
      r (f m)
        (Classical.choose (p := fun (x : α) ↦
          (∀ (x : α),
              Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ seqOfForallFinsetExistsAux P r h' (↑i : ℕ)) univ)
                  x →
                P x) →
            P x ∧
              ∀ (x_1 : α),
                Membership.mem (γ := Finset α)
                    (image (fun (i : Fin n) ↦ seqOfForallFinsetExistsAux P r h' (↑i : ℕ)) univ) x_1 →
                  r x_1 x)
          ⋯)
a :
  ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s))
    (h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y),
    let f := seqOfForallFinsetExistsAux P r h';
    ∀ (hf : f = seqOfForallFinsetExistsAux P r h') (A : ∀ (n : ℕ), P (f n)) (m n : ℕ) (hmn : m < n),
      Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ f (↑i : ℕ)) univ) (f m)
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)

Tactic:
classical
    have : Nonempty α := by
      rcases h ∅ (by simp) with ⟨y, _⟩
      exact ⟨y⟩
    choose! F hF using h
    have h' : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y := fun s => ⟨F s, hF s⟩
    set f := seqOfForallFinsetExistsAux P r h' with hf
    have A : ∀ n : ℕ, P (f n) := by
      intro n
      induction n using Nat.strong_induction_on with | _ n IH
      have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2
      rw [hf, seqOfForallFinsetExistsAux]
      exact
        (Classical.choose_spec
            (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n))))
            (by simp [IH'])).1
    refine ⟨f, A, fun m n hmn => ?_⟩
    conv_rhs => rw [hf]
    rw [seqOfForallFinsetExistsAux]
    apply
      (Classical.choose_spec
          (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n)))) (by simp [A])).2
    exact Finset.mem_image.2 ⟨⟨m, hmn⟩, Finset.mem_univ _, rfl⟩

Premises used: Iff.mpr, Finset.mem_univ, Finset.mem_image, seqOfForallFinsetExistsAux, And.intro, Exists.intro, rfl