Erdős Problem 25: Logarithmic density of size-dependent congruences

Let $n_1 < n_2 < \dots$ be an arbitrary sequence of integers, each with an associated residue class $a_i \pmod{n_i}$. Let $A$ be the set of integers $n$ such that for every $i$ either $n < n_i$ or $n \not\equiv a_i \pmod{n_i}$. Must the logarithmic density of $A$ exist?

Reference: erdosproblems.com/25

theorem Erdos25.erdos_25 : sorry ↔ ∀ (seq_n : ℕ → ℕ) (seq_a : ℕ → ℤ), (∀ (i : ℕ), 0 < seq_n i) → StrictMono seq_n → ∃ (d : ℝ), {x : ℕ | ∀ (i : ℕ), ↑x < ↑(seq_n i) ∨ ¬↑x ≡ seq_a i [ZMOD ↑(seq_n i)]}.HasLogDensity d

Erdős Problem 25

Let $n_1 < n_2 < \dots$ be an arbitrary sequence of integers, each with an associated residue class $a_i \pmod{n_i}$. Let $A$ be the set of integers $n$ such that for every $i$ either $n < n_i$ or $n \not\equiv a_i \pmod{n_i}$. Must the logarithmic density of $A$ exist?