awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ (↑P.k : ℂ) ∨ P.g₀ = 0
refine_2 :
  ∀ (hs' : s ≠ (↑P.k : ℂ)), DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) s
refine_2₁ :
  ∀ (hs' : P.g₀ = 0), DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) s
⊢ DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) s

Tactic:
rcases hs' with hs' | hs'
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ (↑P.k : ℂ)
refine_2 : DifferentiableAt ℂ (F := ℂ) (fun (y : ℂ) ↦ P.ε / ((↑P.k : ℂ) - y)) s
⊢ DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) s

Tactic:
apply DifferentiableAt.smul_const

Premises used: DifferentiableAt.smul_const
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ (↑P.k : ℂ)
refine_2 : (↑P.k : ℂ) - s ≠ 0
⊢ DifferentiableAt ℂ (F := ℂ) (fun (y : ℂ) ↦ P.ε / ((↑P.k : ℂ) - y)) s

Tactic:
apply (differentiableAt_const _).div ((differentiableAt_const _).sub (differentiable_id _))

Premises used: DifferentiableAt.div, differentiableAt_const
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ (↑P.k : ℂ)
⊢ (↑P.k : ℂ) - s ≠ 0

Tactic:
simpa [sub_eq_zero, eq_comm]

Premises used: sub_eq_zero, eq_comm
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : P.g₀ = 0
⊢ DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) s

