Erdős Problem 728

Reference: erdosproblems.com/728

theorem Erdos728.erdos_728 : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ C > 0, ∀ C' > C, ∃ (a : ℕ) (b : ℕ) (n : ℕ), 0 < n ∧ ε * ↑n < ↑a ∧ ε * ↑n < ↑b ∧ a.factorial * b.factorial ∣ n.factorial * (a + b - n).factorial ∧ ↑a + ↑b > ↑n + C * Real.log ↑n ∧ ↑a + ↑b < ↑n + C' * Real.log ↑n

Let $\varepsilon$ be sufficiently small and $C, C' > 0$. Are there integers $a, b, n$ such that $$a, b > \varepsilon n\quad a!\, b! \mid n!\, (a + b - n)!, $$ and $$C \log n < a + b - n < C' \log n ?$$

Note that the website currently displays a simpler (trivial) version of this problem because $a + b$ isn't assumed to be in the $n + O(\log n)$ regime.