internlm/Lean-Github huggingface dataset:
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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]
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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]
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof 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)
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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]
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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]
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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]
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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]
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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]
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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]
Proof state after:
case neg.hnc
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
⊢ ¬(d ∣ l ∧ ↑l ^ 2 ≤ y)
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof state after:
case neg.hnc
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
⊢ d ∣ l → y < ↑l ^ 2
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof state after:
case neg.hnc
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
h : d ∣ l
⊢ y < ↑l ^ 2
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof state after:
case neg.hnc
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
h : d ∣ l
⊢ False
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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)
Proof state after:
no goals
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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]
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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]
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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⟩
Proof state after:
no goals
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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⟩
Proof state after:
no goals
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof 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)
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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)
Proof 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)
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof state after:
no goals
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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]
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof state after:
no goals
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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]
Proof 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)
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof 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
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof 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
Proof state after:
no goals
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (∑ d ∈ P.divisors, if l ∣ d then ν d * s.selbergWeights d else 0) =
    ∑ d ∈ P.divisors, ∑ k ∈ P.divisors, if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
Tactic:
apply sum_congr rfl
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if l ∣ x then ν x * s.selbergWeights x else 0) =
      ∑ k ∈ P.divisors, if l ∣ x ∧ x ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ x) else 0
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if l ∣ x then ν x * s.selbergWeights x else 0) =
      ∑ k ∈ P.divisors, if l ∣ x ∧ x ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ x) else 0
Tactic:
intro d _
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ (if l ∣ d then ν d * s.selbergWeights d else 0) =
    ∑ k ∈ P.divisors, if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ (if l ∣ d then ν d * s.selbergWeights d else 0) =
    ∑ k ∈ P.divisors, if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
Tactic:
rw [selbergWeights_eq_dvds_sum, ← boole_mul, mul_sum, mul_sum]
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ ∑ i ∈ P.divisors, (if l ∣ d then 1 else 0) * (S⁻¹ * ↑(μ d) * if d ∣ i ∧ ↑i ^ 2 ≤ y then g i else 0) =
    ∑ k ∈ P.divisors, if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ ∑ i ∈ P.divisors, (if l ∣ d then 1 else 0) * (S⁻¹ * ↑(μ d) * if d ∣ i ∧ ↑i ^ 2 ≤ y then g i else 0) =
    ∑ k ∈ P.divisors, if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
Tactic:
apply sum_congr rfl
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if l ∣ d then 1 else 0) * (S⁻¹ * ↑(μ d) * if d ∣ x ∧ ↑x ^ 2 ≤ y then g x else 0) =
      if l ∣ d ∧ d ∣ x ∧ ↑x ^ 2 ≤ y then g x * S⁻¹ * ↑(μ d) else 0
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if l ∣ d then 1 else 0) * (S⁻¹ * ↑(μ d) * if d ∣ x ∧ ↑x ^ 2 ≤ y then g x else 0) =
      if l ∣ d ∧ d ∣ x ∧ ↑x ^ 2 ≤ y then g x * S⁻¹ * ↑(μ d) else 0
Tactic:
intro k _
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝¹ : d ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ (if l ∣ d then 1 else 0) * (S⁻¹ * ↑(μ d) * if d ∣ k ∧ ↑k ^ 2 ≤ y then g k else 0) =
    if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝¹ : d ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ (if l ∣ d then 1 else 0) * (S⁻¹ * ↑(μ d) * if d ∣ k ∧ ↑k ^ 2 ≤ y then g k else 0) =
    if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
Tactic:
rw [mul_ite_zero, ite_zero_mul_ite_zero]
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝¹ : d ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ (if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then 1 * (S⁻¹ * ↑(μ d) * g k) else 0) =
    if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝¹ : d ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ (if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then 1 * (S⁻¹ * ↑(μ d) * g k) else 0) =
    if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
Tactic:
apply if_ctx_congr Iff.rfl _ (fun _ => rfl)
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝¹ : d ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y → 1 * (S⁻¹ * ↑(μ d) * g k) = g k * S⁻¹ * ↑(μ d)
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝¹ : d ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y → 1 * (S⁻¹ * ↑(μ d) * g k) = g k * S⁻¹ * ↑(μ d)
Tactic:
intro _
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝² : d ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
a✝ : l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y
⊢ 1 * (S⁻¹ * ↑(μ d) * g k) = g k * S⁻¹ * ↑(μ d)
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝² : d ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
a✝ : l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y
⊢ 1 * (S⁻¹ * ↑(μ d) * g k) = g k * S⁻¹ * ↑(μ d)
Tactic:
ring
Proof state after:
no goals
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (∑ d ∈ P.divisors, ∑ k ∈ P.divisors, if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0) =
    ∑ k ∈ P.divisors, if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0
Tactic:
rw [sum_comm]
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (∑ y ∈ P.divisors, ∑ x ∈ P.divisors, if l ∣ x ∧ x ∣ y ∧ ↑y ^ 2 ≤ y then g y * S⁻¹ * ↑(μ x) else 0) =
    ∑ k ∈ P.divisors, if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0
Theorem: SelbergSieve.selbergWeights_diagonalisation
Proof state before:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (∑ y ∈ P.divisors, ∑ x ∈ P.divisors, if l ∣ x ∧ x ∣ y ∧ ↑y ^ 2 ≤ y then g y * S⁻¹ * ↑(μ x) else 0) =
    ∑ k ∈ P.divisors, if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0
Tactic:
apply sum_congr rfl
Proof state after:
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (∑ x_1 ∈ P.divisors, if l ∣ x_1 ∧ x_1 ∣ x ∧ ↑x ^ 2 ≤ y then g x * S⁻¹ * ↑(μ x_1) else 0) =
      if ↑x ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ x then ↑(μ d) else 0) * g x * S⁻¹ else 0