Tactic:
simp [hs']
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
⊢ MellinConvergent.{u_1} (E := E) (fun (x : ℝ) ↦ P.f x - P.f₀) s

Tactic:
have hc1 : MellinConvergent (P.f · - P.f₀) s :=
    let ⟨_, ht⟩ := exists_gt s.re
    mellinConvergent_of_isBigO_rpow (P.hf_int.sub (locallyIntegrableOn_const _)) (P.hf_top _) ht
      P.hf_zero' hs
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent.{u_1} (E := E) (fun (x : ℝ) ↦ P.f x - P.f₀) s
⊢ HasMellin (fun (x : ℝ) ↦ P.f x - P.f₀) s (P.Λ s)

Tactic:
⟨hc1, ?_⟩

Premises used: And.intro, HasMellin
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent.{u_1} (E := E) (fun (x : ℝ) ↦ P.f x - P.f₀) s
refine : mellin (fun (x : ℝ) ↦ P.f x - P.f₀) s = P.Λ s
⊢ HasMellin (fun (x : ℝ) ↦ P.f x - P.f₀) s (P.Λ s)

Tactic:
refine ⟨hc1, ?_⟩
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent.{u_1} (E := E) (fun (x : ℝ) ↦ P.f x - P.f₀) s
⊢ HasMellin P.f_modif s (P.Λ₀ s)

Tactic:
have hc2 : HasMellin P.f_modif s (P.Λ₀ s) := P.toStrongFEPair.hasMellin s
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent.{u_1} (E := E) (fun (x : ℝ) ↦ P.f x - P.f₀) s
hc2 : HasMellin P.f_modif s (P.Λ₀ s)
⊢ mellin (fun (x : ℝ) ↦ P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀

Tactic:
have hc3 : mellin (fun x ↦ f_modif P x - f P x + P.f₀) s =
    (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀ := P.f_modif_aux2 hs
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent.{u_1} (E := E) (fun (x : ℝ) ↦ P.f x - P.f₀) s
hc2 : HasMellin P.f_modif s (P.Λ₀ s)
hc3 : mellin (fun (x : ℝ) ↦ P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
⊢ mellin (fun (t : ℝ) ↦ P.f_modif t - (P.f t - P.f₀)) s = mellin P.f_modif s - mellin (fun (x : ℝ) ↦ P.f x - P.f₀) s

Tactic:
have := (hasMellin_sub hc2.1 hc1).2
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent.{u_1} (E := E) (fun (x : ℝ) ↦ P.f x - P.f₀) s
hc2 : HasMellin P.f_modif s (P.Λ₀ s)
hc3 : mellin (fun (x : ℝ) ↦ P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
this :
  mellin (fun (t : ℝ) ↦ P.f_modif t - (P.f t - P.f₀)) s = mellin P.f_modif s - mellin (fun (x : ℝ) ↦ P.f x - P.f₀) s
⊢ mellin (fun (x : ℝ) ↦ P.f x - P.f₀) s = mellin P.f_modif s - (1 / s) • P.f₀ - (P.ε / ((↑P.k : ℂ) - s)) • P.g₀

Tactic:
simp_rw [← sub_add, hc3, eq_sub_iff_add_eq, ← eq_sub_iff_add_eq', ← sub_sub] at this

Premises used: sub_add, eq_sub_iff_add_eq', eq_sub_iff_add_eq, sub_sub
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent.{u_1} (E := E) (fun (x : ℝ) ↦ P.f x - P.f₀) s
hc2 : HasMellin P.f_modif s (P.Λ₀ s)
hc3 : mellin (fun (x : ℝ) ↦ P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
this : mellin (fun (x : ℝ) ↦ P.f x - P.f₀) s = mellin P.f_modif s - (1 / s) • P.f₀ - (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
⊢ mellin (fun (x : ℝ) ↦ P.f x - P.f₀) s = P.Λ s

Tactic:
this

Premises used: WeakFEPair.Λ₀, WeakFEPair.Λ
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent.{u_1} (E := E) (fun (x : ℝ) ↦ P.f x - P.f₀) s
hc2 : HasMellin P.f_modif s (P.Λ₀ s)
hc3 : mellin (fun (x : ℝ) ↦ P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
this : mellin (fun (x : ℝ) ↦ P.f x - P.f₀) s = mellin P.f_modif s - (1 / s) • P.f₀ - (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
⊢ mellin (fun (x : ℝ) ↦ P.f x - P.f₀) s = P.Λ s

Tactic:
exact this
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
⊢ P.Λ₀ ((↑P.k : ℂ) - s) = P.ε • P.symm.Λ₀ s

Tactic:
P.toStrongFEPair.functional_equation s

Premises used: WeakFEPair.Λ₀, StrongFEPair.functional_equation, WeakFEPair.toStrongFEPair, WeakFEPair.f_modif
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
⊢ P.Λ ((↑P.k : ℂ) - s) +
        (P.ε • P.symm.Λ₀ s + P.Λ₀ ((↑P.k : ℂ) - s) +
            P.ε • (P.symm.Λ s + (1 / s) • P.g₀ + (P.ε⁻¹ / ((↑P.k : ℂ) - s)) • P.f₀) +
          (1 / ((↑P.k : ℂ) - s)) • P.f₀) -
      (P.ε • P.symm.Λ s +
        (P.Λ₀ ((↑P.k : ℂ) - s) +
              (P.Λ ((↑P.k : ℂ) - s) + (1 / ((↑P.k : ℂ) - s)) • P.f₀ + (P.ε / ((↑P.k : ℂ) - ((↑P.k : ℂ) - s))) • P.g₀) +
            P.ε • P.symm.Λ₀ s +
          (P.ε * P.ε⁻¹ / ((↑P.k : ℂ) - s)) • P.f₀)) =
    0

Tactic:
module
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
a :
  P.Λ ((↑P.k : ℂ) - s) +
        (P.ε • P.symm.Λ₀ s + P.Λ₀ ((↑P.k : ℂ) - s) +
            P.ε • (P.symm.Λ s + (1 / s) • P.g₀ + (P.ε⁻¹ / ((↑P.k : ℂ) - s)) • P.f₀) +
          (1 / ((↑P.k : ℂ) - s)) • P.f₀) -
      (P.ε • P.symm.Λ s +
        (P.Λ₀ ((↑P.k : ℂ) - s) +
              (P.Λ ((↑P.k : ℂ) - s) + (1 / ((↑P.k : ℂ) - s)) • P.f₀ + (P.ε / ((↑P.k : ℂ) - ((↑P.k : ℂ) - s))) • P.g₀) +
            P.ε • P.symm.Λ₀ s +
          (P.ε * P.ε⁻¹ / ((↑P.k : ℂ) - s)) • P.f₀)) =
    0
⊢ P.Λ ((↑P.k : ℂ) - s) = P.ε • P.symm.Λ s

Tactic:
linear_combination (norm := module) P.functional_equation₀ s - P.Λ₀_eq (P.k - s)
    + congr(P.ε • $(P.symm_Λ₀_eq s)) + congr(($(mul_inv_cancel₀ P.hε) / ((P.k:ℂ) - s)) • P.f₀)

Premises used: WeakFEPair.symm_Λ₀_eq, HSub.hSub, WeakFEPair.ε, WeakFEPair.Λ₀_eq, WeakFEPair.f₀, Complex.ofReal, WeakFEPair.functional_equation₀, WeakFEPair.k
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ 𝓝 (P.ε • P.g₀) = 𝓝 (HSub.hSub (α := E) 0 0 - -P.ε • P.g₀)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
simp_rw :
  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 : ℂ)) (𝓝 (HSub.hSub (α := E) 0 0 - -P.ε • P.g₀))
⊢ 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₀))]

Premises used: WeakFEPair.Λ, smul_sub
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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 : ℂ)) (𝓝 (HSub.hSub (α := E) 0 0 - -P.ε • P.g₀))

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

Premises used: nhdsWithin_le_nhds, Filter.Tendsto.mono_left, Filter.Tendsto.sub
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
refine_1 : Tendsto.{0, u_1} (β := E) (fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • P.Λ₀ s) (𝓝 (↑P.k : ℂ)) (𝓝 0)
refine_2 : Tendsto.{0, u_1} (β := E) (fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • (1 / s) • P.f₀) (𝓝 (↑P.k : ℂ)) (𝓝 0)
refine_3 :
  Tendsto (fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) (𝓝[≠] (↑P.k : ℂ)) (𝓝 (-P.ε • P.g₀))
⊢ 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 : ℂ)) (𝓝 (HSub.hSub (α := E) 0 0 - -P.ε • P.g₀))

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

Premises used: nhdsWithin_le_nhds, Filter.Tendsto.mono_left, Filter.Tendsto.sub
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
rw : 𝓝 0 = 𝓝 (HSMul.hSMul (α := ℂ) 0 (P.Λ₀ (↑P.k : ℂ)))
rw₁ rw₂ : Eq.{u_1 + 1} (α := Filter E) (𝓝 0) (𝓝 0)
⊢ 𝓝 0 = 𝓝 (((↑P.k : ℂ) - (↑P.k : ℂ)) • P.Λ₀ (↑P.k : ℂ))

Tactic:
rw [sub_self, zero_smul]

Premises used: sub_self, zero_smul
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
refine_1 :
  Tendsto (fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • P.Λ₀ s) (𝓝 (↑P.k : ℂ)) (𝓝 (((↑P.k : ℂ) - (↑P.k : ℂ)) • P.Λ₀ (↑P.k : ℂ)))
⊢ Tendsto.{0, u_1} (β := E) (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))]
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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

