Theorem: BrunTitchmarsh.Nat.ceil_le_self_add_one (PrimeNumberTheoremAnd/BrunTitchmarsh.lean)

State before:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌈x⌉₊ ≤ x + 1
Tactic:
trans Nat.floor x + 1
State after:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌈x⌉₊ ≤ ↑⌊x⌋₊ + 1

x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌊x⌋₊ + 1 ≤ x + 1

State before:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌊x⌋₊ + 1 ≤ x + 1
Tactic:
gcongr
State after:
case bc
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌊x⌋₊ ≤ x

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

State before:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌈x⌉₊ ≤ ↑⌊x⌋₊ + 1
Tactic:
norm_cast
State after:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ⌈x⌉₊ ≤ ⌊x⌋₊ + 1

State before:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ⌈x⌉₊ ≤ ⌊x⌋₊ + 1
Tactic:
exact Nat.ceil_le_floor_add_one x
State after:
no goals