-- Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
theorem _root_.tendsto_riemannZeta_sub_one_div :
    Tendsto (fun s : ℂ ↦ riemannZeta s - 1 / (s - 1)) (𝓝[≠] 1) (𝓝 γ)

Proof state:
case refine_2.refine_2.hf
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun x => (x - 1) * (1 / (x - 1))) (𝓝[≠] 1) (𝓝 1)

Tactic:
refine Tendsto.congr' ?_ (tendsto_const_nhds.mono_left nhdsWithin_le_nhds)

Result:
case refine_2.refine_2.hf
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ (fun x => 1) =ᶠ[𝓝[≠] 1] fun x => (x - 1) * (1 / (x - 1))

Proof state:
case h
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
s : ℂ
hs : s ∈ {1}ᶜ
⊢ DifferentiableAt ℂ f s

Tactic:
refine (differentiableAt_riemannZeta hs).sub ((differentiableAt_const _).div ?_ ?_)

Result:
case h.refine_1
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
s : ℂ
hs : s ∈ {1}ᶜ
⊢ DifferentiableAt ℂ (fun s => s - 1) s

case h.refine_2
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
s : ℂ
hs : s ∈ {1}ᶜ
⊢ s - 1 ≠ 0

Proof state:
case h
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
a : ℝ
ha : a ∈ Ioi 1
⊢ ¬a = 1

Tactic:
exact ne_of_gt ha

Result:
no goals

Proof state:
case intro.refine_1
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
⊢ Tendsto Complex.ofReal (𝓝[>] 1) (𝓝 1)

Tactic:
exact (Complex.continuous_ofReal.tendsto 1).mono_left (nhdsWithin_le_nhds ..)

Result:
no goals

Proof state:
case h
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
t : ℂ
ht : t ∈ {1}ᶜ
ht' : t = 1
⊢ f t - f 1 = 0

Tactic:
tauto

Result:
no goals

Proof state:
case refine_2.refine_2.hf
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun x => f x * (x - 1)) (𝓝[≠] 1) (𝓝 (1 - 1))

Tactic:
simp_rw [mul_comm (f _), f, mul_sub]

Result:
case refine_2.refine_2.hf
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun x => (x - 1) * riemannZeta x - (x - 1) * (1 / (x - 1))) (𝓝[≠] 1) (𝓝 (1 - 1))

Proof state:
case intro
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
⊢ Tendsto (fun s => f ↑s) (𝓝[>] 1) (𝓝 C)

Tactic:
refine hC.comp (tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ ?_ ?_)

Result:
case intro.refine_1
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
⊢ Tendsto Complex.ofReal (𝓝[>] 1) (𝓝 1)

case intro.refine_2
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 1, ↑x ∈ {1}ᶜ

Proof state:
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ ∃ C, Tendsto f (𝓝[≠] 1) (𝓝 C)

Tactic:
refine ⟨_, Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO ?_ ?_⟩

Result:
case refine_1
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] 1, DifferentiableAt ℂ f z

case refine_2
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ (fun z => f z - f 1) =o[𝓝[≠] 1] fun z => (z - 1)⁻¹

Proof state:
case refine_2.refine_2
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun x => f x * (x - 1) - f 1 * (x - 1)) (𝓝[≠] 1) (𝓝 (1 - 1 - f 1 * (1 - 1)))

Tactic:
apply Tendsto.sub

Result:
case refine_2.refine_2.hf
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun x => f x * (x - 1)) (𝓝[≠] 1) (𝓝 (1 - 1))

case refine_2.refine_2.hg
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun x => f 1 * (x - 1)) (𝓝[≠] 1) (𝓝 (f 1 * (1 - 1)))

Proof state:
case refine_2.refine_2.hf
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun x => (x - 1) * riemannZeta x - (x - 1) * (1 / (x - 1))) (𝓝[≠] 1) (𝓝 (1 - 1))

Tactic:
apply riemannZeta_residue_one.sub

Result:
case refine_2.refine_2.hf
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun x => (x - 1) * (1 / (x - 1))) (𝓝[≠] 1) (𝓝 1)

Proof state:
case intro
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
⊢ Tendsto (fun s => riemannZeta s - 1 / (s - 1)) (𝓝[≠] 1) (𝓝 ↑γ)

Tactic:
suffices Tendsto (fun s : ℝ ↦ f s) _ _
  from (tendsto_nhds_unique this tendsto_riemannZeta_sub_one_div_nhds_right) ▸ hC

Result:
case intro
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
⊢ Tendsto (fun s => f ↑s) (𝓝[>] 1) (𝓝 C)

