apply if_ctx_congr _ _ fun _ => rfl
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 ∧ k = d.gcd (k * m) ∧ ↑(k * m) ^ 2 ≤ y then g (k * m) else 0) =
    if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g k * 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
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ k * m ∣ P ∧ k = d.gcd (k * m) ∧ ↑(k * m) ^ 2 ≤ y ↔ (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d

s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d → g (k * m) = g k * g m

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