[GOAL]
ι : Sort u_1
α : ι → Sort u_2
ne : ∀ (i : ι), Nonempty (α i)
p : ι → Prop
f : (i : Subtype p) → α i.val
⊢ ∃ g, (fun i => g i.val) = f
[PROOFSTEP]
haveI : DecidablePred p := fun i ↦ Classical.propDecidable (p i)
[GOAL]
ι : Sort u_1
α : ι → Sort u_2
ne : ∀ (i : ι), Nonempty (α i)
p : ι → Prop
f : (i : Subtype p) → α i.val
this : DecidablePred p
⊢ ∃ g, (fun i => g i.val) = f
[PROOFSTEP]
exact ⟨fun i => if hi : p i then f ⟨i, hi⟩ else Classical.choice (ne i), funext fun i ↦ dif_pos i.2⟩
