rw[primeInterSieve]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (∑ n ∈ (primeInterSieve x y z hz).support, if d ∣ n then (primeInterSieve x y z hz).weights n else 0) =
    ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d)
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (∑
      n ∈
        { support := Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊, prodPrimes := primorial ⌊z⌋₊, prodPrimes_squarefree := ⋯,
            weights := fun x => 1, weights_nonneg := primeInterSieve.proof_2, totalMass := y,
            nu := (↑ζ).pdiv ↑ArithmeticFunction.id, nu_mult := primeInterSieve.proof_3, nu_pos_of_prime := ⋯,
            nu_lt_one_of_prime := ⋯, level := z, one_le_level := hz }.support,
      if d ∣ n then
        { support := Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊, prodPrimes := primorial ⌊z⌋₊, prodPrimes_squarefree := ⋯,
              weights := fun x => 1, weights_nonneg := primeInterSieve.proof_2, totalMass := y,
              nu := (↑ζ).pdiv ↑ArithmeticFunction.id, nu_mult := primeInterSieve.proof_3, nu_pos_of_prime := ⋯,
              nu_lt_one_of_prime := ⋯, level := z, one_le_level := hz }.weights
          n
      else 0) =
    ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d)