Theorem: riemannZeta_isBigO_of_ne_one_horizontal (EulerProducts/PNT.lean)

State before:
y : ℝ
hy : y ≠ 0
⊢ (fun x => ζ (1 + ↑x + I * ↑y)) =O[𝓝[>] 0] fun x => 1
Tactic:
refine Asymptotics.IsBigO.mono ?_ nhdsWithin_le_nhds
State after:
y : ℝ
hy : y ≠ 0
⊢ (fun x => ζ (1 + ↑x + I * ↑y)) =O[𝓝 0] fun x => 1

State before:
y : ℝ
hy : y ≠ 0
⊢ (fun x => ζ (1 + ↑x + I * ↑y)) =O[𝓝 0] fun x => 1
Tactic:
have hy' : 1 + I * y ≠ 1 := by simp [hy]
State after:
y : ℝ
hy : y ≠ 0
hy' : 1 + I * ↑y ≠ 1
⊢ (fun x => ζ (1 + ↑x + I * ↑y)) =O[𝓝 0] fun x => 1

State before:
y : ℝ
hy : y ≠ 0
hy' : 1 + I * ↑y ≠ 1
⊢ (fun x => ζ (1 + ↑x + I * ↑y)) =O[𝓝 0] fun x => 1
Tactic:
convert isBigO_comp_ofReal
  (differentiableAt_riemannZeta hy').continuousAt.isBigO using 3 with x
State after:
case h.e'_7.h.h.e'_1
y : ℝ
hy : y ≠ 0
hy' : 1 + I * ↑y ≠ 1
x : ℝ
⊢ 1 + ↑x + I * ↑y = ↑x + (1 + I * ↑y)

State before:
case h.e'_7.h.h.e'_1
y : ℝ
hy : y ≠ 0
hy' : 1 + I * ↑y ≠ 1
x : ℝ
⊢ 1 + ↑x + I * ↑y = ↑x + (1 + I * ↑y)
Tactic:
ring
State after:
no goals

State before:
y : ℝ
hy : y ≠ 0
⊢ 1 + I * ↑y ≠ 1
Tactic:
simp [hy]
State after:
no goals