norm_cast
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_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