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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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]
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

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
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

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
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

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
State after:
no goals

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
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

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 ⊢
State after:
no goals

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
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

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
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

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
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

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
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

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]
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

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
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

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
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

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
State after:
no goals

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 ⊢)
State after:
no goals

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
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

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 ⊢
State after:
no goals

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
State after:
no goals