Theorem: riemannZeta_isBigO_near_one_horizontal (EulerProducts/PNT.lean)

State before:
this : (fun w => ζ (1 + w)) =O[𝓝[≠] 0] fun x => 1 / x
⊢ (fun x => ζ (1 + ↑x)) =O[𝓝[>] 0] fun x => 1 / ↑x
Tactic:
exact (isBigO_comp_ofReal_nhds_ne this).mono <| nhds_right'_le_nhds_ne 0
State after:
no goals

State before:
H : Tendsto (fun w => w * ζ (1 + w)) (𝓝[≠] 0) (𝓝 1)
⊢ (fun w => ζ (1 + w)) =O[𝓝[≠] 0] fun x => 1 / x
Tactic:
exact ((isBigO_mul_iff_isBigO_div eventually_mem_nhdsWithin).mp <|
  Tendsto.isBigO_one ℂ H).trans <| isBigO_refl ..
State after:
no goals

State before:
⊢ Tendsto (fun w => w * ζ (1 + w)) (𝓝[≠] 0) (𝓝 1)
Tactic:
convert Tendsto.comp (f := fun w ↦ 1 + w) riemannZeta_residue_one ?_ using 1
State after:
case h.e'_3

⊢ (fun w => w * ζ (1 + w)) = (fun s => (s - 1) * ζ s) ∘ fun w => 1 + w

case convert_2

⊢ Tendsto (fun w => 1 + w) (𝓝[≠] 0) (𝓝[≠] 1)

State before:
case h.e'_3

⊢ (fun w => w * ζ (1 + w)) = (fun s => (s - 1) * ζ s) ∘ fun w => 1 + w
Tactic:
ext w
State after:
case h.e'_3.h
w : ℂ
⊢ w * ζ (1 + w) = ((fun s => (s - 1) * ζ s) ∘ fun w => 1 + w) w

State before:
case h.e'_3.h
w : ℂ
⊢ w * ζ (1 + w) = ((fun s => (s - 1) * ζ s) ∘ fun w => 1 + w) w
Tactic:
simp only [Function.comp_apply, add_sub_cancel_left]
State after:
no goals

State before:
case convert_2

⊢ Tendsto (fun w => 1 + w) (𝓝[≠] 0) (𝓝[≠] 1)
Tactic:
refine tendsto_iff_comap.mpr <| map_le_iff_le_comap.mp <| Eq.le ?_
State after:
case convert_2

⊢ map (fun w => 1 + w) (𝓝[≠] 0) = 𝓝[≠] 1

State before:
case convert_2

⊢ map (fun w => 1 + w) (𝓝[≠] 0) = 𝓝[≠] 1
Tactic:
convert map_punctured_nhds_eq (Homeomorph.addLeft (1 : ℂ)) 0 using 2 <;> simp
State after:
no goals