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

State before:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ∃ C, |C| ≤ 1 ∧ ↑⌈x⌉₊ = x + C
Tactic:
use ↑(Nat.ceil x) - x
State after:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ |↑⌈x⌉₊ - x| ≤ 1 ∧ ↑⌈x⌉₊ = x + (↑⌈x⌉₊ - x)

State before:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ |↑⌈x⌉₊ - x| ≤ 1 ∧ ↑⌈x⌉₊ = x + (↑⌈x⌉₊ - x)
Tactic:
simp only [add_sub_cancel, and_true]
State after:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ |↑⌈x⌉₊ - x| ≤ 1

State before:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ |↑⌈x⌉₊ - x| ≤ 1
Tactic:
rw[abs_le]
State after:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ -1 ≤ ↑⌈x⌉₊ - x ∧ ↑⌈x⌉₊ - x ≤ 1

State before:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ -1 ≤ ↑⌈x⌉₊ - x ∧ ↑⌈x⌉₊ - x ≤ 1
Tactic:
constructor
State after:
case h.left
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ -1 ≤ ↑⌈x⌉₊ - x

case h.right
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌈x⌉₊ - x ≤ 1

State before:
case h.left
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ -1 ≤ ↑⌈x⌉₊ - x
Tactic:
simp only [neg_le_sub_iff_le_add]
State after:
case h.left
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ x ≤ ↑⌈x⌉₊ + 1

State before:
case h.left
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ x ≤ ↑⌈x⌉₊ + 1
Tactic:
linarith [Nat.le_ceil x]
State after:
no goals

State before:
case h.right
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌈x⌉₊ - x ≤ 1
Tactic:
simp only [tsub_le_iff_right]
State after:
case h.right
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌈x⌉₊ ≤ 1 + x

State before:
case h.right
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌈x⌉₊ ≤ 1 + x
Tactic:
rw[add_comm]
State after:
case h.right
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌈x⌉₊ ≤ x + 1

State before:
case h.right
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌈x⌉₊ ≤ x + 1
Tactic:
exact Nat.ceil_le_self_add_one x hx
State after:
no goals