I'm learning about natural deduction from https://www.inf.ed.ac.uk/teaching/courses/ar//slides02.pdf
I'm trying to understand its proof of
$$ P \land (Q \lor R) \vDash (P \land Q) \lor (P \wedge R) $$
which is given as
$$ \frac{ \displaystyle \frac{ P \land (Q \lor R) }{ Q \lor R } \quad \frac{ \displaystyle \frac{ \displaystyle \frac{P \land (Q \lor R)}{P} \quad[Q] }{ (P \land Q) } }{ (P \land Q) \lor (P \wedge R) } \quad \frac{ \displaystyle \frac{ \displaystyle \frac{P \land (Q \lor R)}{P} \quad[R] }{ (P \land R) } }{ (P \land Q) \lor (P \wedge R) } } { (P \land Q) \lor (P \land R) } $$ I think I understand the application of the various rules: conjI, conjunct1, conjunct2, disjI1, disjI2. But I'm having trouble reasoning about how disjE is applied on the bottom step. The structure of the proof doesn't seem to match how the rule is given:
$$ \frac{P \lor Q\quad \begin{matrix}[P] \\ \vdots \\ R\end{matrix} \quad \begin{matrix}[Q] \\ \vdots \\ R\end{matrix}}{R} $$
Specifically, for each of the $[P]$ and $[Q]$ terms in the rule (so $[Q]$ and $[R]$ in the proof) there is an extra premise(?) next to it, so it's not clear to me that disjE can be applied.
How disjE is applied here?
The last rule in the given derivation in the OP does match with the general scheme of the rule for elimination of disjunction $\lor_E$ below (I only changed the letters with respect to the rule in the OP)
\begin{equation}\tag{1} \frac{Q \lor R \quad \begin{matrix}[Q] \\ \vdots \\ P\end{matrix} \quad \begin{matrix}[R] \\ \vdots \\ P\end{matrix}}{P}\lor_E \end{equation}
Indeed, in $(1)$, writing
$$\tag{2} \begin{matrix}[Q] \\ \vdots \\ P\end{matrix} $$
means that there is a derivation whose conclusion is $P$ and that a number (possibly 0) of occurrences of $Q$ among the assumptions for that derivation will be discharged by the rule $\lor_E$ in $(1)$. It does not exclude the possibility that in $(2)$ there are other assumptions (or other occurrences of the same assumption $Q$ that won't be discharged later by $\lor_E$). Said differently, $(2)$ does not mean that $Q$ is the only "legitimate" assumption that can be used to derive $P$.
In the given derivation in the OP, the subderivation below
$$\tag{3} \displaystyle \frac{ \displaystyle \frac{ \displaystyle \frac{P \land (Q \lor R)}{P} \quad[Q] }{ (P \land Q) } }{ (P \land Q) \lor (P \wedge R) } $$ perfectly matches the pattern in $(2)$. Indeed, $(3)$ is a derivation where there are two assumptions: