dsimp only [Nat.Coprime, delta] at *
s : Sieve
d : ℕ
a✝ : d ∈ A
⊢ (if P.Coprime d then s.weights d else 0) = s.weights d * δ (P.gcd d)
s : Sieve
d : ℕ
a✝ : d ∈ A
⊢ (if P.gcd d = 1 then s.weights d else 0) = s.weights d * if P.gcd d = 1 then 1 else 0