-- Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
theorem Λ_residue_k :
    Tendsto (fun s : ℂ ↦ (s - P.k) • P.Λ s) (𝓝[≠] P.k) (𝓝 (P.ε • P.g₀))

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

Tactic:
rw [(by rw [sub_self, zero_smul] : 𝓝 0 = 𝓝 ((P.k - P.k : ℂ) • (1 / P.k : ℂ) • P.f₀))]

Result:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s => (s - ↑P.k) • (1 / s) • P.f₀) (𝓝 ↑P.k) (𝓝 ((↑P.k - ↑P.k) • (1 / ↑P.k) • P.f₀))

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

Tactic:
refine (continuous_sub_right _).continuousAt.smul (ContinuousAt.smul ?_ continuousAt_const)

Result:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ ContinuousAt (HDiv.hDiv 1) ↑P.k

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

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ ContinuousAt (HDiv.hDiv 1) ↑P.k

Tactic:
exact continuousAt_const.div continuousAt_id (ofReal_ne_zero.mpr P.hk.ne')

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ ↑P.k
⊢ -(P.ε * (↑P.k - s)) = (s - ↑P.k) * P.ε

Tactic:
ring

Result:
no goals

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

Tactic:
match_scalars

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ ↑P.k
⊢ -P.ε * 1 = (s - ↑P.k) * (P.ε / (↑P.k - s) * 1)

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

Tactic:
rw [(by rw [sub_self, zero_smul] : 𝓝 0 = 𝓝 ((P.k - P.k : ℂ) • P.Λ₀ P.k))]

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

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

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

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

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

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

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

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

Tactic:
apply ((continuous_sub_right _).smul P.differentiable_Λ₀.continuous).tendsto

Result:
no goals

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

Tactic:
refine eventually_nhdsWithin_of_forall (fun s (hs : s ≠ P.k) ↦ ?_)

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

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

Tactic:
rw [sub_self, zero_smul]

Result:
no goals

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

Tactic:
field_simp [sub_ne_zero.mpr hs.symm]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ ↑P.k
⊢ -(P.ε * (↑P.k - s)) = (s - ↑P.k) * P.ε

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

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

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

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

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

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

Tactic:
rw [sub_self, zero_smul]

Result:
no goals