rw[h.1]
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
h : k = l ∧ ↑l ^ 2 ≤ y
⊢ ↑(μ l) * g k * S⁻¹ = g l * ↑(μ l) * S⁻¹
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
h : k = l ∧ ↑l ^ 2 ≤ y
⊢ ↑(μ l) * g l * S⁻¹ = g l * ↑(μ l) * S⁻¹