I need help to finish a proof in Lean 4, Well Ordering Principle implies Axiom of Choice

Question

The problem I got is once I've defined the Well Ordering Principle and the Axiom of Choice I am not able to sustract the information to formalize the proof. The idea is using the WOP in a collection of sets so I have the min of each set, once I have that I can create a function s from the collection of sets to the union of them that maps the set to the min which is an element of the set.

This is what I currently have:

import Mathlib.Tactic

variable {γ : Type _}
variable {I : Type _}
variable (X : I → Set γ)
variable (A : Set γ)
open Set

def well_ordered_principle (R : γ  → γ → Prop) : Prop := (∀ (A : Set γ), Nonempty A) → ∃ n ∈ A, ∀ m ∈ A, R n m

def axiom_of_choice : Prop := (∀ (i : I), Nonempty (X i)) → ∃ (f : (I → ⋃ i, X i)), ∀ (i : I), (f i).1 ∈ X i


theorem wop_aoc (R : γ → γ → Prop) : well_ordered_principle A R → axiom_of_choice X := by
  intro wop nempty

The idea I have is using the relation R to a collection of sets, so using that I have well_ordered_principle as hypothesis I wanted to extract the minimum of each using choice. But I think I don't understand how it works because everything I've tried raised an error.