have h_sq :
  (∑ d in n.divisors, ∑ d1 in d.divisors, ∑ d2 in d.divisors,
    if d = Nat.lcm d1 d2 then weights d1 * weights d2 else 0) =
    (∑ d in n.divisors, weights d) ^ 2 := by
  rw [sq, mul_sum, conv_lambda_sq_larger_sum _ n, sum_comm]
  apply sum_congr rfl; intro d1 hd1
  rw [sum_mul, sum_comm]
  apply sum_congr rfl; intro d2 hd2
  rw [←Aux.sum_intro]
  ring
  rw [mem_divisors, Nat.lcm_dvd_iff]
  exact ⟨⟨dvd_of_mem_divisors hd1, dvd_of_mem_divisors hd2⟩, (mem_divisors.mp hd1).2⟩
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
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h_sq :
  (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0) =
    (∑ d ∈ n.divisors, weights d) ^ 2
⊢ (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