Theorem: SelbergSieve.selbergWeights_eq_dvds_sum (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean)

State before:
s : SelbergSieve
d : ℕ
⊢ ν d * s.selbergWeights d = S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0
Tactic:
by_cases h_dvd : d ∣ P
State after:
case pos
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ν d * s.selbergWeights d = S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0

case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
⊢ ν d * s.selbergWeights d = S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0

State before:
case pos
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ν d * s.selbergWeights d = S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0

case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
⊢ ν d * s.selbergWeights d = S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0
Tactic:
swap
State after:
case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
⊢ ν d * s.selbergWeights d = S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0

case pos
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ν d * s.selbergWeights d = S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0

State before:
case pos
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ν d * s.selbergWeights d = S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0
Tactic:
dsimp only [selbergWeights]
State after:
case pos
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ (ν d *
      if d ∣ P then (ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0
      else 0) =
    S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0

State before:
case pos
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ (ν d *
      if d ∣ P then (ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0
      else 0) =
    S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0
Tactic:
rw [if_pos h_dvd]
State after:
case pos
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) =
    S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0

State before:
case pos
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) =
    S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0
Tactic:
repeat rw [mul_sum]
State after:
case pos
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ∑ i ∈ P.divisors, ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * if (↑d * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0) =
    ∑ i ∈ P.divisors, S⁻¹ * ↑(μ d) * if d ∣ i ∧ ↑i ^ 2 ≤ y then g i else 0

State before:
case pos
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ∑ i ∈ P.divisors, ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * if (↑d * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0) =
    ∑ i ∈ P.divisors, S⁻¹ * ↑(μ d) * if d ∣ i ∧ ↑i ^ 2 ≤ y then g i else 0
Tactic:
apply symm
State after:
case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ (∑ i ∈ P.divisors, S⁻¹ * ↑(μ d) * if d ∣ i ∧ ↑i ^ 2 ≤ y then g i else 0) =
    ∑ i ∈ P.divisors, ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * if (↑d * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0)

State before:
case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ (∑ i ∈ P.divisors, S⁻¹ * ↑(μ d) * if d ∣ i ∧ ↑i ^ 2 ≤ y then g i else 0) =
    ∑ i ∈ P.divisors, ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * if (↑d * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0)
Tactic:
rw [sum_mul_subst d P]
State after:
case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ (∑ m ∈ P.divisors, if d * m ∣ P then S⁻¹ * ↑(μ d) * if d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y then g (d * m) else 0 else 0) =
    ∑ i ∈ P.divisors, ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * if (↑d * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0)

