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

State before:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ (∑ l ∈ P.divisors, if l ∣ d then g l else 0) = g d * (ν d)⁻¹
Tactic:
calc
  (∑ l in divisors P, if l ∣ d then g l else 0) =
      ∑ l in divisors P, if l ∣ d then g (d / l) else 0 := by
    rw [← sum_over_dvd_ite s.prodPrimes_ne_zero hd,
      ← Nat.sum_divisorsAntidiagonal fun x _ => g x, Nat.sum_divisorsAntidiagonal' fun x _ => g x,
      sum_over_dvd_ite s.prodPrimes_ne_zero hd]
  _ = g d * ∑ l in divisors P, if l ∣ d then 1 / g l else 0 := by
    rw [mul_sum]; apply sum_congr rfl; intro l hl
    rw [mul_ite_zero]; apply if_ctx_congr Iff.rfl _ (fun _ => rfl); intro h
    rw [← div_mult_of_dvd_squarefree g s.selbergTerms_mult d l]; ring
    exact h; apply Squarefree.squarefree_of_dvd hd s.prodPrimes_squarefree
    apply _root_.ne_of_gt; rw [mem_divisors] at hl ; apply selbergTerms_pos; exact hl.left
  _ = g d * (ν d)⁻¹ := by rw [← s.nu_eq_conv_one_div_selbergTerms d hd]
State after:
no goals

State before:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ (∑ l ∈ P.divisors, if l ∣ d then g l else 0) = ∑ l ∈ P.divisors, if l ∣ d then g (d / l) else 0
Tactic:
rw [← sum_over_dvd_ite s.prodPrimes_ne_zero hd,
  ← Nat.sum_divisorsAntidiagonal fun x _ => g x, Nat.sum_divisorsAntidiagonal' fun x _ => g x,
  sum_over_dvd_ite s.prodPrimes_ne_zero hd]
State after:
no goals

State before:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ (∑ l ∈ P.divisors, if l ∣ d then g (d / l) else 0) = g d * ∑ l ∈ P.divisors, if l ∣ d then 1 / g l else 0
Tactic:
rw [mul_sum]
State after:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ (∑ l ∈ P.divisors, if l ∣ d then g (d / l) else 0) = ∑ i ∈ P.divisors, g d * if i ∣ d then 1 / g i else 0

State before:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ (∑ l ∈ P.divisors, if l ∣ d then g (d / l) else 0) = ∑ i ∈ P.divisors, g d * if i ∣ d then 1 / g i else 0
Tactic:
apply sum_congr rfl
State after:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ ∀ x ∈ P.divisors, (if x ∣ d then g (d / x) else 0) = g d * if x ∣ d then 1 / g x else 0

State before:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ ∀ x ∈ P.divisors, (if x ∣ d then g (d / x) else 0) = g d * if x ∣ d then 1 / g x else 0
Tactic:
intro l hl
State after:
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
⊢ (if l ∣ d then g (d / l) else 0) = g d * if l ∣ d then 1 / g l else 0

State before:
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
⊢ (if l ∣ d then g (d / l) else 0) = g d * if l ∣ d then 1 / g l else 0
Tactic:
rw [mul_ite_zero]
State after:
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
⊢ (if l ∣ d then g (d / l) else 0) = if l ∣ d then g d * (1 / g l) else 0

State before:
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
⊢ (if l ∣ d then g (d / l) else 0) = if l ∣ d then g d * (1 / g l) else 0
Tactic:
apply if_ctx_congr Iff.rfl _ (fun _ => rfl)
State after:
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
⊢ l ∣ d → g (d / l) = g d * (1 / g l)

State before:
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
⊢ l ∣ d → g (d / l) = g d * (1 / g l)
Tactic:
intro h
State after:
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g (d / l) = g d * (1 / g l)

State before:
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g (d / l) = g d * (1 / g l)
Tactic:
rw [← div_mult_of_dvd_squarefree g s.selbergTerms_mult d l]
State after:
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g d / g l = g d * (1 / g l)

case hdl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ l ∣ d

case hl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ Squarefree d

case hd
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g l ≠ 0

State before:
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g d / g l = g d * (1 / g l)

case hdl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ l ∣ d

case hl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ Squarefree d

case hd
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g l ≠ 0
Tactic:
ring
State after:
case hdl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ l ∣ d

case hl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ Squarefree d

case hd
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g l ≠ 0

State before:
case hdl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ l ∣ d

case hl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ Squarefree d

case hd
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g l ≠ 0
Tactic:
exact h
State after:
case hl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ Squarefree d

case hd
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g l ≠ 0

State before:
case hl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ Squarefree d

case hd
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g l ≠ 0
Tactic:
apply Squarefree.squarefree_of_dvd hd s.prodPrimes_squarefree
State after:
case hd
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g l ≠ 0

State before:
case hd
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g l ≠ 0
Tactic:
apply _root_.ne_of_gt
State after:
case hd.h
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ 0 < g l

State before:
case hd.h
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ 0 < g l
Tactic:
rw [mem_divisors] at hl
State after:
case hd.h
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
h : l ∣ d
⊢ 0 < g l

State before:
case hd.h
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
h : l ∣ d
⊢ 0 < g l
Tactic:
apply selbergTerms_pos
State after:
case hd.h.hl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
h : l ∣ d
⊢ l ∣ P

State before:
case hd.h.hl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
h : l ∣ d
⊢ l ∣ P
Tactic:
exact hl.left
State after:
no goals

State before:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ (g d * ∑ l ∈ P.divisors, if l ∣ d then 1 / g l else 0) = g d * (ν d)⁻¹
Tactic:
rw [← s.nu_eq_conv_one_div_selbergTerms d hd]
State after:
no goals