The Ax-Schanuel conjecture for mixed Shimura varieties

Let $S$ be a connected mixed Shimura variety associated with $(P,\mathcal{X}^+)$ and let $\mathrm{unif}\colon\mathcal{X}^+\to S$ be its uniformization. Let $\mathbscr{Z}$ be the graph of the restriction of $\mathrm{unif}$ to a complex analytic irreducible subvariety $\widetilde{Z}$, and let $\mathbscr{B}$ be its Zariski closure in $\mathcal{X}^+\times S$. Let $F$ be the smallest bi-algebraic, equivalently weakly special, subvariety of $S$ containing $Z=\operatorname{pr}_S(\mathbscr{Z})$. Ax-Schanuel conjecture for mixed Shimura varieties. Then

$$\dim\mathbscr{B}-\dim\mathbscr{Z}\geqslant\dim F.$$

This is stated as a common generalization of the Ax logarithmique and Ax–Lindemann theorems for mixed Shimura varieties; the supplied text does not state that it has been proved.