-- Mathlib/NumberTheory/LSeries/Deriv.lean
private lemma LSeries.LSeriesSummable_logMul_and_hasDerivAt {f : ℕ → ℂ} {s : ℂ}
    (h : abscissaOfAbsConv f < s.re) :
    LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Proof state:
case intro.intro.intro.intro
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n => ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x => term f x n) S
h₂ : IsOpen S
h₃ : ∀ (n : ℕ), ∀ z ∈ S, ‖term f z n‖ ≤ ‖term f (↑x) n‖
H : HasSum (fun i => deriv (fun x => term f x i) s) (deriv (fun w => ∑' (i : ℕ), term f w i) s)
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Tactic:
simp_rw [(hasDerivAt_term f _ _).deriv] at H

Result:
case intro.intro.intro.intro
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n => ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x => term f x n) S
h₂ : IsOpen S
h₃ : ∀ (n : ℕ), ∀ z ∈ S, ‖term f z n‖ ≤ ‖term f (↑x) n‖
H : HasSum (fun i => -term (logMul f) s i) (deriv (fun w => ∑' (i : ℕ), term f w i) s)
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Proof state:
case intro.intro.intro.intro
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n => ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x => term f x n) S
h₂ : IsOpen S
h₃ : ∀ (n : ℕ), ∀ z ∈ S, ‖term f z n‖ ≤ ‖term f (↑x) n‖
H : HasSum (fun i => -term (logMul f) s i) (deriv (fun w => ∑' (i : ℕ), term f w i) s)
⊢ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Tactic:
simpa [← H.tsum_eq, tsum_neg] using ((differentiableOn_tsum_of_summable_norm
  h₀ h₁ h₂ h₃).differentiableAt <| h₂.mem_nhds hys).hasDerivAt

Result:
no goals

Proof state:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n => ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x => term f x n) S
h₂ : IsOpen S
n : ℕ
z : ℂ
hz : z ∈ S
⊢ (↑x).re ≤ z.re

Tactic:
simpa using (hxy.trans hz).le

Result:
no goals

Proof state:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Tactic:
obtain ⟨x, hxs, hf⟩ := LSeriesSummable_lt_re_of_abscissaOfAbsConv_lt_re h

Result:
case intro.intro
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Proof state:
case intro.intro.intro.intro
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Tactic:
have h₀ : Summable (fun n ↦ ‖term f x n‖) := summable_norm_iff.mpr hf

Result:
case intro.intro.intro.intro
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n => ‖term f (↑x) n‖
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Proof state:
case intro.intro.intro.intro
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n => ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x => term f x n) S
h₂ : IsOpen S
h₃ : ∀ (n : ℕ), ∀ z ∈ S, ‖term f z n‖ ≤ ‖term f (↑x) n‖
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Tactic:
have H := hasSum_deriv_of_summable_norm h₀ h₁ h₂ h₃ hys

Result:
case intro.intro.intro.intro
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n => ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x => term f x n) S
h₂ : IsOpen S
h₃ : ∀ (n : ℕ), ∀ z ∈ S, ‖term f z n‖ ≤ ‖term f (↑x) n‖
H : HasSum (fun i => deriv (fun x => term f x i) s) (deriv (fun w => ∑' (i : ℕ), term f w i) s)
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Proof state:
case intro.intro.intro.intro
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n => ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x => term f x n) S
h₂ : IsOpen S
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Tactic:
have h₃ (n z) (hz : z ∈ S) : ‖term f z n‖ ≤ ‖term f x n‖ :=
  norm_term_le_of_re_le_re f (by simpa using (hxy.trans hz).le) n

Result:
case intro.intro.intro.intro
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n => ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x => term f x n) S
h₂ : IsOpen S
h₃ : ∀ (n : ℕ), ∀ z ∈ S, ‖term f z n‖ ≤ ‖term f (↑x) n‖
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Proof state:
case intro.intro.intro.intro
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n => ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x => term f x n) S
h₂ : IsOpen S
h₃ : ∀ (n : ℕ), ∀ z ∈ S, ‖term f z n‖ ≤ ‖term f (↑x) n‖
H : HasSum (fun i => -term (logMul f) s i) (deriv (fun w => ∑' (i : ℕ), term f w i) s)
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Tactic:
refine ⟨summable_neg_iff.mp H.summable, ?_⟩

Result:
case intro.intro.intro.intro
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n => ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x => term f x n) S
h₂ : IsOpen S
h₃ : ∀ (n : ℕ), ∀ z ∈ S, ‖term f z n‖ ≤ ‖term f (↑x) n‖
H : HasSum (fun i => -term (logMul f) s i) (deriv (fun w => ∑' (i : ℕ), term f w i) s)
⊢ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Proof state:
case intro.intro.intro.intro
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Tactic:
let S : Set ℂ := {z | y < z.re}

Result:
case intro.intro.intro.intro
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Proof state:
case intro.intro
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Tactic:
obtain ⟨y, hxy, hys⟩ := exists_between hxs

Result:
case intro.intro.intro.intro
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s