rw [if_pos (one_dvd P), s.nu_mult.left, s.selbergTerms_mult.left]
s : SelbergSieve
⊢ (if 1 ∣ P then (ν 1)⁻¹ * g 1 * ↑(μ 1) * S⁻¹ * ∑ m ∈ P.divisors, if (↑1 * ↑m) ^ 2 ≤ y ∧ m.Coprime 1 then g m else 0
    else 0) =
    1
s : SelbergSieve
⊢ (1⁻¹ * 1 * ↑(μ 1) * S⁻¹ * ∑ m ∈ P.divisors, if (↑1 * ↑m) ^ 2 ≤ y ∧ m.Coprime 1 then g m else 0) = 1