Erdős Problem 421

Reference: erdosproblems.com/421

theorem erdos_421 : (∃ (d : ℕ → ℕ), StrictMono d ∧ 1 ≤ d 0 ∧ (Set.range d).HasDensity 1 ∧ Set.InjOn (fun (x : ℕ × ℕ) => match x with | (u, v) => ∏ i ∈ Finset.Icc u v, d i) {(u, v) : ℕ × ℕ | u ≤ v}) ↔ sorry

Is there a sequence $1 \le d_1 < d_2 < \dots$ with density 1 such that all products $\prod_{u \le i \le v} d_i$ are distinct?