intro d hd
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
⊢ ∀ x ∈ P.divisors,
    (if x ∣ P.gcd n then s.weights n * μPlus.μPlus x else 0) = if x ∣ n then s.weights n * μPlus.μPlus x else 0
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
d : ℕ
hd : d ∈ P.divisors
⊢ (if d ∣ P.gcd n then s.weights n * μPlus.μPlus d else 0) = if d ∣ n then s.weights n * μPlus.μPlus d else 0