How do I prove an existential goal that asks for a certain function in Coq?

Completely new to coq here.

I know about the exists tactic to prove an existential goal, but in this case it wants a function mapping from two sets. What is the syntax for demonstrating such a function?

And if there is no such function how would I disprove this? (I would suppose through a contradiction, but then how would I pose a contradictory hypothesis?)

Context: Trying to work out the proof that all surjective functions have a right inverse.

1 subgoal
A, B : Set
f : A → B
H : ∀ b : B, ∃ a : A, f a = b
______________________________________(1/1)
∃ g : B → A, ∀ b : B, f (g b) = b

Of course, whether or not a function g exists depends on accepting axiom of choice, so where does that come into coq?

I did find this solution:
https://gist.github.com/pedrominicz/0d9004b82713d9244b762eb250b9c808
and the associated reddit post
https://www.reddit.com/r/logic/comments/fxjypn/what_is_not_constructive_in_this_proof/

But I didn't understand it/didn't work for me.

So, what I want to know is:

How do you specify axiom of choice in coq (to prove/disprove this)?
In general, how would I construct a function to provide witness to an existential goal? (I also want to show that all injective functions have a left inverse)

Solution

Here is an answer that is a complete script (tested with coq 8.13.2). Coq by default does not have the axiom of choice loaded, so you need to say explicitly that you are going to work with it.

Require Import ClassicalChoice.

Lemma question (A B : Set) (f : A -> B) :
   (forall b, exists a, f a = b) -> exists g, forall b, f (g b) = b.
Proof.
intros H.
apply (choice (fun y x => f x = y)).
exact H.
Qed.