gcongr
case calc_2
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ ∑ d1 ∈ n.divisors, |∑ d2 ∈ n.divisors, if n = d1.lcm d2 then s.selbergWeights d1 * s.selbergWeights d2 else 0| ≤
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, |if n = d1.lcm d2 then s.selbergWeights d1 * s.selbergWeights d2 else 0|
case calc_2.h
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
i✝ : ℕ
a✝ : i✝ ∈ n.divisors
⊢ |∑ d2 ∈ n.divisors, if n = i✝.lcm d2 then s.selbergWeights i✝ * s.selbergWeights d2 else 0| ≤
    ∑ d2 ∈ n.divisors, |if n = i✝.lcm d2 then s.selbergWeights i✝ * s.selbergWeights d2 else 0|