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

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (primeInterSieve x y z hz).siftedSum =
    ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card
Tactic:
apply Sieve.siftedSum_eq
State after:
case hw
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ i ∈ (primeInterSieve x y z hz).support, (primeInterSieve x y z hz).weights i = 1

case hz
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ 1 ≤ z

case hP
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (primeInterSieve x y z hz).prodPrimes = primorial ⌊z⌋₊

State before:
case hw
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ i ∈ (primeInterSieve x y z hz).support, (primeInterSieve x y z hz).weights i = 1

case hz
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ 1 ≤ z

case hP
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (primeInterSieve x y z hz).prodPrimes = primorial ⌊z⌋₊
Tactic:
exact fun _ _ => rfl
State after:
case hz
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ 1 ≤ z

case hP
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (primeInterSieve x y z hz).prodPrimes = primorial ⌊z⌋₊

State before:
case hz
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ 1 ≤ z

case hP
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (primeInterSieve x y z hz).prodPrimes = primorial ⌊z⌋₊
Tactic:
exact hz
State after:
case hP
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (primeInterSieve x y z hz).prodPrimes = primorial ⌊z⌋₊

State before:
case hP
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (primeInterSieve x y z hz).prodPrimes = primorial ⌊z⌋₊
Tactic:
rfl
State after:
no goals