Theorem: Sieve.siftedSum_eq (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean)

State before:
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
⊢ s.siftedSum = ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support).card
Tactic:
dsimp only [Sieve.siftedSum]
State after:
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
⊢ (∑ d ∈ s.support, if s.prodPrimes.Coprime d then s.weights d else 0) =
    ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support).card

State before:
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
⊢ (∑ d ∈ s.support, if s.prodPrimes.Coprime d then s.weights d else 0) =
    ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support).card
Tactic:
rw [Finset.card_eq_sum_ones, ←Finset.sum_filter, Nat.cast_sum]
State after:
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
⊢ ∑ a ∈ Finset.filter (fun d => s.prodPrimes.Coprime d) s.support, s.weights a =
    ∑ x ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support, ↑1

State before:
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
⊢ ∑ a ∈ Finset.filter (fun d => s.prodPrimes.Coprime d) s.support, s.weights a =
    ∑ x ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support, ↑1
Tactic:
apply Finset.sum_congr
State after:
case h
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
⊢ Finset.filter (fun d => s.prodPrimes.Coprime d) s.support =
    Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support

case a
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
⊢ ∀ x ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support, s.weights x = ↑1

State before:
case h
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
⊢ Finset.filter (fun d => s.prodPrimes.Coprime d) s.support =
    Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support

case a
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
⊢ ∀ x ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support, s.weights x = ↑1
Tactic:
rw [hP]
State after:
case h
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
⊢ Finset.filter (fun d => (primorial ⌊z⌋₊).Coprime d) s.support =
    Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support

case a
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
⊢ ∀ x ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support, s.weights x = ↑1

State before:
case h
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
⊢ Finset.filter (fun d => (primorial ⌊z⌋₊).Coprime d) s.support =
    Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support

case a
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
⊢ ∀ x ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support, s.weights x = ↑1
Tactic:
ext d
State after:
case h.a
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
⊢ d ∈ Finset.filter (fun d => (primorial ⌊z⌋₊).Coprime d) s.support ↔
    d ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support

case a
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
⊢ ∀ x ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support, s.weights x = ↑1

State before:
case h.a
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
⊢ d ∈ Finset.filter (fun d => (primorial ⌊z⌋₊).Coprime d) s.support ↔
    d ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support

case a
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
⊢ ∀ x ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support, s.weights x = ↑1
Tactic:
constructor
State after:
case h.a.mp
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
⊢ d ∈ Finset.filter (fun d => (primorial ⌊z⌋₊).Coprime d) s.support →
    d ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support

case h.a.mpr
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
⊢ d ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support →
    d ∈ Finset.filter (fun d => (primorial ⌊z⌋₊).Coprime d) s.support

case a
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
⊢ ∀ x ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support, s.weights x = ↑1

State before:
case a
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
⊢ ∀ x ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support, s.weights x = ↑1
Tactic:
simp_rw [Nat.cast_one]
State after:
case a
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
⊢ ∀ x ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support, s.weights x = 1

State before:
case a
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
⊢ ∀ x ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support, s.weights x = 1
Tactic:
intro x hx
State after:
case a
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
x : ℕ
hx : x ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support
⊢ s.weights x = 1

State before:
case a
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
x : ℕ
hx : x ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support
⊢ s.weights x = 1
Tactic:
simp only [Finset.filter_congr_decidable, Finset.mem_filter] at hx
State after:
case a
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
x : ℕ
hx : x ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ x
⊢ s.weights x = 1

State before:
case a
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
x : ℕ
hx : x ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ x
⊢ s.weights x = 1
Tactic:
apply hw x hx.1
State after:
no goals

State before:
case h.a.mp
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
⊢ d ∈ Finset.filter (fun d => (primorial ⌊z⌋₊).Coprime d) s.support →
    d ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support
Tactic:
intro hd
State after:
case h.a.mp
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
hd : d ∈ Finset.filter (fun d => (primorial ⌊z⌋₊).Coprime d) s.support
⊢ d ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support

