rw [sum_divisorsAntidiagonal' (f:=fun x y => (μ <| x) * (ν y)⁻¹) (n:=l)]
case a
s : Sieve
l : ℕ
a✝ : l > 0
hlP : l ∈ fun x => ∃ c, P = x * c
⊢ ∑ x ∈ l.divisorsAntidiagonal, ↑(μ x.1) * (ν x.2)⁻¹ = 1 / g l
case a
s : Sieve
l : ℕ
a✝ : l > 0
hlP : l ∈ fun x => ∃ c, P = x * c
⊢ ∑ i ∈ l.divisors, ↑(μ (l / i)) * (ν i)⁻¹ = 1 / g l