Erdos392.Params.initial.card

@[blueprint  "initial-factorization-card"  (statement := /-- The number of elements in this initial factorization is at most $n$. -/)  (latexEnv := "sublemma")]theorem Params.initial.card (P : Params) : P.initial.a.card ≤ P.n := by  calc Multiset.card (filter (fun m ↦ m ∈ (P.n / P.L).smoothNumbers)      (replicate P.M (Multiset.Ico (P.n - P.n / P.M) P.n)).join)    _ ≤ Multiset.card (replicate P.M (Multiset.Ico (P.n - P.n / P.M) P.n)).join :=        card_le_card (filter_le _ _)    _ = P.M * Multiset.card (Multiset.Ico (P.n - P.n / P.M) P.n) := by        rw [card_join, map_replicate, sum_replicate, smul_eq_mul]    _ = P.M * (P.n - (P.n - P.n / P.M)) := by congr 1; simp [Multiset.Ico]    _ = P.M * (P.n / P.M) := by congr 1; exact Nat.sub_sub_self (div_le_self P.n P.M)    _ ≤ P.n := mul_div_le P.n P.M