rfl
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ ↑(filter (fun x => x ∈ A) (Ioc 0 n)).card / ↑n + ↑(filter (fun x => x ∈ B) (Ioc 0 n)).card / ↑n =
    ↑(countelements A n) / ↑n + ↑(countelements B n) / ↑n
no goals