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

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n : ℕ
⊢ primesBetween 1 ↑n = (Finset.filter Nat.Prime (Finset.range (n + 1))).card
Tactic:
rw [primesBetween]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n : ℕ
⊢ (Finset.filter Nat.Prime (Finset.Icc ⌈1⌉₊ ⌊↑n⌋₊)).card = (Finset.filter Nat.Prime (Finset.range (n + 1))).card

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n : ℕ
⊢ (Finset.filter Nat.Prime (Finset.Icc ⌈1⌉₊ ⌊↑n⌋₊)).card = (Finset.filter Nat.Prime (Finset.range (n + 1))).card
Tactic:
congr 1
State after:
case e_s
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n : ℕ
⊢ Finset.filter Nat.Prime (Finset.Icc ⌈1⌉₊ ⌊↑n⌋₊) = Finset.filter Nat.Prime (Finset.range (n + 1))

State before:
case e_s
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n : ℕ
⊢ Finset.filter Nat.Prime (Finset.Icc ⌈1⌉₊ ⌊↑n⌋₊) = Finset.filter Nat.Prime (Finset.range (n + 1))
Tactic:
ext p
State after:
case e_s.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
⊢ p ∈ Finset.filter Nat.Prime (Finset.Icc ⌈1⌉₊ ⌊↑n⌋₊) ↔ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1))

State before:
case e_s.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
⊢ p ∈ Finset.filter Nat.Prime (Finset.Icc ⌈1⌉₊ ⌊↑n⌋₊) ↔ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1))
Tactic:
simp only [Nat.ceil_one, Nat.floor_coe, Finset.mem_filter, Finset.mem_Icc, Finset.mem_range,
  and_congr_left_iff]
State after:
case e_s.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
⊢ p.Prime → (1 ≤ p ∧ p ≤ n ↔ p < n + 1)

State before:
case e_s.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
⊢ p.Prime → (1 ≤ p ∧ p ≤ n ↔ p < n + 1)
Tactic:
intro hp
State after:
case e_s.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
⊢ 1 ≤ p ∧ p ≤ n ↔ p < n + 1

State before:
case e_s.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
⊢ 1 ≤ p ∧ p ≤ n ↔ p < n + 1
Tactic:
refine ⟨?_, ?_⟩
State after:
case e_s.a.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
⊢ 1 ≤ p ∧ p ≤ n → p < n + 1

case e_s.a.refine_2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
⊢ p < n + 1 → 1 ≤ p ∧ p ≤ n

State before:
case e_s.a.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
⊢ 1 ≤ p ∧ p ≤ n → p < n + 1
Tactic:
exact fun h => by omega
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
h : 1 ≤ p ∧ p ≤ n
⊢ p < n + 1
Tactic:
omega
State after:
no goals

State before:
case e_s.a.refine_2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
⊢ p < n + 1 → 1 ≤ p ∧ p ≤ n
Tactic:
refine fun h => ⟨by have := hp.pos; omega, by omega⟩
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
h : p < n + 1
⊢ 1 ≤ p
Tactic:
have := hp.pos
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
h : p < n + 1
this : 0 < p
⊢ 1 ≤ p

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
h : p < n + 1
this : 0 < p
⊢ 1 ≤ p
Tactic:
omega
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
hp : p.Prime
h : p < n + 1
⊢ p ≤ n
Tactic:
omega
State after:
no goals