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

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => 1 + N.log / Real.log 2) =O[atTop] fun N => N.log
Tactic:
refine IsBigO.add ?h₁ ?h₂
State after:
case h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => 1) =O[atTop] fun N => N.log

case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => N.log / Real.log 2) =O[atTop] fun N => N.log

State before:
case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => N.log / Real.log 2) =O[atTop] fun N => N.log
Tactic:
simp_rw [div_eq_inv_mul]
State after:
case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => (Real.log 2)⁻¹ * N.log) =O[atTop] fun N => N.log

State before:
case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => (Real.log 2)⁻¹ * N.log) =O[atTop] fun N => N.log
Tactic:
apply IsBigO.const_mul_left
State after:
case h₂.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => x.log) =O[atTop] fun N => N.log

State before:
case h₂.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => x.log) =O[atTop] fun N => N.log
Tactic:
apply isBigO_refl
State after:
no goals

State before:
case h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => 1) =O[atTop] fun N => N.log
Tactic:
convert Real.isLittleO_const_log_atTop.isBigO
State after:
no goals