internlm/Lean-Github huggingface dataset:
Theorem: SelbergSieve._helper
Proof state before:
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
⊢ k * m ∣ P ∧ k = d.gcd (k * m) ∧ (↑k * ↑m) ^ 2 ≤ y ↔ (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
Tactic:
constructor
Proof state after:
case mp
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
⊢ k * m ∣ P ∧ k = d.gcd (k * m) ∧ (↑k * ↑m) ^ 2 ≤ y → (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d

case mpr
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
⊢ (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d → k * m ∣ P ∧ k = d.gcd (k * m) ∧ (↑k * ↑m) ^ 2 ≤ y
Theorem: SelbergSieve._helper
Proof state before:
case mp
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
⊢ k * m ∣ P ∧ k = d.gcd (k * m) ∧ (↑k * ↑m) ^ 2 ≤ y → (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
Tactic:
intro h
Proof state after:
case mp
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : k * m ∣ P ∧ k = d.gcd (k * m) ∧ (↑k * ↑m) ^ 2 ≤ y
⊢ (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
Theorem: SelbergSieve._helper
Proof state before:
case mp
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : k * m ∣ P ∧ k = d.gcd (k * m) ∧ (↑k * ↑m) ^ 2 ≤ y
⊢ (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
Tactic:
constructor
Proof state after:
case mp.left
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : k * m ∣ P ∧ k = d.gcd (k * m) ∧ (↑k * ↑m) ^ 2 ≤ y
⊢ (↑k * ↑m) ^ 2 ≤ y

case mp.right
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : k * m ∣ P ∧ k = d.gcd (k * m) ∧ (↑k * ↑m) ^ 2 ≤ y
⊢ m.Coprime d
Theorem: SelbergSieve._helper
Proof state before:
case mp.left
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : k * m ∣ P ∧ k = d.gcd (k * m) ∧ (↑k * ↑m) ^ 2 ≤ y
⊢ (↑k * ↑m) ^ 2 ≤ y
Tactic:
exact h.2.2
Proof state after:
no goals
Theorem: SelbergSieve._helper
Proof state before:
case mp.right
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : k * m ∣ P ∧ k = d.gcd (k * m) ∧ (↑k * ↑m) ^ 2 ≤ y
⊢ m.Coprime d
Tactic:
cases' hkd with r hr
Proof state after:
case mp.right.intro
s : SelbergSieve
k m d : ℕ
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : k * m ∣ P ∧ k = d.gcd (k * m) ∧ (↑k * ↑m) ^ 2 ≤ y
r : ℕ
hr : d = k * r
⊢ m.Coprime d
Theorem: SelbergSieve._helper
Proof state before:
case mp.right.intro
s : SelbergSieve
k m d : ℕ
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : k * m ∣ P ∧ k = d.gcd (k * m) ∧ (↑k * ↑m) ^ 2 ≤ y
r : ℕ
hr : d = k * r
⊢ m.Coprime d
Tactic:
rw [hr, Nat.gcd_mul_left, eq_comm, mul_eq_left₀ (by rintro rfl; simp at hk ⊢)] at h
Proof state after:
case mp.right.intro
s : SelbergSieve
k m d : ℕ
hk : k ∈ P.divisors
hm : m ∈ P.divisors
r : ℕ
h : k * m ∣ P ∧ r.gcd m = 1 ∧ (↑k * ↑m) ^ 2 ≤ y
hr : d = k * r
⊢ m.Coprime d
Theorem: SelbergSieve._helper
Proof state before:
case mp.right.intro
s : SelbergSieve
k m d : ℕ
hk : k ∈ P.divisors
hm : m ∈ P.divisors
r : ℕ
h : k * m ∣ P ∧ r.gcd m = 1 ∧ (↑k * ↑m) ^ 2 ≤ y
hr : d = k * r
⊢ m.Coprime d
Tactic:
rw [hr, coprime_comm]
Proof state after:
case mp.right.intro
s : SelbergSieve
k m d : ℕ
hk : k ∈ P.divisors
hm : m ∈ P.divisors
r : ℕ
h : k * m ∣ P ∧ r.gcd m = 1 ∧ (↑k * ↑m) ^ 2 ≤ y
hr : d = k * r
⊢ (k * r).Coprime m
Theorem: SelbergSieve._helper
Proof state before:
case mp.right.intro
s : SelbergSieve
k m d : ℕ
hk : k ∈ P.divisors
hm : m ∈ P.divisors
r : ℕ
h : k * m ∣ P ∧ r.gcd m = 1 ∧ (↑k * ↑m) ^ 2 ≤ y
hr : d = k * r
⊢ (k * r).Coprime m
Tactic:
apply Coprime.mul
Proof state after:
case mp.right.intro.H1
s : SelbergSieve
k m d : ℕ
hk : k ∈ P.divisors
hm : m ∈ P.divisors
r : ℕ
h : k * m ∣ P ∧ r.gcd m = 1 ∧ (↑k * ↑m) ^ 2 ≤ y
hr : d = k * r
⊢ k.Coprime m

case mp.right.intro.H2
s : SelbergSieve
k m d : ℕ
hk : k ∈ P.divisors
hm : m ∈ P.divisors
r : ℕ
h : k * m ∣ P ∧ r.gcd m = 1 ∧ (↑k * ↑m) ^ 2 ≤ y
hr : d = k * r
⊢ r.Coprime m
Theorem: SelbergSieve._helper
Proof state before:
case mp.right.intro.H1
s : SelbergSieve
k m d : ℕ
hk : k ∈ P.divisors
hm : m ∈ P.divisors
r : ℕ
h : k * m ∣ P ∧ r.gcd m = 1 ∧ (↑k * ↑m) ^ 2 ≤ y
hr : d = k * r
⊢ k.Coprime m

case mp.right.intro.H2
s : SelbergSieve
k m d : ℕ
hk : k ∈ P.divisors
hm : m ∈ P.divisors
r : ℕ
h : k * m ∣ P ∧ r.gcd m = 1 ∧ (↑k * ↑m) ^ 2 ≤ y
hr : d = k * r
⊢ r.Coprime m
Tactic:
apply coprime_of_squarefree_mul $ Squarefree.squarefree_of_dvd h.1 s.prodPrimes_squarefree
Proof state after:
case mp.right.intro.H2
s : SelbergSieve
k m d : ℕ
hk : k ∈ P.divisors
hm : m ∈ P.divisors
r : ℕ
h : k * m ∣ P ∧ r.gcd m = 1 ∧ (↑k * ↑m) ^ 2 ≤ y
hr : d = k * r
⊢ r.Coprime m
Theorem: SelbergSieve._helper
Proof state before:
case mp.right.intro.H2
s : SelbergSieve
k m d : ℕ
hk : k ∈ P.divisors
hm : m ∈ P.divisors
r : ℕ
h : k * m ∣ P ∧ r.gcd m = 1 ∧ (↑k * ↑m) ^ 2 ≤ y
hr : d = k * r
⊢ r.Coprime m
Tactic:
exact h.2.1
Proof state after:
no goals
Theorem: SelbergSieve._helper
Proof state before:
s : SelbergSieve
k m d : ℕ
hk : k ∈ P.divisors
hm : m ∈ P.divisors
r : ℕ
h : k * m ∣ P ∧ k * r.gcd m = k ∧ (↑k * ↑m) ^ 2 ≤ y
hr : d = k * r
⊢ k ≠ 0
Tactic:
rintro rfl
Proof state after:
s : SelbergSieve
m d : ℕ
hm : m ∈ P.divisors
r : ℕ
hk : 0 ∈ P.divisors
h : 0 * m ∣ P ∧ 0 * r.gcd m = 0 ∧ (↑0 * ↑m) ^ 2 ≤ y
hr : d = 0 * r
⊢ False
Theorem: SelbergSieve._helper
Proof state before:
s : SelbergSieve
m d : ℕ
hm : m ∈ P.divisors
r : ℕ
hk : 0 ∈ P.divisors
h : 0 * m ∣ P ∧ 0 * r.gcd m = 0 ∧ (↑0 * ↑m) ^ 2 ≤ y
hr : d = 0 * r
⊢ False
Tactic:
simp at hk ⊢
Proof state after:
no goals
Theorem: SelbergSieve._helper
Proof state before:
case mpr
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
⊢ (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d → k * m ∣ P ∧ k = d.gcd (k * m) ∧ (↑k * ↑m) ^ 2 ≤ y
Tactic:
intro h
Proof state after:
case mpr
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ k * m ∣ P ∧ k = d.gcd (k * m) ∧ (↑k * ↑m) ^ 2 ≤ y
Theorem: SelbergSieve._helper
Proof state before:
case mpr
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ k * m ∣ P ∧ k = d.gcd (k * m) ∧ (↑k * ↑m) ^ 2 ≤ y
Tactic:
constructor
Proof state after:
case mpr.left
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ k * m ∣ P

case mpr.right
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ k = d.gcd (k * m) ∧ (↑k * ↑m) ^ 2 ≤ y
Theorem: SelbergSieve._helper
Proof state before:
case mpr.right
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ k = d.gcd (k * m) ∧ (↑k * ↑m) ^ 2 ≤ y
Tactic:
constructor
Proof state after:
case mpr.right.left
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ k = d.gcd (k * m)

case mpr.right.right
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ (↑k * ↑m) ^ 2 ≤ y
Theorem: SelbergSieve._helper
Proof state before:
case mpr.left
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ k * m ∣ P
Tactic:
apply Nat.Coprime.mul_dvd_of_dvd_of_dvd
Proof state after:
case mpr.left.hmn
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ k.Coprime m

case mpr.left.hm
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ k ∣ P

case mpr.left.hn
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ m ∣ P
Theorem: SelbergSieve._helper
Proof state before:
case mpr.left.hmn
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ k.Coprime m

case mpr.left.hm
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ k ∣ P

case mpr.left.hn
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ m ∣ P
Tactic:
rw [coprime_comm]
Proof state after:
case mpr.left.hmn
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ m.Coprime k

case mpr.left.hm
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ k ∣ P

case mpr.left.hn
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ m ∣ P
Theorem: SelbergSieve._helper
Proof state before:
case mpr.left.hmn
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ m.Coprime k

case mpr.left.hm
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ k ∣ P

case mpr.left.hn
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ m ∣ P
Tactic:
exact Coprime.coprime_dvd_right hkd h.2
Proof state after:
case mpr.left.hm
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ k ∣ P

case mpr.left.hn
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ m ∣ P
Theorem: SelbergSieve._helper
Proof state before:
case mpr.left.hm
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ k ∣ P

case mpr.left.hn
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ m ∣ P
Tactic:
exact dvd_of_mem_divisors hk
Proof state after:
case mpr.left.hn
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ m ∣ P
Theorem: SelbergSieve._helper
Proof state before:
case mpr.left.hn
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ m ∣ P
Tactic:
exact dvd_of_mem_divisors hm
Proof state after:
no goals
Theorem: SelbergSieve._helper
Proof state before:
case mpr.right.left
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ k = d.gcd (k * m)
Tactic:
exact eq_gcd_mul_of_dvd_of_coprime hkd h.2 (by rintro rfl; simp at hk ⊢)
Proof state after:
no goals
Theorem: SelbergSieve._helper
Proof state before:
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ k ≠ 0
Tactic:
rintro rfl
Proof state after:
s : SelbergSieve
m d : ℕ
hm : m ∈ P.divisors
hkd : 0 ∣ d
hk : 0 ∈ P.divisors
h : (↑0 * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ False
Theorem: SelbergSieve._helper
Proof state before:
s : SelbergSieve
m d : ℕ
hm : m ∈ P.divisors
hkd : 0 ∣ d
hk : 0 ∈ P.divisors
h : (↑0 * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ False
Tactic:
simp at hk ⊢
Proof state after:
no goals
Theorem: SelbergSieve._helper
Proof state before:
case mpr.right.right
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ (↑k * ↑m) ^ 2 ≤ y
Tactic:
exact h.1
Proof state after:
no goals
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ S = ∑ k ∈ P.divisors, ∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0
Tactic:
dsimp only [selbergBoundingSum]
Proof state after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0) =
    ∑ k ∈ P.divisors, ∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0) =
    ∑ k ∈ P.divisors, ∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0
Tactic:
rw [sum_comm, sum_congr rfl]
Proof state after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ ∀ x ∈ P.divisors, (if ↑x ^ 2 ≤ y then g x else 0) = ∑ x_1 ∈ P.divisors, if x_1 = d.gcd x ∧ ↑x ^ 2 ≤ y then g x else 0
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ ∀ x ∈ P.divisors, (if ↑x ^ 2 ≤ y then g x else 0) = ∑ x_1 ∈ P.divisors, if x_1 = d.gcd x ∧ ↑x ^ 2 ≤ y then g x else 0
Tactic:
intro l _
Proof state after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ (if ↑l ^ 2 ≤ y then g l else 0) = ∑ x ∈ P.divisors, if x = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ (if ↑l ^ 2 ≤ y then g l else 0) = ∑ x ∈ P.divisors, if x = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0
Tactic:
simp_rw [ite_and]
Proof state after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ (if ↑l ^ 2 ≤ y then g l else 0) = ∑ x ∈ P.divisors, if x = d.gcd l then if ↑l ^ 2 ≤ y then g l else 0 else 0
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ (if ↑l ^ 2 ≤ y then g l else 0) = ∑ x ∈ P.divisors, if x = d.gcd l then if ↑l ^ 2 ≤ y then g l else 0 else 0
Tactic:
rw [←Aux.sum_intro]
Proof state after:
case hd
s : SelbergSieve
d : ℕ
hdP : d ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ d.gcd l ∈ P.divisors
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
case hd
s : SelbergSieve
d : ℕ
hdP : d ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ d.gcd l ∈ P.divisors
Tactic:
rw [mem_divisors]
Proof state after:
case hd
s : SelbergSieve
d : ℕ
hdP : d ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ d.gcd l ∣ P ∧ P ≠ 0
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
case hd
s : SelbergSieve
d : ℕ
hdP : d ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ d.gcd l ∣ P ∧ P ≠ 0
Tactic:
exact ⟨(Nat.gcd_dvd_left d l).trans (hdP), s.prodPrimes_ne_zero⟩
Proof state after:
no goals
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (∑ k ∈ P.divisors, ∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
    ∑ k ∈ P.divisors, if k ∣ d then g k * ∑ m ∈ P.divisors, if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0
Tactic:
apply sum_congr rfl
Proof state after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ ∀ x ∈ P.divisors,
    (∑ l ∈ P.divisors, if x = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
      if x ∣ d then g x * ∑ m ∈ P.divisors, if (↑x * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ ∀ x ∈ P.divisors,
    (∑ l ∈ P.divisors, if x = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
      if x ∣ d then g x * ∑ m ∈ P.divisors, if (↑x * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0
Tactic:
intro k hk
Proof state after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
    if k ∣ d then g k * ∑ m ∈ P.divisors, if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
    if k ∣ d then g k * ∑ m ∈ P.divisors, if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0
Tactic:
rw [mul_sum]
Proof state after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
    if k ∣ d then ∑ i ∈ P.divisors, g k * if (↑k * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0 else 0
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
    if k ∣ d then ∑ i ∈ P.divisors, g k * if (↑k * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0 else 0
Tactic:
split_ifs with hkd
Proof state after:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
    ∑ i ∈ P.divisors, g k * if (↑k * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0

case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
    ∑ i ∈ P.divisors, g k * if (↑k * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0

case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
swap
Proof state after:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
    ∑ i ∈ P.divisors, g k * if (↑k * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
    ∑ i ∈ P.divisors, g k * if (↑k * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0
Tactic:
rw [sum_mul_subst k P, sum_congr rfl]
Proof state after:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ x ∈ P.divisors,
    (if k * x ∣ P then if k = d.gcd (k * x) ∧ ↑(k * x) ^ 2 ≤ y then g (k * x) else 0 else 0) =
      g k * if (↑k * ↑x) ^ 2 ≤ y ∧ x.Coprime d then g x else 0

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ (l : ℕ), l ∣ P → ¬k ∣ l → (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ x ∈ P.divisors,
    (if k * x ∣ P then if k = d.gcd (k * x) ∧ ↑(k * x) ^ 2 ≤ y then g (k * x) else 0 else 0) =
      g k * if (↑k * ↑x) ^ 2 ≤ y ∧ x.Coprime d then g x else 0

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ (l : ℕ), l ∣ P → ¬k ∣ l → (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
intro m hm
Proof state after:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ (if k * m ∣ P then if k = d.gcd (k * m) ∧ ↑(k * m) ^ 2 ≤ y then g (k * m) else 0 else 0) =
    g k * if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ (l : ℕ), l ∣ P → ¬k ∣ l → (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ (if k * m ∣ P then if k = d.gcd (k * m) ∧ ↑(k * m) ^ 2 ≤ y then g (k * m) else 0 else 0) =
    g k * if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ (l : ℕ), l ∣ P → ¬k ∣ l → (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
rw [mul_ite_zero, ← ite_and]
Proof state after:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ (if k * m ∣ P ∧ k = d.gcd (k * m) ∧ ↑(k * m) ^ 2 ≤ y then g (k * m) else 0) =
    if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g k * g m else 0

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ (l : ℕ), l ∣ P → ¬k ∣ l → (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ (if k * m ∣ P ∧ k = d.gcd (k * m) ∧ ↑(k * m) ^ 2 ≤ y then g (k * m) else 0) =
    if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g k * g m else 0

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ (l : ℕ), l ∣ P → ¬k ∣ l → (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
apply if_ctx_congr _ _ fun _ => rfl
Proof state after:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ k * m ∣ P ∧ k = d.gcd (k * m) ∧ ↑(k * m) ^ 2 ≤ y ↔ (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d

s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d → g (k * m) = g k * g m

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ (l : ℕ), l ∣ P → ¬k ∣ l → (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
rw [sum_eq_zero]
Proof state after:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
⊢ ∀ x ∈ P.divisors, (if k = d.gcd x ∧ ↑x ^ 2 ≤ y then g x else 0) = 0
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
⊢ ∀ x ∈ P.divisors, (if k = d.gcd x ∧ ↑x ^ 2 ≤ y then g x else 0) = 0
Tactic:
intro l _
Proof state after:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
l : ℕ
a✝ : l ∈ P.divisors
⊢ (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
l : ℕ
a✝ : l ∈ P.divisors
⊢ (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
Tactic:
rw [if_neg]
Proof state after:
case neg.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
l : ℕ
a✝ : l ∈ P.divisors
⊢ ¬(k = d.gcd l ∧ ↑l ^ 2 ≤ y)
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
case neg.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
l : ℕ
a✝ : l ∈ P.divisors
⊢ ¬(k = d.gcd l ∧ ↑l ^ 2 ≤ y)
Tactic:
push_neg
Proof state after:
case neg.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
l : ℕ
a✝ : l ∈ P.divisors
⊢ k = d.gcd l → y < ↑l ^ 2
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
case neg.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
l : ℕ
a✝ : l ∈ P.divisors
⊢ k = d.gcd l → y < ↑l ^ 2
Tactic:
intro h
Proof state after:
case neg.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
l : ℕ
a✝ : l ∈ P.divisors
h : k = d.gcd l
⊢ y < ↑l ^ 2
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
case neg.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
l : ℕ
a✝ : l ∈ P.divisors
h : k = d.gcd l
⊢ y < ↑l ^ 2
Tactic:
exfalso
Proof state after:
case neg.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
l : ℕ
a✝ : l ∈ P.divisors
h : k = d.gcd l
⊢ False
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
case neg.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : ¬k ∣ d
l : ℕ
a✝ : l ∈ P.divisors
h : k = d.gcd l
⊢ False
Tactic:
rw [h] at hkd
Proof state after:
case neg.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
l : ℕ
hkd : ¬d.gcd l ∣ d
a✝ : l ∈ P.divisors
h : k = d.gcd l
⊢ False
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
case neg.hnc
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
l : ℕ
hkd : ¬d.gcd l ∣ d
a✝ : l ∈ P.divisors
h : k = d.gcd l
⊢ False
Tactic:
exact hkd $ Nat.gcd_dvd_left d l
Proof state after:
no goals
Theorem: SelbergSieve.selbergBoundingSum_ge
Proof state before:
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ k * m ∣ P ∧ k = d.gcd (k * m) ∧ ↑(k * m) ^ 2 ≤ y ↔ (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
Tactic:
exact_mod_cast s._helper hkd hk hm
Proof state after:
no goals