Theorem: BrunTitchmarsh.primesBetween_le_siftedSum_add (PrimeNumberTheoremAnd/BrunTitchmarsh.lean)

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

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

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

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
State after:
case bc
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(Finset.Icc 1 ⌊z⌋₊).card ≤ z

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]
State after:
case bc
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(⌊z⌋₊ + 1 - 1) ≤ z

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]
State after:
case bc
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑⌊z⌋₊ ≤ z

State before:
case bc
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑⌊z⌋₊ ≤ z
Tactic:
apply Nat.floor_le
State after:
case bc.ha
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ 0 ≤ z

State before:
case bc.ha
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ 0 ≤ z
Tactic:
linarith
State after:
no goals

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

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

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

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

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

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