State before:
case h.a.mp
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
hd : d ∈ Finset.filter (fun d => (primorial ⌊z⌋₊).Coprime d) s.support
⊢ d ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support
Tactic:
rw [Finset.mem_filter] at *
State after:
case h.a.mp
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
hd : d ∈ s.support ∧ (primorial ⌊z⌋₊).Coprime d
⊢ d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d

State before:
case h.a.mp
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
hd : d ∈ s.support ∧ (primorial ⌊z⌋₊).Coprime d
⊢ d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
Tactic:
constructor
State after:
case h.a.mp.left
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
hd : d ∈ s.support ∧ (primorial ⌊z⌋₊).Coprime d
⊢ d ∈ s.support

case h.a.mp.right
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
hd : d ∈ s.support ∧ (primorial ⌊z⌋₊).Coprime d
⊢ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d

State before:
case h.a.mp.left
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
hd : d ∈ s.support ∧ (primorial ⌊z⌋₊).Coprime d
⊢ d ∈ s.support
Tactic:
exact hd.1
State after:
no goals

State before:
case h.a.mp.right
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
hd : d ∈ s.support ∧ (primorial ⌊z⌋₊).Coprime d
⊢ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
Tactic:
intro p hpp hpy
State after:
case h.a.mp.right
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
hd : d ∈ s.support ∧ (primorial ⌊z⌋₊).Coprime d
p : ℕ
hpp : p.Prime
hpy : ↑p ≤ z
⊢ ¬p ∣ d

State before:
case h.a.mp.right
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
hd : d ∈ s.support ∧ (primorial ⌊z⌋₊).Coprime d
p : ℕ
hpp : p.Prime
hpy : ↑p ≤ z
⊢ ¬p ∣ d
Tactic:
rw [←Nat.Prime.coprime_iff_not_dvd hpp]
State after:
case h.a.mp.right
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
hd : d ∈ s.support ∧ (primorial ⌊z⌋₊).Coprime d
p : ℕ
hpp : p.Prime
hpy : ↑p ≤ z
⊢ p.Coprime d

State before:
case h.a.mp.right
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
hd : d ∈ s.support ∧ (primorial ⌊z⌋₊).Coprime d
p : ℕ
hpp : p.Prime
hpy : ↑p ≤ z
⊢ p.Coprime d
Tactic:
apply Nat.Coprime.coprime_dvd_left _ hd.2
State after:
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
hd : d ∈ s.support ∧ (primorial ⌊z⌋₊).Coprime d
p : ℕ
hpp : p.Prime
hpy : ↑p ≤ z
⊢ p ∣ primorial ⌊z⌋₊

State before:
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
hd : d ∈ s.support ∧ (primorial ⌊z⌋₊).Coprime d
p : ℕ
hpp : p.Prime
hpy : ↑p ≤ z
⊢ p ∣ primorial ⌊z⌋₊
Tactic:
rw [prime_dvd_primorial_iff _ _ hpp]
State after:
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
hd : d ∈ s.support ∧ (primorial ⌊z⌋₊).Coprime d
p : ℕ
hpp : p.Prime
hpy : ↑p ≤ z
⊢ p ≤ ⌊z⌋₊

State before:
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
hd : d ∈ s.support ∧ (primorial ⌊z⌋₊).Coprime d
p : ℕ
hpp : p.Prime
hpy : ↑p ≤ z
⊢ p ≤ ⌊z⌋₊
Tactic:
apply Nat.le_floor hpy
State after:
no goals

State before:
case h.a.mpr
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
⊢ d ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support →
    d ∈ Finset.filter (fun d => (primorial ⌊z⌋₊).Coprime d) s.support
Tactic:
intro h
State after:
case h.a.mpr
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support
⊢ d ∈ Finset.filter (fun d => (primorial ⌊z⌋₊).Coprime d) s.support

