intro l _
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
⊢ ∀ x ∈ P.divisors,
    (ν d1 * w d1 * ν d2 * w d2 * if x ∣ d1.gcd d2 then 1 / g x else 0) =
      if x ∣ d1.gcd d2 then 1 / g x * (ν d1 * w d1) * (ν d2 * w d2) else 0
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝¹ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ (ν d1 * w d1 * ν d2 * w d2 * if l ∣ d1.gcd d2 then 1 / g l else 0) =
    if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0