apply and_congr_right
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ k = l ∧ ↑k ^ 2 ≤ y ↔ k = l ∧ ↑l ^ 2 ≤ y

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

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