apply if_ctx_congr Iff.rfl _ (fun _ => rfl)
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
⊢ (if l ∣ d then g (d / l) else 0) = if l ∣ d then g d * (1 / g l) else 0
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
⊢ l ∣ d → g (d / l) = g d * (1 / g l)