apply (ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq_on _ (fun _ _ => Nat.dvd_trans)).mpr
case a
s : Sieve
⊢ ∀ (d : ℕ), 0 < d → d ∣ P → ∑ a ∈ d.divisors, 1 / g a = (ν d)⁻¹
case a
s : Sieve
⊢ ∀ n > 0, (n ∈ fun x => ∃ c, P = x * c) → ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * (ν x.2)⁻¹ = 1 / g n