Theorem: Sieve.nu_eq_conv_one_div_selbergTerms (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean)

State before:
s : Sieve
d : ℕ
hdP : d ∣ P
⊢ (ν d)⁻¹ = ∑ l ∈ P.divisors, if l ∣ d then 1 / g l else 0
Tactic:
apply symm
State after:
case a
s : Sieve
d : ℕ
hdP : d ∣ P
⊢ (∑ l ∈ P.divisors, if l ∣ d then 1 / g l else 0) = (ν d)⁻¹

State before:
case a
s : Sieve
d : ℕ
hdP : d ∣ P
⊢ (∑ l ∈ P.divisors, if l ∣ d then 1 / g l else 0) = (ν d)⁻¹
Tactic:
rw [←sum_filter, Nat.divisors_filter_dvd_of_dvd s.prodPrimes_ne_zero hdP]
State after:
case a
s : Sieve
d : ℕ
hdP : d ∣ P
⊢ ∑ a ∈ d.divisors, 1 / g a = (ν d)⁻¹

State before:
case a
s : Sieve
d : ℕ
hdP : d ∣ P
⊢ ∑ a ∈ d.divisors, 1 / g a = (ν d)⁻¹
Tactic:
have hd_pos : 0 < d := Nat.pos_of_ne_zero $ ne_zero_of_dvd_ne_zero s.prodPrimes_ne_zero hdP
State after:
case a
s : Sieve
d : ℕ
hdP : d ∣ P
hd_pos : 0 < d
⊢ ∑ a ∈ d.divisors, 1 / g a = (ν d)⁻¹

State before:
case a
s : Sieve
d : ℕ
hdP : d ∣ P
hd_pos : 0 < d
⊢ ∑ a ∈ d.divisors, 1 / g a = (ν d)⁻¹
Tactic:
revert hdP
State after:
case a
s : Sieve
d : ℕ
hd_pos : 0 < d
⊢ d ∣ P → ∑ a ∈ d.divisors, 1 / g a = (ν d)⁻¹

State before:
case a
s : Sieve
d : ℕ
hd_pos : 0 < d
⊢ d ∣ P → ∑ a ∈ d.divisors, 1 / g a = (ν d)⁻¹
Tactic:
revert d
State after:
case a
s : Sieve
⊢ ∀ (d : ℕ), 0 < d → d ∣ P → ∑ a ∈ d.divisors, 1 / g a = (ν d)⁻¹

State before:
case a
s : Sieve
⊢ ∀ (d : ℕ), 0 < d → d ∣ P → ∑ a ∈ d.divisors, 1 / g a = (ν d)⁻¹
Tactic:
apply (ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq_on _ (fun _ _ => Nat.dvd_trans)).mpr
State after:
case a
s : Sieve
⊢ ∀ n > 0, (n ∈ fun x => ∃ c, P = x * c) → ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * (ν x.2)⁻¹ = 1 / g n

State before:
case a
s : Sieve
⊢ ∀ n > 0, (n ∈ fun x => ∃ c, P = x * c) → ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * (ν x.2)⁻¹ = 1 / g n
Tactic:
intro l _ hlP
State after:
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

State before:
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
Tactic:
rw [sum_divisorsAntidiagonal' (f:=fun x y => (μ <| x) * (ν y)⁻¹) (n:=l)]
State after:
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

State before:
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
Tactic:
apply symm
State after:
case a.a
s : Sieve
l : ℕ
a✝ : l > 0
hlP : l ∈ fun x => ∃ c, P = x * c
⊢ 1 / g l = ∑ i ∈ l.divisors, ↑(μ (l / i)) * (ν i)⁻¹

State before:
case a.a
s : Sieve
l : ℕ
a✝ : l > 0
hlP : l ∈ fun x => ∃ c, P = x * c
⊢ 1 / g l = ∑ i ∈ l.divisors, ↑(μ (l / i)) * (ν i)⁻¹
Tactic:
exact s.one_div_selbergTerms_eq_conv_moebius_nu l
  (Squarefree.squarefree_of_dvd hlP s.prodPrimes_squarefree)
  (_root_.ne_of_gt $ s.nu_pos_of_dvd_prodPrimes hlP)
State after:
no goals