case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ∀ (l : ℕ), l ∣ P → ¬d ∣ l → (S⁻¹ * ↑(μ d) * if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0

State before:
case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ (∑ m ∈ P.divisors, if d * m ∣ P then S⁻¹ * ↑(μ d) * if d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y then g (d * m) else 0 else 0) =
    ∑ i ∈ P.divisors, ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * if (↑d * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0)

case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ∀ (l : ℕ), l ∣ P → ¬d ∣ l → (S⁻¹ * ↑(μ d) * if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
apply sum_congr rfl
State after:
case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ∀ x ∈ P.divisors,
    (if d * x ∣ P then S⁻¹ * ↑(μ d) * if d ∣ d * x ∧ ↑(d * x) ^ 2 ≤ y then g (d * x) else 0 else 0) =
      ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * if (↑d * ↑x) ^ 2 ≤ y ∧ x.Coprime d then g x else 0)

case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ∀ (l : ℕ), l ∣ P → ¬d ∣ l → (S⁻¹ * ↑(μ d) * if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0

State before:
case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ∀ x ∈ P.divisors,
    (if d * x ∣ P then S⁻¹ * ↑(μ d) * if d ∣ d * x ∧ ↑(d * x) ^ 2 ≤ y then g (d * x) else 0 else 0) =
      ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * if (↑d * ↑x) ^ 2 ≤ y ∧ x.Coprime d then g x else 0)

case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ∀ (l : ℕ), l ∣ P → ¬d ∣ l → (S⁻¹ * ↑(μ d) * if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
intro m hm
State after:
case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
⊢ (if d * m ∣ P then S⁻¹ * ↑(μ d) * if d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y then g (d * m) else 0 else 0) =
    ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0)

case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ∀ (l : ℕ), l ∣ P → ¬d ∣ l → (S⁻¹ * ↑(μ d) * if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0

State before:
case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
⊢ (if d * m ∣ P then S⁻¹ * ↑(μ d) * if d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y then g (d * m) else 0 else 0) =
    ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0)

case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ∀ (l : ℕ), l ∣ P → ¬d ∣ l → (S⁻¹ * ↑(μ d) * if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
rw [mul_ite_zero, ←ite_and, mul_ite_zero, mul_ite_zero]
State after:
case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
⊢ (if d * m ∣ P ∧ d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y then S⁻¹ * ↑(μ d) * g (d * m) else 0) =
    if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * g m) else 0

case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ∀ (l : ℕ), l ∣ P → ¬d ∣ l → (S⁻¹ * ↑(μ d) * if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0

State before:
case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
⊢ (if d * m ∣ P ∧ d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y then S⁻¹ * ↑(μ d) * g (d * m) else 0) =
    if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * g m) else 0

case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ∀ (l : ℕ), l ∣ P → ¬d ∣ l → (S⁻¹ * ↑(μ d) * if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
apply if_ctx_congr _ _ fun _ => rfl
State after:
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
⊢ d * m ∣ P ∧ d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y ↔ (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d

s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
⊢ (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d → S⁻¹ * ↑(μ d) * g (d * m) = ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * g m)

case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ∀ (l : ℕ), l ∣ P → ¬d ∣ l → (S⁻¹ * ↑(μ d) * if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0

State before:
case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
⊢ ν d * s.selbergWeights d = S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0
Tactic:
dsimp only [selbergWeights]
State after:
case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
⊢ (ν d *
      if d ∣ P then (ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0
      else 0) =
    S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0

State before:
case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
⊢ (ν d *
      if d ∣ P then (ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0
      else 0) =
    S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0
Tactic:
rw [if_neg h_dvd]
State after:
case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
⊢ ν d * 0 = S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0

State before:
case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
⊢ ν d * 0 = S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0
Tactic:
rw [sum_eq_zero]
State after:
case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
⊢ ν d * 0 = S⁻¹ * ↑(μ d) * 0

case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
⊢ ∀ x ∈ P.divisors, (if d ∣ x ∧ ↑x ^ 2 ≤ y then g x else 0) = 0

State before:
case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
⊢ ν d * 0 = S⁻¹ * ↑(μ d) * 0

case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
⊢ ∀ x ∈ P.divisors, (if d ∣ x ∧ ↑x ^ 2 ≤ y then g x else 0) = 0
Tactic:
ring
State after:
case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
⊢ ∀ x ∈ P.divisors, (if d ∣ x ∧ ↑x ^ 2 ≤ y then g x else 0) = 0

State before:
case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
⊢ ∀ x ∈ P.divisors, (if d ∣ x ∧ ↑x ^ 2 ≤ y then g x else 0) = 0
Tactic:
intro l hl
State after:
case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
l : ℕ
hl : l ∈ P.divisors
⊢ (if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0

State before:
case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
l : ℕ
hl : l ∈ P.divisors
⊢ (if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
rw [mem_divisors] at hl
State after:
case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
⊢ (if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0

State before:
case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
⊢ (if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
rw [if_neg]
State after:
case neg.hnc
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
⊢ ¬(d ∣ l ∧ ↑l ^ 2 ≤ y)

State before:
case neg.hnc
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
⊢ ¬(d ∣ l ∧ ↑l ^ 2 ≤ y)
Tactic:
push_neg
State after:
case neg.hnc
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
⊢ d ∣ l → y < ↑l ^ 2

State before:
case neg.hnc
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
⊢ d ∣ l → y < ↑l ^ 2
Tactic:
intro h
State after:
case neg.hnc
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
h : d ∣ l
⊢ y < ↑l ^ 2

State before:
case neg.hnc
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
h : d ∣ l
⊢ y < ↑l ^ 2
Tactic:
exfalso
State after:
case neg.hnc
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
h : d ∣ l
⊢ False

State before:
case neg.hnc
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
h : d ∣ l
⊢ False
Tactic:
exact h_dvd (dvd_trans h hl.left)
State after:
no goals

State before:
case pos
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ∑ i ∈ P.divisors, ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * if (↑d * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0) =
    S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0
Tactic:
rw [mul_sum]
State after:
case pos
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ∑ i ∈ P.divisors, ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * if (↑d * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0) =
    ∑ i ∈ P.divisors, S⁻¹ * ↑(μ d) * if d ∣ i ∧ ↑i ^ 2 ≤ y then g i else 0

State before:
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
⊢ d * m ∣ P ∧ d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y ↔ (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
Tactic:
rw [coprime_comm]
State after:
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
⊢ d * m ∣ P ∧ d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y ↔ (↑d * ↑m) ^ 2 ≤ y ∧ d.Coprime m

State before:
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
⊢ d * m ∣ P ∧ d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y ↔ (↑d * ↑m) ^ 2 ≤ y ∧ d.Coprime m
Tactic:
constructor
State after:
case mp
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
⊢ d * m ∣ P ∧ d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y → (↑d * ↑m) ^ 2 ≤ y ∧ d.Coprime m

case mpr
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
⊢ (↑d * ↑m) ^ 2 ≤ y ∧ d.Coprime m → d * m ∣ P ∧ d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y

State before:
case mp
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
⊢ d * m ∣ P ∧ d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y → (↑d * ↑m) ^ 2 ≤ y ∧ d.Coprime m
Tactic:
intro h
State after:
case mp
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
h : d * m ∣ P ∧ d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y
⊢ (↑d * ↑m) ^ 2 ≤ y ∧ d.Coprime m

State before:
case mp
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
h : d * m ∣ P ∧ d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y
⊢ (↑d * ↑m) ^ 2 ≤ y ∧ d.Coprime m
Tactic:
push_cast at h
State after:
case mp
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
h : d * m ∣ P ∧ d ∣ d * m ∧ (↑d * ↑m) ^ 2 ≤ y
⊢ (↑d * ↑m) ^ 2 ≤ y ∧ d.Coprime m

State before:
case mp
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
h : d * m ∣ P ∧ d ∣ d * m ∧ (↑d * ↑m) ^ 2 ≤ y
⊢ (↑d * ↑m) ^ 2 ≤ y ∧ d.Coprime m
Tactic:
exact ⟨h.2.2, coprime_of_squarefree_mul $ Squarefree.squarefree_of_dvd h.1 s.prodPrimes_squarefree⟩
State after:
no goals

State before:
case mpr
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
⊢ (↑d * ↑m) ^ 2 ≤ y ∧ d.Coprime m → d * m ∣ P ∧ d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y
Tactic:
intro h
State after:
case mpr
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ d.Coprime m
⊢ d * m ∣ P ∧ d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y

State before:
case mpr
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ d.Coprime m
⊢ d * m ∣ P ∧ d ∣ d * m ∧ ↑(d * m) ^ 2 ≤ y
Tactic:
push_cast
State after:
case mpr
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ d.Coprime m
⊢ d * m ∣ P ∧ d ∣ d * m ∧ (↑d * ↑m) ^ 2 ≤ y

State before:
case mpr
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ d.Coprime m
⊢ d * m ∣ P ∧ d ∣ d * m ∧ (↑d * ↑m) ^ 2 ≤ y
Tactic:
exact ⟨ Coprime.mul_dvd_of_dvd_of_dvd h.2 h_dvd (dvd_of_mem_divisors hm), Nat.dvd_mul_right d m, h.1⟩
State after:
no goals

State before:
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
⊢ (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d → S⁻¹ * ↑(μ d) * g (d * m) = ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * g m)
Tactic:
intro h
State after:
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ S⁻¹ * ↑(μ d) * g (d * m) = ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * g m)

State before:
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ S⁻¹ * ↑(μ d) * g (d * m) = ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * g m)
Tactic:
trans ((ν d)⁻¹ * (ν d) * g d * μ d / S * g m)
State after:
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ S⁻¹ * ↑(μ d) * g (d * m) = (ν d)⁻¹ * ν d * g d * ↑(μ d) / S * g m

s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ (ν d)⁻¹ * ν d * g d * ↑(μ d) / S * g m = ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * g m)

State before:
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ (ν d)⁻¹ * ν d * g d * ↑(μ d) / S * g m = ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * g m)
Tactic:
ring
State after:
no goals

State before:
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ S⁻¹ * ↑(μ d) * g (d * m) = (ν d)⁻¹ * ν d * g d * ↑(μ d) / S * g m
Tactic:
rw [inv_mul_cancel (s.nu_ne_zero h_dvd), s.selbergTerms_mult.map_mul_of_coprime
  $ coprime_comm.mp h.2]
State after:
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ S⁻¹ * ↑(μ d) * (g d * g m) = 1 * g d * ↑(μ d) / S * g m

State before:
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ S⁻¹ * ↑(μ d) * (g d * g m) = 1 * g d * ↑(μ d) / S * g m
Tactic:
ring
State after:
no goals

State before:
case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ∀ (l : ℕ), l ∣ P → ¬d ∣ l → (S⁻¹ * ↑(μ d) * if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
intro l _ hdl
State after:
case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
l : ℕ
a✝ : l ∣ P
hdl : ¬d ∣ l
⊢ (S⁻¹ * ↑(μ d) * if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0

State before:
case pos.a
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
l : ℕ
a✝ : l ∣ P
hdl : ¬d ∣ l
⊢ (S⁻¹ * ↑(μ d) * if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
rw [if_neg, mul_zero]
State after:
case pos.a.hnc
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
l : ℕ
a✝ : l ∣ P
hdl : ¬d ∣ l
⊢ ¬(d ∣ l ∧ ↑l ^ 2 ≤ y)

State before:
case pos.a.hnc
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
l : ℕ
a✝ : l ∣ P
hdl : ¬d ∣ l
⊢ ¬(d ∣ l ∧ ↑l ^ 2 ≤ y)
Tactic:
push_neg
State after:
case pos.a.hnc
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
l : ℕ
a✝ : l ∣ P
hdl : ¬d ∣ l
⊢ d ∣ l → y < ↑l ^ 2

State before:
case pos.a.hnc
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
l : ℕ
a✝ : l ∣ P
hdl : ¬d ∣ l
⊢ d ∣ l → y < ↑l ^ 2
Tactic:
intro h
State after:
case pos.a.hnc
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
l : ℕ
a✝ : l ∣ P
hdl : ¬d ∣ l
h : d ∣ l
⊢ y < ↑l ^ 2

State before:
case pos.a.hnc
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
l : ℕ
a✝ : l ∣ P
hdl : ¬d ∣ l
h : d ∣ l
⊢ y < ↑l ^ 2
Tactic:
contradiction
State after:
no goals