Proving a theorem in an extension of S$_4$ S$_{4.4}$ is the modal propositional system S$_4$ with the axiom schema $(\phi \land \Diamond \Box \phi) \rightarrow \Box \phi$. This schema is also equivalent to $\phi \rightarrow (\Diamond \Box \phi \rightarrow \Box \phi)$.
I am trying to prove the formula $(\Diamond P \land \Diamond Q) \rightarrow (\Diamond (P \land \Diamond Q) \lor \Diamond (Q \land \Diamond P))$
I know that the dual of the above is the formula $(\Box(P \lor \Box Q) \land \Box (Q \lor \Box P)) \rightarrow (\Box P \lor \Box Q)$. So I attempted to prove the dual version.
I know $\Box(P \lor \Box Q) \rightarrow (\Box P \lor \Diamond \Box Q)$ by a version of the K axiom.
Similarly, $\Box(Q \lor \Box P) \rightarrow (\Box Q \lor \Diamond \Box P)$ by a version of the K axiom.
Hence, $(\Box(P \lor \Box Q) \land \Box(Q \lor \Box P)) \rightarrow ((\Box P \lor \Diamond \Box Q) \land (\Box Q \lor \Diamond \Box P))$
But from here I don't know how else to proceed to reach the dual version of the sentence I am trying to prove.
 A: Derivable rules in S$_{4.4}$
$\def\pra#1{\left(#1\right)}$
The system S$_{4.4}$ have
Rules:
\begin{align}
&\frac{\varphi,\varphi\to\psi}{\psi}\tag{MP}\\
&~~~~~\frac{\varphi}{\square\varphi}\tag{NEC}
\end{align}
Axioms:
\begin{align}
&\varphi\to\pra{\psi\to\varphi}\tag{PL$_1$}\\
&\pra{\varphi\to\pra{\psi\to\chi}}\to\pra{\pra{\varphi\to\psi}\to\pra{\varphi\to\chi}}\tag{PL$_2$}\\
&\pra{\lnot\psi\to\lnot\varphi}\to\pra{\pra{\lnot\psi\to\varphi}\to\psi}\tag{PL$_3$}\\
&\square\pra{\varphi\to\psi}\to\pra{\square\varphi\to\square\psi}\tag{K}\\
&\square\varphi\to\varphi\tag{T}\\
&\square\varphi\to\square\square\varphi\tag{S$_{4}$}\\
&\pra{\varphi\land\Diamond\square\varphi}\to\square\varphi\tag{S$_{4.4}$}
\end{align}
The (K $\Diamond$) and (T $\Diamond$) are two useful Derivable rules in S$_{4.4}$. Since we will mainly focus on the modal logic, just cite PL for any consequences of PL$_1$-PL$_3$:
\begin{align}
&\square\pra{\varphi\to\psi}\to\pra{\Diamond\varphi\to\Diamond\psi}\tag{K$\Diamond$}\\
1.&~~(\varphi\to\psi)\to(\lnot\psi\to\lnot\varphi)\tag*{PL(contraposition)}\\
2.&~~\square(\varphi\to\psi)\to\square(\lnot\psi\to\lnot\varphi)\tag*{1,NEC,K,MP}\\
3.&~~\square(\lnot\psi\to\lnot\varphi)\to(\square\lnot\psi\to\square\lnot\varphi)\tag*{K}\\
4.&~~\square(\varphi\to\psi)\to(\square\lnot\psi\to\square\lnot\varphi)\tag*{2,3,PL (syllogism)}\\
5.&~~\square(\varphi\to\psi)\to(\lnot\square\lnot\varphi\to\lnot\square\lnot\psi)\tag*{4,PL (contraposition)}\\\\
&\varphi\to\Diamond\varphi\tag{T$\Diamond$}\\
1.&~\square\lnot\varphi\to\lnot\varphi\tag*{T}\\
2.&~\varphi\to\lnot\square\lnot\varphi\tag*{1, PL}
\end{align}
The above proof gives in $\textit{logic for philosophy}$ by Sider. In system K, we also have the four (MN) theorem schemas, which are also derivable in S$_{4.4}$, they are
\begin{align}
&\lnot\square\varphi\to\Diamond\lnot\varphi&&\Diamond\lnot\varphi\to\lnot\square\varphi\tag{MN}\\
&\lnot\Diamond\varphi\to\square\lnot\varphi&&\square\lnot\varphi\to\lnot\Diamond\varphi
\end{align}
Since we will only need the first one i.e.
\begin{align}
&\lnot\square\varphi\to\Diamond\lnot\varphi\\
1.&~\lnot\lnot\varphi\to\varphi\tag*{PL}\\
2.&~\square\lnot\lnot\varphi\to\square\varphi\tag*{1, NEC, K, MP}\\
3.&~\lnot\square\varphi\to\lnot\square\lnot\lnot\varphi\tag*{2, PL}
\end{align}
for the rest, you can do them as exercise if you are interested.

