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

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b : ℕ
⊢ ∃ C, |C| ≤ 1 ∧ ↑(a / b) = ↑a / ↑b + C
Tactic:
rw[←Nat.floor_div_eq_div (α:=ℝ)]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b : ℕ
⊢ ∃ C, |C| ≤ 1 ∧ ↑⌊↑a / ↑b⌋₊ = ↑a / ↑b + C

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b : ℕ
⊢ ∃ C, |C| ≤ 1 ∧ ↑⌊↑a / ↑b⌋₊ = ↑a / ↑b + C
Tactic:
apply floor_approx (a/b:ℝ) (by positivity)
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b : ℕ
⊢ 0 ≤ ↑a / ↑b
Tactic:
positivity
State after:
no goals