Premises used: Continuous.tendsto, Continuous.smul, continuous_sub_right, Differentiable.continuous, WeakFEPair.differentiable_Λ₀
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
rw : 𝓝 0 = 𝓝 (HSMul.hSMul (α := ℂ) 0 ((1 / (↑P.k : ℂ)) • P.f₀))
rw₁ rw₂ : Eq.{u_1 + 1} (α := Filter E) (𝓝 0) (𝓝 0)
⊢ 𝓝 0 = 𝓝 (((↑P.k : ℂ) - (↑P.k : ℂ)) • (1 / (↑P.k : ℂ)) • P.f₀)

Tactic:
rw [sub_self, zero_smul]

Premises used: sub_self, zero_smul
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
refine_2 :
  Tendsto (fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • (1 / s) • P.f₀) (𝓝 (↑P.k : ℂ))
    (𝓝 (((↑P.k : ℂ) - (↑P.k : ℂ)) • (1 / (↑P.k : ℂ)) • P.f₀))
⊢ Tendsto.{0, u_1} (β := E) (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₀))]
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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:
(continuous_sub_right _).continuousAt.smul (ContinuousAt.smul ?_ continuousAt_const)

Premises used: ContinuousAt, ContinuousAt.smul, continuousAt_const, Continuous.continuousAt, continuous_sub_right
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
refine_2 : ContinuousAt (HDiv.hDiv (α := ℂ) 1) (↑P.k : ℂ)
⊢ 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)

Premises used: ContinuousAt.smul, continuousAt_const, Continuous.continuousAt, continuous_sub_right
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ (↑P.k : ℂ) ≠ 0

Tactic:
have := ofReal_ne_zero.mpr P.hk.ne'
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
this : (↑P.k : ℂ) ≠ 0
funProp : (↑P.k : ℂ) ≠ 0
⊢ ContinuousAt (HDiv.hDiv (α := ℂ) 1) (↑P.k : ℂ)

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) (𝓝[≠] (↑P.k : ℂ)) (𝓝 (-P.ε • P.g₀))

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

