Mahler's bound: the irrationality measure of π is at most 42

The irrationality measure of $\pi$ is at most $42$. Explicitly, for every real $\varepsilon>0$, there exists $Q\in\mathbb N$ such that for every $p\in\mathbb Z$ and every $q\in\mathbb N$ with $q>0$ and $q\ge Q$,

This is the epsilon upper-bound consequence of Mahler (1953), Theorem 1. The mathematical result is known; this mission leaves its Lean proof open.