formal proof challenge I am desperately trying to figure out the formal proof for this argument. 
$$\begin{array}{r}
A\lor B\\
A\lor C\\
\hline
A\lor (B \land C)
\end{array}$$
I am trying to apply the backwards method here. I am trying to infer A, in order to use vIntro in the last step and introduce the final disjunction. But I got stuck finding sufficient proof for A.
Any hint will be greatly appreciated. Thank you!
 A: Is the following a "formal proof"?
Let $a$, $b$, $c$ be boolean variables representing the truth values of $A$, $B$, $C$. Then by the second distributive law of Boolean algebra we have
$$(a\vee b)\wedge(a\vee c)=a\vee(b\wedge c)\ .$$
This shows that your "argument" not only proves the truth of the third line under the assumption of the first two, but that in fact the stuff above  the \hline is logically equivalent to what's underneath.
A: Since you've pointed out the text elsewhere these problems seem to come from, here goes:
1 (A v B) premise
2 (A v C) premise
3 | A hypothesis
4 | (A v (B^C)) 3 V introduction
5 | B hypothesis
6 || A hypothesis
7 || (A v (B^C)) 6 V introduction
8 || C hypothesis
9 || (B^C) 5, 8 ^ introduction
10 || (Av(B^C)) 9 V introduction
11 | (Av(B^C)) 6-7, 8-10, 2 V elimination
12 (Av(B^C)) 3-4, 5-11, 1 V elimination.

A: The following proof uses the law of the excluded middle (LEM) on $A$ to derive the goal:

I consider two cases $A$ and $¬A$. The first case uses disjunction introduction (∨I). The second case uses disjunctive syllogism (DS) and disjunction introduction. 
Further information about the inference rules and the proof checker are given in the links below.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf
A: 
I am trying to apply the backwards method here. I am trying to infer A, in order to use vIntro in the last step and introduce the final disjunction. But I got stuck finding sufficient proof for A.

You don't prove it; you assume it -- To be precise: you assume both cases aiming to derive the same conclusion from each.  The disjunction elimination rule then discharges the assumptions. This is also known as the Proof By Cases argument.  $$\dfrac{\dfrac{[A]^\star\\~~\vdots}{A\lor(B\land C)}\quad\dfrac{[B]^\star\\~~\vdots}{A\lor(B\land C)}\quad\lower{1.5ex}{A\lor B}~}{A\lor(B\land C)}{\small\lor\mathsf E^\star}$$
So, in this proof you need two $\lor$ eliminations and therefore four assumptions must be made and discharged.  The trick is how you combine the assumptions of $B$ and $C$.

 $$\dfrac{\dfrac{[A]^1}{A\lor(B\land C)}{\small\lor\mathsf I}\quad\dfrac{\dfrac{[A]^2}{A\lor(B\land C)}{\small\lor\mathsf I}\quad\dfrac{\dfrac{[B]^1\quad[C]^2}{B\land C}{\small\land\mathsf I}}{A\lor(B\land C)}{\small\lor\mathsf I}\quad\lower{1.5ex}{A\lor C}}{A\lor (B\land C)}{\small\lor\mathsf E^2}\quad\lower{1.5ex}{A\lor B}}{A\lor (B\land C)}{\small\lor\mathsf E^1}$$

