internlm/Lean-Github huggingface dataset:
Theorem: BrunTitchmarsh.primesBetween_subset
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ Finset.filter Nat.Prime (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ⊆
    Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ∪ Finset.Icc 1 ⌊z⌋₊
Tactic:
intro p
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
⊢ p ∈ Finset.filter Nat.Prime (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) →
    p ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ∪ Finset.Icc 1 ⌊z⌋₊
Theorem: BrunTitchmarsh.primesBetween_subset
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
⊢ p ∈ Finset.filter Nat.Prime (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) →
    p ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ∪ Finset.Icc 1 ⌊z⌋₊
Tactic:
simp only [Finset.mem_filter, Finset.mem_Icc, Nat.ceil_le, Finset.mem_union, and_imp]
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
⊢ x ≤ ↑p →
    p ≤ ⌊x + y⌋₊ → p.Prime → ((x ≤ ↑p ∧ p ≤ ⌊x + y⌋₊) ∧ ∀ (p_1 : ℕ), p_1.Prime → ↑p_1 ≤ z → ¬p_1 ∣ p) ∨ 1 ≤ p ∧ p ≤ ⌊z⌋₊
Theorem: BrunTitchmarsh.primesBetween_subset
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
⊢ x ≤ ↑p →
    p ≤ ⌊x + y⌋₊ → p.Prime → ((x ≤ ↑p ∧ p ≤ ⌊x + y⌋₊) ∧ ∀ (p_1 : ℕ), p_1.Prime → ↑p_1 ≤ z → ¬p_1 ∣ p) ∨ 1 ≤ p ∧ p ≤ ⌊z⌋₊
Tactic:
intro hx hxy hp
Proof state after:
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
⊢ ((x ≤ ↑p ∧ p ≤ ⌊x + y⌋₊) ∧ ∀ (p_1 : ℕ), p_1.Prime → ↑p_1 ≤ z → ¬p_1 ∣ p) ∨ 1 ≤ p ∧ p ≤ ⌊z⌋₊
Theorem: BrunTitchmarsh.primesBetween_subset
Proof state before:
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
⊢ ((x ≤ ↑p ∧ p ≤ ⌊x + y⌋₊) ∧ ∀ (p_1 : ℕ), p_1.Prime → ↑p_1 ≤ z → ¬p_1 ∣ p) ∨ 1 ≤ p ∧ p ≤ ⌊z⌋₊
Tactic:
by_cases hpz : p ≤ z
Proof state after:
case pos
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ↑p ≤ z
⊢ ((x ≤ ↑p ∧ p ≤ ⌊x + y⌋₊) ∧ ∀ (p_1 : ℕ), p_1.Prime → ↑p_1 ≤ z → ¬p_1 ∣ p) ∨ 1 ≤ p ∧ p ≤ ⌊z⌋₊

case neg
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ¬↑p ≤ z
⊢ ((x ≤ ↑p ∧ p ≤ ⌊x + y⌋₊) ∧ ∀ (p_1 : ℕ), p_1.Prime → ↑p_1 ≤ z → ¬p_1 ∣ p) ∨ 1 ≤ p ∧ p ≤ ⌊z⌋₊
Theorem: BrunTitchmarsh.primesBetween_subset
Proof state before:
case pos
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ↑p ≤ z
⊢ ((x ≤ ↑p ∧ p ≤ ⌊x + y⌋₊) ∧ ∀ (p_1 : ℕ), p_1.Prime → ↑p_1 ≤ z → ¬p_1 ∣ p) ∨ 1 ≤ p ∧ p ≤ ⌊z⌋₊
Tactic:
right
Proof state after:
case pos.h
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ↑p ≤ z
⊢ 1 ≤ p ∧ p ≤ ⌊z⌋₊
Theorem: BrunTitchmarsh.primesBetween_subset
Proof state before:
case pos.h
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ↑p ≤ z
⊢ 1 ≤ p ∧ p ≤ ⌊z⌋₊
Tactic:
rw[Nat.le_floor_iff (by linarith)]
Proof state after:
case pos.h
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ↑p ≤ z
⊢ 1 ≤ p ∧ ↑p ≤ z
Theorem: BrunTitchmarsh.primesBetween_subset
Proof state before:
case pos.h
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ↑p ≤ z
⊢ 1 ≤ p ∧ ↑p ≤ z
Tactic:
have := hp.ne_zero
Proof state after:
case pos.h
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ↑p ≤ z
this : p ≠ 0
⊢ 1 ≤ p ∧ ↑p ≤ z
Theorem: BrunTitchmarsh.primesBetween_subset
Proof state before:
case pos.h
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ↑p ≤ z
this : p ≠ 0
⊢ 1 ≤ p ∧ ↑p ≤ z
Tactic:
exact ⟨by omega, hpz⟩
Proof state after:
no goals
Theorem: BrunTitchmarsh.primesBetween_subset
Proof state before:
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ↑p ≤ z
⊢ 0 ≤ z
Tactic:
linarith
Proof state after:
no goals
Theorem: BrunTitchmarsh.primesBetween_subset
Proof state before:
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ↑p ≤ z
this : p ≠ 0
⊢ 1 ≤ p
Tactic:
omega
Proof state after:
no goals
Theorem: BrunTitchmarsh.primesBetween_subset
Proof state before:
case neg
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ¬↑p ≤ z
⊢ ((x ≤ ↑p ∧ p ≤ ⌊x + y⌋₊) ∧ ∀ (p_1 : ℕ), p_1.Prime → ↑p_1 ≤ z → ¬p_1 ∣ p) ∨ 1 ≤ p ∧ p ≤ ⌊z⌋₊
Tactic:
left
Proof state after:
case neg.h
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ¬↑p ≤ z
⊢ (x ≤ ↑p ∧ p ≤ ⌊x + y⌋₊) ∧ ∀ (p_1 : ℕ), p_1.Prime → ↑p_1 ≤ z → ¬p_1 ∣ p
Theorem: BrunTitchmarsh.primesBetween_subset
Proof state before:
case neg.h
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ¬↑p ≤ z
⊢ (x ≤ ↑p ∧ p ≤ ⌊x + y⌋₊) ∧ ∀ (p_1 : ℕ), p_1.Prime → ↑p_1 ≤ z → ¬p_1 ∣ p
Tactic:
refine ⟨⟨hx, hxy⟩, ?_⟩
Proof state after:
case neg.h
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ¬↑p ≤ z
⊢ ∀ (p_1 : ℕ), p_1.Prime → ↑p_1 ≤ z → ¬p_1 ∣ p
Theorem: BrunTitchmarsh.primesBetween_subset
Proof state before:
case neg.h
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ¬↑p ≤ z
⊢ ∀ (p_1 : ℕ), p_1.Prime → ↑p_1 ≤ z → ¬p_1 ∣ p
Tactic:
intro q hq hqz
Proof state after:
case neg.h
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ¬↑p ≤ z
q : ℕ
hq : q.Prime
hqz : ↑q ≤ z
⊢ ¬q ∣ p
Theorem: BrunTitchmarsh.primesBetween_subset
Proof state before:
case neg.h
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ¬↑p ≤ z
q : ℕ
hq : q.Prime
hqz : ↑q ≤ z
⊢ ¬q ∣ p
Tactic:
rw[hp.dvd_iff_eq (hq.ne_one)]
Proof state after:
case neg.h
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ¬↑p ≤ z
q : ℕ
hq : q.Prime
hqz : ↑q ≤ z
⊢ ¬p = q
Theorem: BrunTitchmarsh.primesBetween_subset
Proof state before:
case neg.h
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ¬↑p ≤ z
q : ℕ
hq : q.Prime
hqz : ↑q ≤ z
⊢ ¬p = q
Tactic:
rintro rfl
Proof state after:
case neg.h
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ¬↑p ≤ z
hq : p.Prime
hqz : ↑p ≤ z
⊢ False
Theorem: BrunTitchmarsh.primesBetween_subset
Proof state before:
case neg.h
x y z : ℝ
hx✝ : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hx : x ≤ ↑p
hxy : p ≤ ⌊x + y⌋₊
hp : p.Prime
hpz : ¬↑p ≤ z
hq : p.Prime
hqz : ↑p ≤ z
⊢ False
Tactic:
exact hpz hqz
Proof state after:
no goals
Theorem: BrunTitchmarsh.primesBetween_le_siftedSum_add
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(primesBetween x (x + y)) ≤ (primeInterSieve x y z hz).siftedSum + z
Tactic:
trans ↑((Finset.Icc (Nat.ceil x) (Nat.floor (x+y))).filter (fun d => ∀ p:ℕ, p.Prime → p ≤ z → ¬p ∣ d)
    ∪ (Finset.Icc 1 (Nat.floor z))).card
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(primesBetween x (x + y)) ≤
    ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ∪ Finset.Icc 1 ⌊z⌋₊).card