Proof state:
case h
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
a : ℝ
ha : a ∈ Ioi 1
⊢ ↑a ∈ {1}ᶜ

Tactic:
rw [mem_compl_singleton_iff, ← Complex.ofReal_one, Ne, Complex.ofReal_inj]

Result:
case h
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
a : ℝ
ha : a ∈ Ioi 1
⊢ ¬a = 1

Proof state:
case h.refine_2
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
s : ℂ
hs : s ∈ {1}ᶜ
⊢ s - 1 ≠ 0

Tactic:
rwa [mem_compl_singleton_iff, ← sub_ne_zero] at hs

Result:
no goals

Proof state:
⊢ Tendsto (fun s => riemannZeta s - 1 / (s - 1)) (𝓝[≠] 1) (𝓝 ↑γ)

Tactic:
let f (s : ℂ) := riemannZeta s - 1 / (s - 1)

Result:
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun s => riemannZeta s - 1 / (s - 1)) (𝓝[≠] 1) (𝓝 ↑γ)

Proof state:
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ 𝓝 0 = 𝓝 (1 - 1 - f 1 * (1 - 1))

Tactic:
ring_nf

Result:
no goals

Proof state:
case refine_2.refine_1
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ ∀ᶠ (x : ℂ) in 𝓝[≠] 1, (x - 1)⁻¹ = 0 → f x - f 1 = 0

Tactic:
filter_upwards [self_mem_nhdsWithin] with t ht ht'

Result:
case h
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
t : ℂ
ht : t ∈ {1}ᶜ
ht' : (t - 1)⁻¹ = 0
⊢ f t - f 1 = 0

Proof state:
case h.refine_1
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
s : ℂ
hs : s ∈ {1}ᶜ
⊢ DifferentiableAt ℂ (fun s => s - 1) s

Tactic:
fun_prop

Result:
no goals

Proof state:
case refine_2.refine_2.hg
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun x => f 1 * (x - 1)) (𝓝[≠] 1) (𝓝 (f 1 * (1 - 1)))

Tactic:
exact ((tendsto_id.sub tendsto_const_nhds).mono_left nhdsWithin_le_nhds).const_mul _

Result:
no goals

Proof state:
case intro.refine_2
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 1, ↑x ∈ {1}ᶜ

Tactic:
filter_upwards [self_mem_nhdsWithin] with a ha

Result:
case h
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
a : ℝ
ha : a ∈ Ioi 1
⊢ ↑a ∈ {1}ᶜ

Proof state:
case h
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
x : ℂ
hx : x ∈ {1}ᶜ
⊢ 1 = (x - 1) * (1 / (x - 1))

Tactic:
field_simp [sub_ne_zero.mpr <| mem_compl_singleton_iff.mp hx]

Result:
no goals

Proof state:
case h
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
t : ℂ
ht : t ∈ {1}ᶜ
ht' : (t - 1)⁻¹ = 0
⊢ f t - f 1 = 0

Tactic:
rw [inv_eq_zero, sub_eq_zero] at ht'

Result:
case h
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
t : ℂ
ht : t ∈ {1}ᶜ
ht' : t = 1
⊢ f t - f 1 = 0

Proof state:
case refine_2
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ (fun z => f z - f 1) =o[𝓝[≠] 1] fun z => (z - 1)⁻¹

Tactic:
refine Asymptotics.isLittleO_of_tendsto' ?_ ?_

Result:
case refine_2.refine_1
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ ∀ᶠ (x : ℂ) in 𝓝[≠] 1, (x - 1)⁻¹ = 0 → f x - f 1 = 0

case refine_2.refine_2
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun x => (f x - f 1) / (x - 1)⁻¹) (𝓝[≠] 1) (𝓝 0)

Proof state:
case refine_2.refine_2
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun x => (f x - f 1) / (x - 1)⁻¹) (𝓝[≠] 1) (𝓝 0)

Tactic:
simp_rw [div_eq_mul_inv, inv_inv, sub_mul,
  (by ring_nf : 𝓝 (0 : ℂ) = 𝓝 ((1 - 1) - f 1 * (1 - 1)))]

Result:
case refine_2.refine_2
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun x => f x * (x - 1) - f 1 * (x - 1)) (𝓝[≠] 1) (𝓝 (1 - 1 - f 1 * (1 - 1)))

Proof state:
case refine_2.refine_2.hf
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ (fun x => 1) =ᶠ[𝓝[≠] 1] fun x => (x - 1) * (1 / (x - 1))

Tactic:
filter_upwards [self_mem_nhdsWithin] with x hx

Result:
case h
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
x : ℂ
hx : x ∈ {1}ᶜ
⊢ 1 = (x - 1) * (1 / (x - 1))