-- Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
theorem Λ_residue_zero :
    Tendsto (fun s : ℂ ↦ s • P.Λ s) (𝓝[≠] 0) (𝓝 (-P.f₀))

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s => s • P.Λ₀ s - s • (1 / s) • P.f₀ - s • (P.ε / (↑P.k - s)) • P.g₀) (𝓝[≠] 0)
    (𝓝 (0 • P.Λ₀ 0 - P.f₀ - 0))

Tactic:
refine ((Tendsto.mono_left ?_ nhdsWithin_le_nhds).sub ?_).sub ?_

Result:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s => s • P.Λ₀ s) (𝓝 0) (𝓝 (0 • P.Λ₀ 0))

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s => s • (1 / s) • P.f₀) (𝓝[≠] 0) (𝓝 P.f₀)

case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s => s • (P.ε / (↑P.k - s)) • P.g₀) (𝓝[≠] 0) (𝓝 0)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ 𝓝 0 = 𝓝 (0 • (P.ε / (↑P.k - 0)) • P.g₀)

Tactic:
rw [zero_smul]

Result:
no goals

Proof state:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x => P.f₀) =ᶠ[𝓝[≠] 0] fun s => s • (1 / s) • P.f₀

Tactic:
refine eventually_nhdsWithin_of_forall (fun s (hs : s ≠ 0) ↦ ?_)

Result:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0
⊢ (fun x => P.f₀) s = (fun s => s • (1 / s) • P.f₀) s

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0
⊢ 1 = s * (1 / s * 1)

Tactic:
field_simp [sub_ne_zero.mpr hs.symm]

Result:
no goals

Proof state:
case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s => s • (P.ε / (↑P.k - s)) • P.g₀) (𝓝[≠] 0) (𝓝 (0 • (P.ε / (↑P.k - 0)) • P.g₀))

Tactic:
exact (continuousAt_id.smul ((continuousAt_const.div ((continuous_sub_left _).continuousAt)
  (by simpa using P.hk.ne')).smul continuousAt_const)).mono_left nhdsWithin_le_nhds

Result:
no goals

Proof state:
case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s => s • (P.ε / (↑P.k - s)) • P.g₀) (𝓝[≠] 0) (𝓝 0)

Tactic:
rw [show 𝓝 0 = 𝓝 ((0 : ℂ) • (P.ε / (P.k - 0 : ℂ)) • P.g₀) by rw [zero_smul]]

Result:
case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s => s • (P.ε / (↑P.k - s)) • P.g₀) (𝓝[≠] 0) (𝓝 (0 • (P.ε / (↑P.k - 0)) • P.g₀))

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ 𝓝 (-P.f₀) = 𝓝 (0 • P.Λ₀ 0 - P.f₀ - 0)

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s => s • (1 / s) • P.f₀) (𝓝[≠] 0) (𝓝 P.f₀)

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

Result:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x => P.f₀) =ᶠ[𝓝[≠] 0] fun s => s • (1 / s) • P.f₀

Proof state:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s => s • P.Λ₀ s) (𝓝 0) (𝓝 (0 • P.Λ₀ 0))

Tactic:
exact (continuous_id.smul P.differentiable_Λ₀.continuous).tendsto _

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s => s • P.Λ s) (𝓝[≠] 0) (𝓝 (-P.f₀))

Tactic:
simp_rw [Λ, smul_sub, (by simp : 𝓝 (-P.f₀) = 𝓝 (((0 : ℂ) • P.Λ₀ 0) - P.f₀ - 0))]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s => s • P.Λ₀ s - s • (1 / s) • P.f₀ - s • (P.ε / (↑P.k - s)) • P.g₀) (𝓝[≠] 0)
    (𝓝 (0 • P.Λ₀ 0 - P.f₀ - 0))

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ ↑P.k - 0 ≠ 0

Tactic:
simpa using P.hk.ne'

Result:
no goals

Proof state:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0
⊢ (fun x => P.f₀) s = (fun s => s • (1 / s) • P.f₀) s

Tactic:
match_scalars

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0
⊢ 1 = s * (1 / s * 1)