Erdos392.Params.rough_set_card_le

lemma Params.rough_set_card_le (P : Params) :    (rough_set P).card ≤ (Nat.primeCounting P.n) * P.L := by  have h_struct : ∀ m ∈ rough_set P,      ∃ q k, q.Prime ∧ q ≥ P.n / P.L ∧ k ≤ P.L ∧ m = q * k ∧ m.factorization q = 1 :=    fun m hm => rough_set_structure P m hm  have h_subset : rough_set P ⊆ Finset.image (fun p : ℕ × ℕ => p.1 * p.2)      (Finset.product (Finset.filter Nat.Prime (Finset.Icc 1 P.n)) (Finset.Icc 1 P.L)) := by    intro m hm    obtain ⟨q, k, hq, hq', hk, rfl, _⟩ := h_struct m hm    exact Finset.mem_image.mpr ⟨(q, k), Finset.mem_product.mpr      ⟨Finset.mem_filter.mpr ⟨Finset.mem_Icc.mpr ⟨hq.pos, by        have := Finset.mem_Ico.mp (Finset.mem_filter.mp hm |>.1)        nlinarith [Nat.pos_of_ne_zero (show k ≠ 0 from by aesop)]⟩, hq⟩,      Finset.mem_Icc.mpr ⟨Nat.pos_of_ne_zero (by aesop), hk⟩⟩, rfl⟩  refine le_trans (Finset.card_le_card h_subset) (le_trans Finset.card_image_le ?_)  erw [Finset.card_product, Nat.primeCounting, Nat.primeCounting', Nat.count_eq_card_filter_range]  simp only [Finset.range_eq_Ico, Nat.card_Icc, add_tsub_cancel_right]  have h1 : Finset.filter Nat.Prime (Finset.Icc 1 P.n) =      Finset.filter Nat.Prime (Finset.Icc 0 P.n) := by    ext p    simp only [Finset.mem_filter, Finset.mem_Icc]    constructor <;> intro ⟨⟨hl, hr⟩, hp⟩    · exact ⟨⟨Nat.zero_le _, hr⟩, hp⟩    · exact ⟨⟨hp.one_le, hr⟩, hp⟩  have h2 : Finset.filter Nat.Prime (Finset.Ico 0 (P.n + 1)) =      Finset.filter Nat.Prime (Finset.Icc 0 P.n) := by congr 1  rw [h1, h2, mul_comm]