Prove the dual version

Hence, $(□(P∨□Q)∧□(Q∨□P))→((□P∨◊□Q)∧(□Q∨◊□P))$
But from here I don't know how else to proceed to reach the dual version of the sentence I am trying to prove.

Here what you got is correct. However, in this case, to prove the dual version, this seems not very useful, so we try something else, for example
\begin{align}
1.&~\pra{P\lor\square Q}\to\pra{\lnot P\to\square Q}\tag*{PL}\\
2.&~\square\pra{P\lor\square Q}\to\square\pra{\lnot P\to\square Q}\tag*{1, NEC, K, MP}\\
3.&~\square\pra{\lnot P\to\square Q}\to\pra{\lnot\square P\to\Diamond\square Q}\tag*{K$\Diamond$, MN, PL}\\
4.&~\square\pra{P\lor\square Q}\to\pra{\lnot\square P\to\Diamond\square Q}\tag*{2,3, PL}\\
5.&~\square\pra{Q\lor\square P}\to\pra{Q\lor\square P}\tag*{T}\\
6.&~\pra{Q\lor\square P}\to\pra{\lnot\square P\to Q}\tag*{PL}\\
7.&~\square\pra{Q\lor\square P}\to\pra{\lnot\square P\to Q}\tag*{5,6, PL}\\
8.&~\pra{\square\pra{P\lor\square Q}\land\square\pra{Q\lor\square P}}\\
&\to\pra{\lnot\square P\to\pra{Q\land\Diamond\square Q}}\tag*{4,7, PL}\\
9.&~\pra{Q\land\Diamond\square Q}\to\square Q\tag*{S$_{4.4}$}\\
10.&~\pra{\square\pra{P\lor\square Q}\land\square\pra{Q\lor\square P}}\to\pra{\square P\lor\square Q}\tag*{8,9, PL}
\end{align}
Hence $\vdash_{\text{S}_{4.4}}\pra{\square\pra{P\lor\square Q}\land\square\pra{Q\lor\square P}}\to\pra{\square P\lor\square Q}$. In this example, it substituted $Q$ to the axiom schema (S$_{4.4}$), we can also substitute $P$, the idea is the same.

Prove the original version
For a more direct approach, we can give a proof for the original version, which is also doable, and for the S$_{4.4}$  axiom schema, we substitute either $\lnot P$ or $\lnot Q$ instead of $P$ or $Q$.
\begin{align}
        1.&~\pra{\square\pra{Q\to\square\lnot P}\land\Diamond Q}\to\Diamond\square\lnot P\tag*{K$\Diamond$, PL}\\
        2.&~\pra{\lnot P\land\Diamond\square\lnot P}\to\square\lnot P\tag*{S$_{4.4}$}\\
        3.&~\Diamond P\to\pra{\Diamond\square\lnot P\to P}\tag*{2, PL}\\
        4.&~\pra{\square\pra{Q\to\square\lnot P}\land\Diamond P\land\Diamond Q}\to \pra{P\land\Diamond Q}\tag*{1,3, PL}\\
        5.&~\pra{P\land\Diamond Q}\to\Diamond\pra{P\land\Diamond Q}\tag*{T$\Diamond$}\\
        6.&~\pra{\square\pra{Q\to\square\lnot P}\land\Diamond P\land\Diamond Q}\to\Diamond\pra{P\land\Diamond Q}\tag*{4,5, PL}\\
        7.&~\pra{\Diamond P\land\Diamond Q}\to\pra{\Diamond\pra{P\land\Diamond Q}\lor\Diamond\pra{Q\land\Diamond P}}\tag*{6, MN, PL}
    \end{align}
Hence $\vdash_{\text{S}_{4.4}}\pra{\Diamond P\land\Diamond Q}\to\pra{\Diamond\pra{P\land\Diamond Q}\lor\Diamond\pra{Q\land\Diamond P}}$.
