dsimp [UpperMoebius, lambdaSquared]
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
⊢ UpperMoebius (lambdaSquared weights)
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
⊢ ∀ (n : ℕ),
    (if n = 1 then 1 else 0) ≤
      ∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0