$\mathrm{Diff}(D^4)$ is a $5$-fold loop space

Let $\mathrm{Diff}(D^4)$ be the group of diffeomorphisms of the $4$-ball that are the identity on the boundary, with the $C^\infty$ topology. Then $\mathrm{Diff}(D^4)$ has the homotopy type of a $5$-fold loop space: there is a pointed space $(Y,y)$ with

In general the Cerf–Morlet comparison theorem gives $\mathrm{Diff}(D^n)\simeq\Omega^{n+1}(PL_n/O_n)$; for $n=4$ this is the stated $5$-fold delooping (see also Budney, Little cubes and long knots). A consequence is that all homotopy groups of $\mathrm{Diff}(D^4)$, including $\pi_0$ with its composition group structure, are abelian.

Formalization Note $\Omega^5(Y,y)$ is Mathlib's space of generalized loops GenLoop (Fin 5) Y y: continuous maps $[0,1]^5\to Y$ sending the boundary of the cube to $y$, with the compact-open topology. The space $Y$ is only required to be some topological space; the source's $Y = PL_4/O_4$ is not formalized.