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

State before:
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ 1 / g l = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹
Tactic:
rw [selbergTerms_apply]
State after:
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ 1 / (ν l * ∏ p ∈ l.primeFactors, 1 / (1 - ν p)) = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹

State before:
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ 1 / (ν l * ∏ p ∈ l.primeFactors, 1 / (1 - ν p)) = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹
Tactic:
simp only [one_div, mul_inv, inv_div, inv_inv, Finset.prod_congr, Finset.prod_inv_distrib]
State after:
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ (ν l)⁻¹ * ∏ x ∈ l.primeFactors, (1 - ν x) = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹

State before:
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ (ν l)⁻¹ * ∏ x ∈ l.primeFactors, (1 - ν x) = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹
Tactic:
rw [(s.nu_mult).prodPrimeFactors_one_sub_of_squarefree _ hl]
State after:
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ (ν l)⁻¹ * ∑ d ∈ l.divisors, ↑(μ d) * ν d = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹

State before:
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ (ν l)⁻¹ * ∑ d ∈ l.divisors, ↑(μ d) * ν d = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹
Tactic:
rw [mul_sum]
State after:
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ ∑ i ∈ l.divisors, (ν l)⁻¹ * (↑(μ i) * ν i) = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹

State before:
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ ∑ i ∈ l.divisors, (ν l)⁻¹ * (↑(μ i) * ν i) = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹
Tactic:
apply symm
State after:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹ = ∑ i ∈ l.divisors, (ν l)⁻¹ * (↑(μ i) * ν i)

State before:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹ = ∑ i ∈ l.divisors, (ν l)⁻¹ * (↑(μ i) * ν i)
Tactic:
rw [← Nat.sum_divisorsAntidiagonal' fun d e : ℕ => ↑(μ d) * (ν e)⁻¹]
State after:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ ∑ i ∈ l.divisorsAntidiagonal, ↑(μ i.1) * (ν i.2)⁻¹ = ∑ i ∈ l.divisors, (ν l)⁻¹ * (↑(μ i) * ν i)

State before:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ ∑ i ∈ l.divisorsAntidiagonal, ↑(μ i.1) * (ν i.2)⁻¹ = ∑ i ∈ l.divisors, (ν l)⁻¹ * (↑(μ i) * ν i)
Tactic:
rw [Nat.sum_divisorsAntidiagonal fun d e : ℕ => ↑(μ d) * (ν e)⁻¹]
State after:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ ∑ i ∈ l.divisors, ↑(μ i) * (ν (l / i))⁻¹ = ∑ i ∈ l.divisors, (ν l)⁻¹ * (↑(μ i) * ν i)

State before:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ ∑ i ∈ l.divisors, ↑(μ i) * (ν (l / i))⁻¹ = ∑ i ∈ l.divisors, (ν l)⁻¹ * (↑(μ i) * ν i)
Tactic:
apply sum_congr rfl
State after:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ ∀ x ∈ l.divisors, ↑(μ x) * (ν (l / x))⁻¹ = (ν l)⁻¹ * (↑(μ x) * ν x)

State before:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ ∀ x ∈ l.divisors, ↑(μ x) * (ν (l / x))⁻¹ = (ν l)⁻¹ * (↑(μ x) * ν x)
Tactic:
intro d hd
State after:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
⊢ ↑(μ d) * (ν (l / d))⁻¹ = (ν l)⁻¹ * (↑(μ d) * ν d)

State before:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
⊢ ↑(μ d) * (ν (l / d))⁻¹ = (ν l)⁻¹ * (↑(μ d) * ν d)
Tactic:
have hd_dvd : d ∣ l := dvd_of_mem_divisors hd
State after:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ↑(μ d) * (ν (l / d))⁻¹ = (ν l)⁻¹ * (↑(μ d) * ν d)

State before:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ↑(μ d) * (ν (l / d))⁻¹ = (ν l)⁻¹ * (↑(μ d) * ν d)
Tactic:
rw [←div_mult_of_dvd_squarefree ν s.nu_mult l d (dvd_of_mem_divisors hd) hl, inv_div]
State after:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ↑(μ d) * (ν d / ν l) = (ν l)⁻¹ * (↑(μ d) * ν d)

case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ν d ≠ 0

State before:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ↑(μ d) * (ν d / ν l) = (ν l)⁻¹ * (↑(μ d) * ν d)

case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ν d ≠ 0
Tactic:
ring
State after:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ν d ≠ 0

State before:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ν d ≠ 0
Tactic:
revert hnu_nonzero
State after:
case a
s : Sieve
l : ℕ
hl : Squarefree l
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ν l ≠ 0 → ν d ≠ 0

State before:
case a
s : Sieve
l : ℕ
hl : Squarefree l
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ν l ≠ 0 → ν d ≠ 0
Tactic:
contrapose!
State after:
case a
s : Sieve
l : ℕ
hl : Squarefree l
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ν d = 0 → ν l = 0

State before:
case a
s : Sieve
l : ℕ
hl : Squarefree l
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ν d = 0 → ν l = 0
Tactic:
exact multiplicative_zero_of_zero_dvd ν s.nu_mult hl hd_dvd
State after:
no goals