English
For all N,k, the sum of the cardinalities #(smoothNumbersUpTo N k) + #(roughNumbersUpTo N k) equals N.
Русский
Для всех N,k сумма кардинальностей #(smoothNumbersUpTo N k) и #(roughNumbersUpTo N k) равна N.
LaTeX
$$$\#(\mathrm{smoothNumbersUpTo}(N,k)) + \#(\mathrm{roughNumbersUpTo}(N,k)) = N$$$
Lean4
theorem smoothNumbersUpTo_card_add_roughNumbersUpTo_card (N k : ℕ) :
#(smoothNumbersUpTo N k) + #(roughNumbersUpTo N k) = N :=
by
rw [smoothNumbersUpTo, roughNumbersUpTo, ←
Finset.card_union_of_disjoint <| Finset.disjoint_filter.mpr fun n _ hn₂ h ↦ h.2 hn₂, Finset.filter_union_right]
suffices #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N
by
have hn' (n) : n ∈ smoothNumbers k ∨ n ≠ 0 ∧ n ∉ smoothNumbers k ↔ n ≠ 0 :=
by
have : n ∈ smoothNumbers k → n ≠ 0 := ne_zero_of_mem_smoothNumbers
refine ⟨fun H ↦ Or.elim H this fun H ↦ H.1, fun H ↦ ?_⟩
simp only [ne_eq, H, not_false_eq_true, true_and, or_not]
rwa [Finset.filter_congr (s := Finset.range (succ N)) fun n _ ↦ hn' n]
rw [Finset.filter_ne', Finset.card_erase_of_mem <| Finset.mem_range_succ_iff.mpr <| zero_le N]
simp only [Finset.card_range, succ_sub_succ_eq_sub, tsub_zero]