Premises used: tendsto_const_nhds, nhdsWithin_le_nhds, Filter.Tendsto.mono_left, Filter.Tendsto.congr'
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
refine_3 :
  EventuallyEq.{0, u_1} (β := E) (𝓝[≠] (↑P.k : ℂ)) (fun (x : ℂ) ↦ -P.ε • P.g₀) fun (s : ℂ) ↦
    (s - (↑P.k : ℂ)) • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
⊢ 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' ?_

Premises used: tendsto_const_nhds, nhdsWithin_le_nhds, Filter.Tendsto.mono_left, Filter.Tendsto.congr'
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ EventuallyEq.{0, u_1} (β := E) (𝓝[≠] (↑P.k : ℂ)) (fun (x : ℂ) ↦ -P.ε • P.g₀) fun (s : ℂ) ↦
    (s - (↑P.k : ℂ)) • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀

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

Premises used: Filter.EventuallyEq, eventually_nhdsWithin_of_forall
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
refine_3 :
  ∀ (s : ℂ) (hs : s ≠ (↑P.k : ℂ)),
    Eq.{u_1 + 1} (α := E) ((fun (x : ℂ) ↦ -P.ε • P.g₀) s)
      ((fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) s)
⊢ EventuallyEq.{0, u_1} (β := E) (𝓝[≠] (↑P.k : ℂ)) (fun (x : ℂ) ↦ -P.ε • P.g₀) fun (s : ℂ) ↦
    (s - (↑P.k : ℂ)) • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀

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

Premises used: eventually_nhdsWithin_of_forall
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ (↑P.k : ℂ)
match_scalars : -P.ε * 1 = (s - (↑P.k : ℂ)) * (P.ε / ((↑P.k : ℂ) - s) * 1)
⊢ Eq.{u_1 + 1} (α := E) ((fun (x : ℂ) ↦ -P.ε • P.g₀) s)
    ((fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) s)

Tactic:
match_scalars
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ (↑P.k : ℂ)
⊢ -P.ε * 1 = (s - (↑P.k : ℂ)) * (P.ε / ((↑P.k : ℂ) - s) * 1)

Tactic:
field [sub_ne_zero.mpr hs.symm]

Premises used: Iff.mpr, sub_ne_zero, Ne.symm
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ 𝓝 (-P.f₀) = 𝓝 (HSMul.hSMul (α := ℂ) 0 (P.Λ₀ 0) - P.f₀ - 0)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
simp_rw :
  Tendsto (fun (s : ℂ) ↦ s • P.Λ₀ s - s • (1 / s) • P.f₀ - s • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) (𝓝[≠] 0)
    (𝓝 (HSMul.hSMul (α := ℂ) 0 (P.Λ₀ 0) - P.f₀ - 0))
⊢ Tendsto (fun (s : ℂ) ↦ s • P.Λ s) (𝓝[≠] 0) (𝓝 (-P.f₀))

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

Premises used: WeakFEPair.Λ, smul_sub
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun (s : ℂ) ↦ s • P.Λ₀ s - s • (1 / s) • P.f₀ - s • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) (𝓝[≠] 0)
    (𝓝 (HSMul.hSMul (α := ℂ) 0 (P.Λ₀ 0) - P.f₀ - 0))

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

Premises used: nhdsWithin_le_nhds, Filter.Tendsto.mono_left, Filter.Tendsto.sub
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
refine_1 : Tendsto (fun (s : ℂ) ↦ s • P.Λ₀ s) (𝓝 0) (𝓝 (HSMul.hSMul (α := ℂ) 0 (P.Λ₀ 0)))
refine_2 : Tendsto (fun (s : ℂ) ↦ s • (1 / s) • P.f₀) (𝓝[≠] 0) (𝓝 P.f₀)
refine_3 : Tendsto.{0, u_1} (β := E) (fun (s : ℂ) ↦ s • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) (𝓝[≠] 0) (𝓝 0)
⊢ Tendsto (fun (s : ℂ) ↦ s • P.Λ₀ s - s • (1 / s) • P.f₀ - s • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) (𝓝[≠] 0)
    (𝓝 (HSMul.hSMul (α := ℂ) 0 (P.Λ₀ 0) - P.f₀ - 0))

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