x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ∪ Finset.Icc 1 ⌊z⌋₊).card ≤
    (primeInterSieve x y z hz).siftedSum + z
Theorem: BrunTitchmarsh.primesBetween_le_siftedSum_add
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ∪ Finset.Icc 1 ⌊z⌋₊).card ≤
    (primeInterSieve x y z hz).siftedSum + z
Tactic:
trans ↑((Finset.Icc (Nat.ceil x) (Nat.floor (x+y))).filter (fun d => ∀ p:ℕ, p.Prime → p ≤ z → ¬p ∣ d)).card
  + ↑(Finset.Icc 1 (Nat.floor z)).card
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ∪ Finset.Icc 1 ⌊z⌋₊).card ≤
    ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card +
      ↑(Finset.Icc 1 ⌊z⌋₊).card

x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card +
      ↑(Finset.Icc 1 ⌊z⌋₊).card ≤
    (primeInterSieve x y z hz).siftedSum + z
Theorem: BrunTitchmarsh.primesBetween_le_siftedSum_add
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card +
      ↑(Finset.Icc 1 ⌊z⌋₊).card ≤
    (primeInterSieve x y z hz).siftedSum + z
Tactic:
rw[siftedSum_eq_card]
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card +
      ↑(Finset.Icc 1 ⌊z⌋₊).card ≤
    ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card + z
