no goals
α : Type u_1
β : Type u_2
γ : Type ?u.65525
ι : Sort ?u.65528
π : α → Type ?u.65533
inst✝ : Nonempty α
s : Set α
f : α → β
a : α
b : β
h : ¬∃ a, a ∈ s ∧ f a = b
⊢ invFunOn f s b = Classical.choice inst✝
rw [invFunOn, dif_neg h]