internlm/Lean-Github huggingface dataset:
Theorem: Sieve.prime_dvd_primorial_iff
Proof state before:
case mp.intro
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
q : ℕ
hq : (q < n + 1 ∧ q.Prime) ∧ p ∣ q
⊢ p ≤ n
Tactic:
rw [prime_dvd_prime_iff_eq (Nat.Prime.prime hp) (Nat.Prime.prime hq.1.2)] at hq
Proof state after:
case mp.intro
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
q : ℕ
hq : (q < n + 1 ∧ q.Prime) ∧ p = q
⊢ p ≤ n
Theorem: Sieve.prime_dvd_primorial_iff
Proof state before:
case mp.intro
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
q : ℕ
hq : (q < n + 1 ∧ q.Prime) ∧ p = q
⊢ p ≤ n
Tactic:
rw [hq.2]
Proof state after:
case mp.intro
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
q : ℕ
hq : (q < n + 1 ∧ q.Prime) ∧ p = q
⊢ q ≤ n
Theorem: Sieve.prime_dvd_primorial_iff
Proof state before:
case mp.intro
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
q : ℕ
hq : (q < n + 1 ∧ q.Prime) ∧ p = q
⊢ q ≤ n
Tactic:
exact Nat.lt_succ.mp hq.1.1
Proof state after:
no goals
Theorem: Sieve.prime_dvd_primorial_iff
Proof state before:
case mpr
n p : ℕ
hp : p.Prime
⊢ p ≤ n → p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
Tactic:
intro h
Proof state after:
case mpr
n p : ℕ
hp : p.Prime
h : p ≤ n
⊢ p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
Theorem: Sieve.prime_dvd_primorial_iff
Proof state before:
case mpr
n p : ℕ
hp : p.Prime
h : p ≤ n
⊢ p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
Tactic:
apply Finset.dvd_prod_of_mem
Proof state after:
case mpr.ha
n p : ℕ
hp : p.Prime
h : p ≤ n
⊢ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1))
Theorem: Sieve.prime_dvd_primorial_iff
Proof state before:
case mpr.ha
n p : ℕ
hp : p.Prime
h : p ≤ n
⊢ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1))
Tactic:
rw [Finset.mem_filter, Finset.mem_range]
Proof state after:
case mpr.ha
n p : ℕ
hp : p.Prime
h : p ≤ n
⊢ p < n + 1 ∧ p.Prime
Theorem: Sieve.prime_dvd_primorial_iff
Proof state before:
case mpr.ha
n p : ℕ
hp : p.Prime
h : p ≤ n
⊢ p < n + 1 ∧ p.Prime
Tactic:
exact ⟨Nat.lt_succ.mpr h, hp⟩
Proof state after:
no goals
Theorem: Sieve.siftedSum_eq
Proof 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]
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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]
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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]
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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]
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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
Proof state after:
no goals
Theorem: Sieve.siftedSum_eq
Proof 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
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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 *
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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
Proof state after:
no goals
Theorem: Sieve.siftedSum_eq
Proof 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
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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]
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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
Proof 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⌋₊
Theorem: Sieve.siftedSum_eq
Proof 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]
Proof 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⌋₊
Theorem: Sieve.siftedSum_eq
Proof 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
Proof state after:
no goals
Theorem: Sieve.siftedSum_eq
Proof 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
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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 *
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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 ?_
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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]
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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)
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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
Proof state after:
no goals
Theorem: Sieve.siftedSum_eq
Proof 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
Proof state after:
no goals
Theorem: Sieve.siftedSum_eq
Proof 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
Proof 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
Theorem: Sieve.siftedSum_eq
Proof 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]
Proof state after:
no goals
Theorem: Sieve.CompletelyMultiplicative.zeta
Proof state before:
⊢ CompletelyMultiplicative ↑ζ
Tactic:
unfold CompletelyMultiplicative
Proof state after:
⊢ ↑ζ 1 = 1 ∧ ∀ (a b : ℕ), ↑ζ (a * b) = ↑ζ a * ↑ζ b
Theorem: Sieve.CompletelyMultiplicative.zeta
Proof state before:
⊢ ↑ζ 1 = 1 ∧ ∀ (a b : ℕ), ↑ζ (a * b) = ↑ζ a * ↑ζ b
Tactic:
simp_rw [ArithmeticFunction.natCoe_apply, ArithmeticFunction.zeta_apply, ite_false, Nat.cast_one,
  mul_eq_zero, Nat.cast_ite, CharP.cast_eq_zero, mul_ite, mul_zero, true_and]
Proof state after:
⊢ ∀ (a b : ℕ), (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1
Theorem: Sieve.CompletelyMultiplicative.zeta
Proof state before:
⊢ ∀ (a b : ℕ), (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1
Tactic:
intro a b
Proof state after:
a b : ℕ
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1
Theorem: Sieve.CompletelyMultiplicative.zeta
Proof state before:
a b : ℕ
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1
Tactic:
by_cases ha : a = 0
Proof state after:
case pos
a b : ℕ
ha : a = 0
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1

case neg
a b : ℕ
ha : ¬a = 0
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1
Theorem: Sieve.CompletelyMultiplicative.zeta
Proof state before:
case neg
a b : ℕ
ha : ¬a = 0
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1
Tactic:
by_cases hb : b = 0
Proof state after:
case pos
a b : ℕ
ha : ¬a = 0
hb : b = 0
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1

case neg
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1
Theorem: Sieve.CompletelyMultiplicative.zeta
Proof state before:
case neg
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1
Tactic:
rw [if_neg, if_neg hb, if_neg ha]
Proof state after:
case neg
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ ↑1 = ↑1 * ↑1

case neg.hnc
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ ¬(a = 0 ∨ b = 0)
Theorem: Sieve.CompletelyMultiplicative.zeta
Proof state before:
case neg
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ ↑1 = ↑1 * ↑1

case neg.hnc
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ ¬(a = 0 ∨ b = 0)
Tactic:
ring
Proof state after:
case neg.hnc
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ ¬(a = 0 ∨ b = 0)