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