intro k _
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (∑ x_1 ∈ P.divisors, if l ∣ x_1 ∧ x_1 ∣ x ∧ ↑x ^ 2 ≤ y then g x * S⁻¹ * ↑(μ x_1) else 0) =
      if ↑x ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ x then ↑(μ d) else 0) * g x * S⁻¹ else 0
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ (∑ x ∈ P.divisors, if l ∣ x ∧ x ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ x) else 0) =
    if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0