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

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

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

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

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

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

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

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

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

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

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

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

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⟩, ?_⟩
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

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

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

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

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