Fitch natural deduction proof of $\forall x F(x) \lor \forall x G(x) \vdash \forall x (F(x) \lor G(x))$

Question

I'm going through old exam papers and I found this question regarding the universal quantifier:

Now this seems to be very obvious, but I just can't get it right. Doing similar proofs with the existential quantifier seems easy, but this one just gets me. This is how I translated the question to the natural deduction site:

Thanks a lot in advance.

EDIT: I think I figured it out. I had the right idea but just didn't execute it correctly with the given tool. Thanks @lemontree for all of your assistance.

Answer 1

Hint: The "hourglass strategy" mentioned my answer to your other question applies to quantifiers just as well:

If you want to work linearly from the top to the conclusion, work your way through the premises from the outside to the inside by destructing them with elimination rules for the operators that occur in the premise, starting with an elimination rule for the main (= outermost) operator of the premise formula, until you disassembled them to minimally complex formulas. Then work your way towards the conclusion by constructing it from the inside out from the pieces you got by using introduction rules, the last one of which will be the main (= outermost) operator of the conclusion formula.
Here, this means: First get rid of the disjunction, then of the $\forall$'s, at which point you arrive at atomic formulas (this also means that your $Fa$ and $Ga$ will not be assumptions, as in the screenshot of your attempt, but derived from other (sub)formulas); then assemble them back together, first by introducing the disjunction, then the universal quantifier.

Often it is easier to start a proof from its conclusion, to see which sub-formulas are needed to be derived from the premises, in which case you use a kind of bottom-up-top-down strategy:
First un-do introduction rules on the conclusion formulas until you can no further disassemble them (or until it makes no more sense to do so), then try to meet in the middle by working your way down from the premises.
Here, this means: Apply backwards the introduction of the universal quantifier from the conclusion, then the introduction of the disjunction. Now try to see how you can arrive at the atoms you reconstructed given the form of the premises. This is where you will have to start working to-down again, disassembling the premises by use of elimination rules to meet the the second half of the proof in the middle.