intro m hm
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ x ∈ P.divisors,
    (if k * x ∣ P then if k = d.gcd (k * x) ∧ ↑(k * x) ^ 2 ≤ y then g (k * x) else 0 else 0) =
      g k * if (↑k * ↑x) ^ 2 ≤ y ∧ x.Coprime d then g x else 0

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ (l : ℕ), l ∣ P → ¬k ∣ l → (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ (if k * m ∣ P then if k = d.gcd (k * m) ∧ ↑(k * m) ^ 2 ≤ y then g (k * m) else 0 else 0) =
    g k * if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ (l : ℕ), l ∣ P → ¬k ∣ l → (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0