Sieve.siftedSum_eq

theorem siftedSum_eq (s : SelbergSieve) (hw : ∀ i ∈ s.support, s.weights i = 1) (z : ℝ)    (hz : 1 ≤ z) (hP : s.prodPrimes = primorial (Nat.floor z)) :    siftedSum (s := s.toBoundingSieve) =    (s.support.filter (fun d => ∀ p:ℕ, p.Prime → p ≤ z → ¬p ∣ d)).card := by  dsimp only [siftedSum]  rw [Finset.card_eq_sum_ones, ←Finset.sum_filter, Nat.cast_sum]  apply Finset.sum_congr  · rw [hP]    ext d; constructor    · intro hd      rw [Finset.mem_filter] at *      constructor      · exact hd.1      · intro p hpp hpy        rw [←Nat.Prime.coprime_iff_not_dvd hpp]        apply Nat.Coprime.coprime_dvd_left _ hd.2        rw [prime_dvd_primorial_iff _ _ hpp]        apply Nat.le_floor hpy    · intro h      rw [Finset.mem_filter] at *      constructor      · exact h.1      refine Nat.coprime_of_dvd ?_      intro p hp      erw [prime_dvd_primorial_iff _ _ hp]      intro hpy      apply h.2 p hp      trans ↑(Nat.floor z)      · norm_cast      · apply Nat.floor_le        linarith only [hz]  simp_rw [Nat.cast_one]  intro x hx  simp only [Finset.mem_filter] at hx  apply hw x hx.1