-- Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
theorem hasMellin [CompleteSpace E]
    {s : ℂ} (hs : P.k < s.re) : HasMellin (P.f · - P.f₀) s (P.Λ s)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent (fun x => P.f x - P.f₀) s
⊢ mellin (fun x => P.f x - P.f₀) s = P.Λ s

Tactic:
have hc2 : HasMellin P.f_modif s (P.Λ₀ s) := P.toStrongFEPair.hasMellin s

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent (fun x => P.f x - P.f₀) s
hc2 : HasMellin P.f_modif s (P.Λ₀ s)
⊢ mellin (fun x => P.f x - P.f₀) s = P.Λ s

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent (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 x => P.f x - P.f₀) s = P.Λ s

Tactic:
have := (hasMellin_sub hc2.1 hc1).2

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent (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 = P.Λ s

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent (fun x => P.f x - P.f₀) s
hc2 : HasMellin P.f_modif s (P.Λ₀ s)
⊢ mellin (fun x => P.f x - P.f₀) s = P.Λ s

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

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent (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 x => P.f x - P.f₀) s = P.Λ s

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent (fun x => P.f x - P.f₀) s
⊢ HasMellin (fun x => P.f x - P.f₀) s (P.Λ s)

Tactic:
refine ⟨hc1, ?_⟩

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent (fun x => P.f x - P.f₀) s
⊢ mellin (fun x => P.f x - P.f₀) s = P.Λ s

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent (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 = P.Λ s

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

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent (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

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent (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

Result:
no goals