Theorem: BrunTitchmarsh.primesBetween_le_siftedSum_add
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card +
      ↑(Finset.Icc 1 ⌊z⌋₊).card ≤
    ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card + z
Tactic:
gcongr
Proof state after:
case bc
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(Finset.Icc 1 ⌊z⌋₊).card ≤ z
Theorem: BrunTitchmarsh.primesBetween_le_siftedSum_add
Proof state before:
case bc
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(Finset.Icc 1 ⌊z⌋₊).card ≤ z
Tactic:
rw[Nat.card_Icc]
Proof state after:
case bc
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(⌊z⌋₊ + 1 - 1) ≤ z
Theorem: BrunTitchmarsh.primesBetween_le_siftedSum_add
Proof state before:
case bc
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(⌊z⌋₊ + 1 - 1) ≤ z
Tactic:
simp only [add_tsub_cancel_right]
Proof state after:
case bc
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑⌊z⌋₊ ≤ z
Theorem: BrunTitchmarsh.primesBetween_le_siftedSum_add
Proof state before:
case bc
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑⌊z⌋₊ ≤ z
Tactic:
apply Nat.floor_le
Proof state after:
case bc.ha
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ 0 ≤ z
Theorem: BrunTitchmarsh.primesBetween_le_siftedSum_add
Proof state before:
case bc.ha
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ 0 ≤ z
Tactic:
linarith
Proof state after:
no goals
Theorem: BrunTitchmarsh.primesBetween_le_siftedSum_add
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(primesBetween x (x + y)) ≤
    ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ∪ Finset.Icc 1 ⌊z⌋₊).card
