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

State before:
s : Sieve
w : ℕ → ℝ
⊢ s.mainSum (lambdaSquared w) = ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0) ^ 2
Tactic:
rw [s.lambdaSquared_mainSum_eq_quad_form w]
State after:
s : Sieve
w : ℕ → ℝ
⊢ ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0) ^ 2

State before:
s : Sieve
w : ℕ → ℝ
⊢ ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0) ^ 2
Tactic:
trans (∑ d1 in divisors P, ∑ d2 in divisors P, (∑ l in divisors P,
        if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0))
State after:
s : Sieve
w : ℕ → ℝ
⊢ ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ d1 ∈ P.divisors,
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0

s : Sieve
w : ℕ → ℝ
⊢ (∑ d1 ∈ P.divisors,
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0) ^ 2

State before:
s : Sieve
w : ℕ → ℝ
⊢ (∑ d1 ∈ P.divisors,
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0) ^ 2
Tactic:
trans (∑ l in divisors P, ∑ d1 in divisors P, ∑ d2 in divisors P,
      if l ∣ Nat.gcd d1 d2 then 1 / selbergTerms s l * (ν d1 * w d1) * (ν d2 * w d2) else 0)
State after:
s : Sieve
w : ℕ → ℝ
⊢ (∑ d1 ∈ P.divisors,
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    ∑ l ∈ P.divisors,
      ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0

s : Sieve
w : ℕ → ℝ
⊢ (∑ l ∈ P.divisors,
      ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0) ^ 2

State before:
s : Sieve
w : ℕ → ℝ
⊢ (∑ l ∈ P.divisors,
      ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0) ^ 2
Tactic:
apply sum_congr rfl
State after:
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    (∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if x ∣ d1.gcd d2 then 1 / g x * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
      1 / g x * (∑ d ∈ P.divisors, if x ∣ d then ν d * w d else 0) ^ 2

State before:
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    (∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if x ∣ d1.gcd d2 then 1 / g x * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
      1 / g x * (∑ d ∈ P.divisors, if x ∣ d then ν d * w d else 0) ^ 2
Tactic:
intro l _
State after:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝ : l ∈ P.divisors
⊢ (∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0) ^ 2

State before:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝ : l ∈ P.divisors
⊢ (∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0) ^ 2
Tactic:
rw [sq, sum_mul, mul_sum, sum_congr rfl]
State after:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝ : l ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (∑ d2 ∈ P.divisors, if l ∣ x.gcd d2 then 1 / g l * (ν x * w x) * (ν d2 * w d2) else 0) =
      1 / g l * ((if l ∣ x then ν x * w x else 0) * ∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0)

State before:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝ : l ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (∑ d2 ∈ P.divisors, if l ∣ x.gcd d2 then 1 / g l * (ν x * w x) * (ν d2 * w d2) else 0) =
      1 / g l * ((if l ∣ x then ν x * w x else 0) * ∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0)
Tactic:
intro d1 _
State after:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝¹ : l ∈ P.divisors
d1 : ℕ
a✝ : d1 ∈ P.divisors
⊢ (∑ d2 ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    1 / g l * ((if l ∣ d1 then ν d1 * w d1 else 0) * ∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0)

State before:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝¹ : l ∈ P.divisors
d1 : ℕ
a✝ : d1 ∈ P.divisors
⊢ (∑ d2 ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    1 / g l * ((if l ∣ d1 then ν d1 * w d1 else 0) * ∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0)
Tactic:
rw [mul_sum, mul_sum, sum_congr rfl]
State after:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝¹ : l ∈ P.divisors
d1 : ℕ
a✝ : d1 ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if l ∣ d1.gcd x then 1 / g l * (ν d1 * w d1) * (ν x * w x) else 0) =
      1 / g l * ((if l ∣ d1 then ν d1 * w d1 else 0) * if l ∣ x then ν x * w x else 0)

State before:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝¹ : l ∈ P.divisors
d1 : ℕ
a✝ : d1 ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if l ∣ d1.gcd x then 1 / g l * (ν d1 * w d1) * (ν x * w x) else 0) =
      1 / g l * ((if l ∣ d1 then ν d1 * w d1 else 0) * if l ∣ x then ν x * w x else 0)
Tactic:
intro d2 _
State after:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝² : l ∈ P.divisors
d1 : ℕ
a✝¹ : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
⊢ (if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    1 / g l * ((if l ∣ d1 then ν d1 * w d1 else 0) * if l ∣ d2 then ν d2 * w d2 else 0)

State before:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝² : l ∈ P.divisors
d1 : ℕ
a✝¹ : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
⊢ (if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    1 / g l * ((if l ∣ d1 then ν d1 * w d1 else 0) * if l ∣ d2 then ν d2 * w d2 else 0)
Tactic:
rw [ite_zero_mul_ite_zero, mul_ite_zero]
State after:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝² : l ∈ P.divisors
d1 : ℕ
a✝¹ : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
⊢ (if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    if l ∣ d1 ∧ l ∣ d2 then 1 / g l * (ν d1 * w d1 * (ν d2 * w d2)) else 0

State before:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝² : l ∈ P.divisors
d1 : ℕ
a✝¹ : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
⊢ (if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    if l ∣ d1 ∧ l ∣ d2 then 1 / g l * (ν d1 * w d1 * (ν d2 * w d2)) else 0
Tactic:
apply if_congr (Nat.dvd_gcd_iff) _ rfl
State after:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝² : l ∈ P.divisors
d1 : ℕ
a✝¹ : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
⊢ 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) = 1 / g l * (ν d1 * w d1 * (ν d2 * w d2))

State before:
s : Sieve
w : ℕ → ℝ
l : ℕ
a✝² : l ∈ P.divisors
d1 : ℕ
a✝¹ : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
⊢ 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) = 1 / g l * (ν d1 * w d1 * (ν d2 * w d2))
Tactic:
ring
State after:
no goals

State before:
s : Sieve
w : ℕ → ℝ
⊢ ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ d1 ∈ P.divisors,
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
apply sum_congr rfl
State after:
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    ∑ d2 ∈ P.divisors, ν x * w x * ν d2 * w d2 * (ν (x.gcd d2))⁻¹ =
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ x.gcd d2 then 1 / g l * (ν x * w x) * (ν d2 * w d2) else 0

State before:
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    ∑ d2 ∈ P.divisors, ν x * w x * ν d2 * w d2 * (ν (x.gcd d2))⁻¹ =
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ x.gcd d2 then 1 / g l * (ν x * w x) * (ν d2 * w d2) else 0
Tactic:
intro d1 hd1
State after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
⊢ ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0

State before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
⊢ ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
apply sum_congr rfl
State after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    ν d1 * w d1 * ν x * w x * (ν (d1.gcd x))⁻¹ =
      ∑ l ∈ P.divisors, if l ∣ d1.gcd x then 1 / g l * (ν d1 * w d1) * (ν x * w x) else 0

State before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    ν d1 * w d1 * ν x * w x * (ν (d1.gcd x))⁻¹ =
      ∑ l ∈ P.divisors, if l ∣ d1.gcd x then 1 / g l * (ν d1 * w d1) * (ν x * w x) else 0
Tactic:
intro d2 _
State after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
⊢ ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0

State before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
⊢ ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
have hgcd_dvd: d1.gcd d2 ∣ P := Trans.trans (Nat.gcd_dvd_left d1 d2) (dvd_of_mem_divisors hd1)
State after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
⊢ ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0

State before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
⊢ ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
rw [s.nu_eq_conv_one_div_selbergTerms _ hgcd_dvd, mul_sum]
State after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
⊢ (∑ i ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * if i ∣ d1.gcd d2 then 1 / g i else 0) =
    ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0

State before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
⊢ (∑ i ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * if i ∣ d1.gcd d2 then 1 / g i else 0) =
    ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
apply sum_congr rfl
State after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
⊢ ∀ x ∈ P.divisors,
    (ν d1 * w d1 * ν d2 * w d2 * if x ∣ d1.gcd d2 then 1 / g x else 0) =
      if x ∣ d1.gcd d2 then 1 / g x * (ν d1 * w d1) * (ν d2 * w d2) else 0

State before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
⊢ ∀ x ∈ P.divisors,
    (ν d1 * w d1 * ν d2 * w d2 * if x ∣ d1.gcd d2 then 1 / g x else 0) =
      if x ∣ d1.gcd d2 then 1 / g x * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
intro l _
State after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝¹ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ (ν d1 * w d1 * ν d2 * w d2 * if l ∣ d1.gcd d2 then 1 / g l else 0) =
    if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0

State before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝¹ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ (ν d1 * w d1 * ν d2 * w d2 * if l ∣ d1.gcd d2 then 1 / g l else 0) =
    if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
rw [mul_ite_zero]
State after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝¹ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ (if l ∣ d1.gcd d2 then ν d1 * w d1 * ν d2 * w d2 * (1 / g l) else 0) =
    if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0

State before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝¹ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ (if l ∣ d1.gcd d2 then ν d1 * w d1 * ν d2 * w d2 * (1 / g l) else 0) =
    if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
apply if_congr Iff.rfl _ rfl
State after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝¹ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ ν d1 * w d1 * ν d2 * w d2 * (1 / g l) = 1 / g l * (ν d1 * w d1) * (ν d2 * w d2)

State before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝¹ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ ν d1 * w d1 * ν d2 * w d2 * (1 / g l) = 1 / g l * (ν d1 * w d1) * (ν d2 * w d2)
Tactic:
ring
State after:
no goals

State before:
s : Sieve
w : ℕ → ℝ
⊢ (∑ d1 ∈ P.divisors,
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    ∑ l ∈ P.divisors,
      ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
apply symm
State after:
case a
s : Sieve
w : ℕ → ℝ
⊢ (∑ l ∈ P.divisors,
      ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    ∑ d1 ∈ P.divisors,
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0

State before:
case a
s : Sieve
w : ℕ → ℝ
⊢ (∑ l ∈ P.divisors,
      ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    ∑ d1 ∈ P.divisors,
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
rw [sum_comm, sum_congr rfl]
State after:
case a
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    (∑ x_1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if x_1 ∣ x.gcd d2 then 1 / g x_1 * (ν x * w x) * (ν d2 * w d2) else 0) =
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ x.gcd d2 then 1 / g l * (ν x * w x) * (ν d2 * w d2) else 0

State before:
case a
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    (∑ x_1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if x_1 ∣ x.gcd d2 then 1 / g x_1 * (ν x * w x) * (ν d2 * w d2) else 0) =
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ x.gcd d2 then 1 / g l * (ν x * w x) * (ν d2 * w d2) else 0
Tactic:
intro d1 _
State after:
case a
s : Sieve
w : ℕ → ℝ
d1 : ℕ
a✝ : d1 ∈ P.divisors
⊢ (∑ x ∈ P.divisors, ∑ d2 ∈ P.divisors, if x ∣ d1.gcd d2 then 1 / g x * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0

State before:
case a
s : Sieve
w : ℕ → ℝ
d1 : ℕ
a✝ : d1 ∈ P.divisors
⊢ (∑ x ∈ P.divisors, ∑ d2 ∈ P.divisors, if x ∣ d1.gcd d2 then 1 / g x * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
rw[sum_comm]
State after:
no goals