calc
  |∑ d1 in n.divisors, ∑ d2 in n.divisors, if n = d1.lcm d2 then γ d1 * γ d2 else 0| ≤
      ∑ d1 in n.divisors, |∑ d2 in n.divisors, if n = d1.lcm d2 then γ d1 * γ d2 else 0| := ?_
  _ ≤ ∑ d1 in n.divisors, ∑ d2 in n.divisors, |if n = d1.lcm d2 then γ d1 * γ d2 else 0| := ?_
  _ ≤ ∑ d1 in n.divisors, ∑ d2 in n.divisors, f d1 d2 := ?_
  _ = (n.divisors ×ˢ n.divisors).sum fun p => f p.fst p.snd := ?_
  _ = Finset.card ((n.divisors ×ˢ n.divisors).filter fun p : ℕ × ℕ => n = p.fst.lcm p.snd) := ?_
  _ = (3:ℕ) ^ ω n := ?_
  _ = (3:ℝ) ^ ω n := ?_
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| ≤
    3 ^ ω n
case calc_1
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
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_3
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, f d1 d2

case calc_4
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, f d1 d2 = ∑ p ∈ n.divisors ×ˢ n.divisors, f p.1 p.2

case calc_5
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ ∑ p ∈ n.divisors ×ˢ n.divisors, f p.1 p.2 = ↑(filter (fun p => n = p.1.lcm p.2) (n.divisors ×ˢ n.divisors)).card

case calc_6
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ ↑(filter (fun p => n = p.1.lcm p.2) (n.divisors ×ˢ n.divisors)).card = ↑3 ^ ω n

case calc_7
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ ↑3 ^ ω n = 3 ^ ω n