apply if_ctx_congr _ _ fun _ => rfl
case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
⊢ (if d * m ∣ P ∧ d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y then S⁻¹ * ↑(μ d) * g (d * m) else 0) =
    if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * g m) else 0

case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ∀ (l : ℕ), l ∣ P → ¬d ∣ l → (S⁻¹ * ↑(μ d) * if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
⊢ d * m ∣ P ∧ d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y ↔ (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d

s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
⊢ (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d → S⁻¹ * ↑(μ d) * g (d * m) = ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * g m)

case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ∀ (l : ℕ), l ∣ P → ¬d ∣ l → (S⁻¹ * ↑(μ d) * if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0