Tactic:
rw [primesBetween]
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(Finset.filter Nat.Prime (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card ≤
    ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ∪ Finset.Icc 1 ⌊z⌋₊).card
Theorem: BrunTitchmarsh.primesBetween_le_siftedSum_add
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(Finset.filter Nat.Prime (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card ≤
    ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ∪ Finset.Icc 1 ⌊z⌋₊).card
Tactic:
norm_cast
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (Finset.filter Nat.Prime (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card ≤
    (Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ∪ Finset.Icc 1 ⌊z⌋₊).card
Theorem: BrunTitchmarsh.primesBetween_le_siftedSum_add
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (Finset.filter Nat.Prime (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card ≤
    (Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ∪ Finset.Icc 1 ⌊z⌋₊).card
Tactic:
apply Finset.card_le_card
Proof state after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ Finset.filter Nat.Prime (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ⊆
    Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ∪ Finset.Icc 1 ⌊z⌋₊
Theorem: BrunTitchmarsh.primesBetween_le_siftedSum_add
Proof state before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ Finset.filter Nat.Prime (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ⊆
    Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ∪ Finset.Icc 1 ⌊z⌋₊
Tactic:
exact primesBetween_subset _ _ _ hz
Proof state after:
no goals
Theorem: BrunTitchmarsh.primesBetween_le_siftedSum_add
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ∪ Finset.Icc 1 ⌊z⌋₊).card ≤
    ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card +
      ↑(Finset.Icc 1 ⌊z⌋₊).card
Tactic:
norm_cast
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ∪ Finset.Icc 1 ⌊z⌋₊).card ≤
    (Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card +
      (Finset.Icc 1 ⌊z⌋₊).card
Theorem: BrunTitchmarsh.primesBetween_le_siftedSum_add
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ∪ Finset.Icc 1 ⌊z⌋₊).card ≤
    (Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card +
      (Finset.Icc 1 ⌊z⌋₊).card
Tactic:
apply Finset.card_union_le
Proof state after:
no goals
Theorem: BrunTitchmarsh.Ioc_filter_dvd_eq
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
⊢ Finset.filter (fun x => d ∣ x) (Finset.Ioc a b) = Finset.image (fun x => x * d) (Finset.Ioc (a / d) (b / d))
Tactic:
ext n
Proof state after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ n ∈ Finset.filter (fun x => d ∣ x) (Finset.Ioc a b) ↔ n ∈ Finset.image (fun x => x * d) (Finset.Ioc (a / d) (b / d))
Theorem: BrunTitchmarsh.Ioc_filter_dvd_eq
Proof state before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ n ∈ Finset.filter (fun x => d ∣ x) (Finset.Ioc a b) ↔ n ∈ Finset.image (fun x => x * d) (Finset.Ioc (a / d) (b / d))
Tactic:
simp only [Finset.mem_filter, Finset.mem_Ioc, Nat.ceil_le, Finset.mem_image,
  Nat.le_floor_iff (show 0 ≤ x+y by linarith)]
Proof state after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ (a < n ∧ n ≤ b) ∧ d ∣ n ↔ ∃ a_1, (a / d < a_1 ∧ a_1 ≤ b / d) ∧ a_1 * d = n
Theorem: BrunTitchmarsh.Ioc_filter_dvd_eq
Proof state before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ (a < n ∧ n ≤ b) ∧ d ∣ n ↔ ∃ a_1, (a / d < a_1 ∧ a_1 ≤ b / d) ∧ a_1 * d = n
Tactic:
constructor
Proof state after:
case a.mp
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ (a < n ∧ n ≤ b) ∧ d ∣ n → ∃ a_2, (a / d < a_2 ∧ a_2 ≤ b / d) ∧ a_2 * d = n

case a.mpr
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ (∃ a_1, (a / d < a_1 ∧ a_1 ≤ b / d) ∧ a_1 * d = n) → (a < n ∧ n ≤ b) ∧ d ∣ n
Theorem: BrunTitchmarsh.Ioc_filter_dvd_eq
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ 0 ≤ x + y
Tactic:
linarith
Proof state after:
no goals
Theorem: BrunTitchmarsh.Ioc_filter_dvd_eq
Proof state before:
case a.mp
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ (a < n ∧ n ≤ b) ∧ d ∣ n → ∃ a_2, (a / d < a_2 ∧ a_2 ≤ b / d) ∧ a_2 * d = n
Tactic:
intro hn
Proof state after:
case a.mp
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
hn : (a < n ∧ n ≤ b) ∧ d ∣ n
⊢ ∃ a_1, (a / d < a_1 ∧ a_1 ≤ b / d) ∧ a_1 * d = n
Theorem: BrunTitchmarsh.Ioc_filter_dvd_eq
Proof state before:
case a.mp
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
hn : (a < n ∧ n ≤ b) ∧ d ∣ n
⊢ ∃ a_1, (a / d < a_1 ∧ a_1 ≤ b / d) ∧ a_1 * d = n
Tactic:
use  n/d
Proof state after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
hn : (a < n ∧ n ≤ b) ∧ d ∣ n
⊢ (a / d < n / d ∧ n / d ≤ b / d) ∧ n / d * d = n
Theorem: BrunTitchmarsh.Ioc_filter_dvd_eq
Proof state before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
hn : (a < n ∧ n ≤ b) ∧ d ∣ n
⊢ (a / d < n / d ∧ n / d ≤ b / d) ∧ n / d * d = n
Tactic:
rcases hn with ⟨⟨han, hnb⟩, hd⟩
Proof state after:
case h.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd✝ : d ≠ 0
n : ℕ
hd : d ∣ n
han : a < n
hnb : n ≤ b
⊢ (a / d < n / d ∧ n / d ≤ b / d) ∧ n / d * d = n
Theorem: BrunTitchmarsh.Ioc_filter_dvd_eq
Proof state before:
case h.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd✝ : d ≠ 0
n : ℕ
hd : d ∣ n
han : a < n
hnb : n ≤ b
⊢ (a / d < n / d ∧ n / d ≤ b / d) ∧ n / d * d = n
Tactic:
refine ⟨⟨?_, ?_⟩, ?_⟩
Proof state after:
case h.intro.intro.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd✝ : d ≠ 0
n : ℕ
hd : d ∣ n
han : a < n
hnb : n ≤ b
⊢ a / d < n / d

case h.intro.intro.refine_2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd✝ : d ≠ 0
n : ℕ
hd : d ∣ n
han : a < n
hnb : n ≤ b
⊢ n / d ≤ b / d

case h.intro.intro.refine_3
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd✝ : d ≠ 0
n : ℕ
hd : d ∣ n
han : a < n
hnb : n ≤ b
⊢ n / d * d = n
Theorem: BrunTitchmarsh.Ioc_filter_dvd_eq
Proof state before:
case h.intro.intro.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd✝ : d ≠ 0
n : ℕ
hd : d ∣ n
han : a < n
hnb : n ≤ b
⊢ a / d < n / d
Tactic:
exact Nat.div_lt_div_of_lt_of_dvd hd han
Proof state after:
no goals
Theorem: BrunTitchmarsh.Ioc_filter_dvd_eq
Proof state before:
case h.intro.intro.refine_2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd✝ : d ≠ 0
n : ℕ
hd : d ∣ n
han : a < n
hnb : n ≤ b
⊢ n / d ≤ b / d
Tactic:
exact Nat.div_le_div_right (Nat.le_floor hnb)
Proof state after:
no goals
Theorem: BrunTitchmarsh.Ioc_filter_dvd_eq
Proof state before:
case h.intro.intro.refine_3
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd✝ : d ≠ 0
n : ℕ
hd : d ∣ n
han : a < n
hnb : n ≤ b
⊢ n / d * d = n
Tactic:
exact Nat.div_mul_cancel hd
Proof state after:
no goals
Theorem: BrunTitchmarsh.Ioc_filter_dvd_eq
Proof state before:
case a.mpr
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ (∃ a_1, (a / d < a_1 ∧ a_1 ≤ b / d) ∧ a_1 * d = n) → (a < n ∧ n ≤ b) ∧ d ∣ n
Tactic:
rintro ⟨r, ⟨ha, ha'⟩, rfl⟩
Proof state after:
case a.mpr.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ (a < r * d ∧ r * d ≤ b) ∧ d ∣ r * d
Theorem: BrunTitchmarsh.Ioc_filter_dvd_eq
Proof state before:
case a.mpr.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ (a < r * d ∧ r * d ≤ b) ∧ d ∣ r * d
Tactic:
refine ⟨⟨?_, ?_⟩, ?_⟩
Proof state after:
case a.mpr.intro.intro.intro.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ a < r * d

case a.mpr.intro.intro.intro.refine_2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ r * d ≤ b

case a.mpr.intro.intro.intro.refine_3
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ d ∣ r * d
Theorem: BrunTitchmarsh.Ioc_filter_dvd_eq
Proof state before:
case a.mpr.intro.intro.intro.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ a < r * d
Tactic:
refine (Nat.div_lt_iff_lt_mul ?_).mp ha
Proof state after:
case a.mpr.intro.intro.intro.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ 0 < d
Theorem: BrunTitchmarsh.Ioc_filter_dvd_eq
Proof state before:
case a.mpr.intro.intro.intro.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ 0 < d
Tactic:
omega
Proof state after:
no goals
Theorem: BrunTitchmarsh.Ioc_filter_dvd_eq
Proof state before:
case a.mpr.intro.intro.intro.refine_2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ r * d ≤ b
Tactic:
exact Nat.mul_le_of_le_div d r b ha'
Proof state after:
no goals
Theorem: BrunTitchmarsh.Ioc_filter_dvd_eq
Proof state before:
case a.mpr.intro.intro.intro.refine_3
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ d ∣ r * d
Tactic:
exact Nat.dvd_mul_left d r
Proof state after:
no goals
Theorem: BrunTitchmarsh.card_Ioc_filter_dvd
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
⊢ (Finset.filter (fun x => d ∣ x) (Finset.Ioc a b)).card = b / d - a / d
Tactic:
rw [Ioc_filter_dvd_eq _ _ _ hd]
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
⊢ (Finset.image (fun x => x * d) (Finset.Ioc (a / d) (b / d))).card = b / d - a / d
Theorem: BrunTitchmarsh.card_Ioc_filter_dvd
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
⊢ (Finset.image (fun x => x * d) (Finset.Ioc (a / d) (b / d))).card = b / d - a / d
Tactic:
rw [Finset.card_image_of_injective _ <| mul_left_injective₀ hd]
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
⊢ (Finset.Ioc (a / d) (b / d)).card = b / d - a / d
Theorem: BrunTitchmarsh.card_Ioc_filter_dvd
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
⊢ (Finset.Ioc (a / d) (b / d)).card = b / d - a / d
Tactic:
simp
Proof state after:
no goals
Theorem: BrunTitchmarsh.multSum_eq
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (primeInterSieve x y z hz).multSum d = ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d)
Tactic:
unfold Sieve.multSum
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (∑ n ∈ (primeInterSieve x y z hz).support, if d ∣ n then (primeInterSieve x y z hz).weights n else 0) =
    ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d)
Theorem: BrunTitchmarsh.multSum_eq
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (∑ n ∈ (primeInterSieve x y z hz).support, if d ∣ n then (primeInterSieve x y z hz).weights n else 0) =
    ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d)
Tactic:
rw[primeInterSieve]
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (∑
      n ∈
        { support := Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊, prodPrimes := primorial ⌊z⌋₊, prodPrimes_squarefree := ⋯,
            weights := fun x => 1, weights_nonneg := primeInterSieve.proof_2, totalMass := y,
            nu := (↑ζ).pdiv ↑ArithmeticFunction.id, nu_mult := primeInterSieve.proof_3, nu_pos_of_prime := ⋯,
            nu_lt_one_of_prime := ⋯, level := z, one_le_level := hz }.support,
      if d ∣ n then
        { support := Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊, prodPrimes := primorial ⌊z⌋₊, prodPrimes_squarefree := ⋯,
              weights := fun x => 1, weights_nonneg := primeInterSieve.proof_2, totalMass := y,
              nu := (↑ζ).pdiv ↑ArithmeticFunction.id, nu_mult := primeInterSieve.proof_3, nu_pos_of_prime := ⋯,
              nu_lt_one_of_prime := ⋯, level := z, one_le_level := hz }.weights
          n
      else 0) =
    ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d)