State before:
case h.a.mpr
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support
⊢ d ∈ Finset.filter (fun d => (primorial ⌊z⌋₊).Coprime d) s.support
Tactic:
rw [Finset.mem_filter] at *
State after:
case h.a.mpr
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
⊢ d ∈ s.support ∧ (primorial ⌊z⌋₊).Coprime d

State before:
case h.a.mpr
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
⊢ d ∈ s.support ∧ (primorial ⌊z⌋₊).Coprime d
Tactic:
constructor
State after:
case h.a.mpr.left
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
⊢ d ∈ s.support

case h.a.mpr.right
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
⊢ (primorial ⌊z⌋₊).Coprime d

State before:
case h.a.mpr.right
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
⊢ (primorial ⌊z⌋₊).Coprime d
Tactic:
refine Nat.coprime_of_dvd ?_
State after:
case h.a.mpr.right
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
⊢ ∀ (k : ℕ), k.Prime → k ∣ primorial ⌊z⌋₊ → ¬k ∣ d

State before:
case h.a.mpr.right
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
⊢ ∀ (k : ℕ), k.Prime → k ∣ primorial ⌊z⌋₊ → ¬k ∣ d
Tactic:
intro p hp
State after:
case h.a.mpr.right
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
p : ℕ
hp : p.Prime
⊢ p ∣ primorial ⌊z⌋₊ → ¬p ∣ d

State before:
case h.a.mpr.right
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
p : ℕ
hp : p.Prime
⊢ p ∣ primorial ⌊z⌋₊ → ¬p ∣ d
Tactic:
erw [prime_dvd_primorial_iff _ _ hp]
State after:
case h.a.mpr.right
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
p : ℕ
hp : p.Prime
⊢ p ≤ ⌊z⌋₊ → ¬p ∣ d

State before:
case h.a.mpr.right
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
p : ℕ
hp : p.Prime
⊢ p ≤ ⌊z⌋₊ → ¬p ∣ d
Tactic:
intro hpy
State after:
case h.a.mpr.right
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
p : ℕ
hp : p.Prime
hpy : p ≤ ⌊z⌋₊
⊢ ¬p ∣ d

State before:
case h.a.mpr.right
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
p : ℕ
hp : p.Prime
hpy : p ≤ ⌊z⌋₊
⊢ ¬p ∣ d
Tactic:
apply h.2 p hp
State after:
case h.a.mpr.right
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
p : ℕ
hp : p.Prime
hpy : p ≤ ⌊z⌋₊
⊢ ↑p ≤ z

State before:
case h.a.mpr.right
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
p : ℕ
hp : p.Prime
hpy : p ≤ ⌊z⌋₊
⊢ ↑p ≤ z
Tactic:
trans ↑(Nat.floor z)
State after:
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
p : ℕ
hp : p.Prime
hpy : p ≤ ⌊z⌋₊
⊢ ↑p ≤ ↑⌊z⌋₊

s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
p : ℕ
hp : p.Prime
hpy : p ≤ ⌊z⌋₊
⊢ ↑⌊z⌋₊ ≤ z

State before:
case h.a.mpr.left
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
⊢ d ∈ s.support
Tactic:
exact h.1
State after:
no goals

State before:
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
p : ℕ
hp : p.Prime
hpy : p ≤ ⌊z⌋₊
⊢ ↑p ≤ ↑⌊z⌋₊
Tactic:
norm_cast
State after:
no goals

State before:
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
p : ℕ
hp : p.Prime
hpy : p ≤ ⌊z⌋₊
⊢ ↑⌊z⌋₊ ≤ z
Tactic:
apply Nat.floor_le
State after:
case ha
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
p : ℕ
hp : p.Prime
hpy : p ≤ ⌊z⌋₊
⊢ 0 ≤ z

State before:
case ha
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
p : ℕ
hp : p.Prime
hpy : p ≤ ⌊z⌋₊
⊢ 0 ≤ z
Tactic:
linarith only [hz]
State after:
no goals