Premises used: nhdsWithin_le_nhds, Filter.Tendsto.mono_left, Filter.Tendsto.sub
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun (s : ℂ) ↦ s • P.Λ₀ s) (𝓝 0) (𝓝 (HSMul.hSMul (α := ℂ) 0 (P.Λ₀ 0)))

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

Premises used: Continuous.tendsto, Continuous.smul, continuous_id, Differentiable.continuous, WeakFEPair.differentiable_Λ₀
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun (s : ℂ) ↦ s • P.Λ₀ s) (𝓝 0) (𝓝 (HSMul.hSMul (α := ℂ) 0 (P.Λ₀ 0)))

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

Premises used: Continuous.tendsto, Continuous.smul, continuous_id, Differentiable.continuous, WeakFEPair.differentiable_Λ₀
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun (s : ℂ) ↦ s • (1 / s) • P.f₀) (𝓝[≠] 0) (𝓝 P.f₀)

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

Premises used: tendsto_const_nhds, nhdsWithin_le_nhds, Filter.Tendsto.mono_left, Filter.Tendsto.congr'
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
refine_2 : EventuallyEq.{0, u_1} (β := E) (𝓝[≠] 0) (fun (x : ℂ) ↦ P.f₀) fun (s : ℂ) ↦ s • (1 / s) • P.f₀
⊢ Tendsto (fun (s : ℂ) ↦ s • (1 / s) • P.f₀) (𝓝[≠] 0) (𝓝 P.f₀)

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

Premises used: tendsto_const_nhds, nhdsWithin_le_nhds, Filter.Tendsto.mono_left, Filter.Tendsto.congr'
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ EventuallyEq.{0, u_1} (β := E) (𝓝[≠] 0) (fun (x : ℂ) ↦ P.f₀) fun (s : ℂ) ↦ s • (1 / s) • P.f₀

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

Premises used: Filter.EventuallyEq, eventually_nhdsWithin_of_forall
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
refine_2 : ∀ (s : ℂ) (hs : s ≠ 0), Eq.{u_1 + 1} (α := E) ((fun (x : ℂ) ↦ P.f₀) s) ((fun (s : ℂ) ↦ s • (1 / s) • P.f₀) s)
⊢ EventuallyEq.{0, u_1} (β := E) (𝓝[≠] 0) (fun (x : ℂ) ↦ P.f₀) fun (s : ℂ) ↦ s • (1 / s) • P.f₀

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

Premises used: eventually_nhdsWithin_of_forall
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0
match_scalars : 1 = s * (1 / s * 1)
⊢ Eq.{u_1 + 1} (α := E) ((fun (x : ℂ) ↦ P.f₀) s) ((fun (s : ℂ) ↦ s • (1 / s) • P.f₀) s)

Tactic:
match_scalars
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0
⊢ 1 = s * (1 / s * 1)

Tactic:
field [sub_ne_zero.mpr hs.symm]

Premises used: Iff.mpr, sub_ne_zero, Ne.symm
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
rw rw₁ : Eq.{u_1 + 1} (α := Filter E) (𝓝 0) (𝓝 0)
⊢ 𝓝 0 = 𝓝 (HSMul.hSMul (α := ℂ) 0 ((P.ε / ((↑P.k : ℂ) - 0)) • P.g₀))

Tactic:
rw [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
refine_3 :
  Tendsto (fun (s : ℂ) ↦ s • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) (𝓝[≠] 0)
    (𝓝 (HSMul.hSMul (α := ℂ) 0 ((P.ε / ((↑P.k : ℂ) - 0)) • P.g₀)))
⊢ Tendsto.{0, u_1} (β := E) (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]]
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ (↑P.k : ℂ) - 0 ≠ 0

Tactic:
simpa using P.hk.ne'

Premises used: WeakFEPair.hk, LT.lt.ne'
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun (s : ℂ) ↦ s • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) (𝓝[≠] 0)
    (𝓝 (HSMul.hSMul (α := ℂ) 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

Premises used: ContinuousAt.smul, continuousAt_const, Continuous.continuousAt, nhdsWithin_le_nhds, ContinuousAt.div, Filter.Tendsto.mono_left, continuous_sub_left, continuousAt_id
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term f s n = if n = 0 then 0 else f n / HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
rfl

Premises used: LSeries.term, rfl