rw [Nat.dvd_gcd_iff, and_iff_right (dvd_of_mem_divisors hd)]
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
d : ℕ
hd : d ∈ P.divisors
⊢ d ∣ P.gcd n ↔ d ∣ n
no goals