awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
n : ℕ
s : ℂ
hn : n ≠ 0
⊢ HasDerivAt (fun (z : ℂ) ↦ f n * HPow.hPow (α := ℂ) (↑n : ℂ) (-z))
    (f n * (-log (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) (-s))) s

Tactic:
exact HasDerivAt.const_mul (f n) (by simpa only [mul_comm, ← mul_neg_one (log n), ← mul_assoc]
    using (hasDerivAt_neg' s).const_cpow (Or.inl <| Nat.cast_ne_zero.mpr hn))

Premises used: HasDerivAt.const_mul
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
obtain :
  ∀ (x : ℝ) (hxs : x < s.re) (hf : LSeriesSummable f (↑x : ℂ)),
    LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
⊢ 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

Premises used: LSeriesSummable_lt_re_of_abscissaOfAbsConv_lt_re
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f (↑x : ℂ)
obtain :
  ∀ (y : ℝ) (hxy : x < y) (hys : y < s.re),
    LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

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

Premises used: exists_between
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f (↑x : ℂ)
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z : ℂ | y < z.re}
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖term f (↑x : ℂ) n‖

Tactic:
have h₀ : Summable (fun n ↦ ‖term f x n‖) := summable_norm_iff.mpr hf
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
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‖
⊢ ∀ (n : ℕ), DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ term f x n) S

Tactic:
have h₁ (n) : DifferentiableOn ℂ (term f · n) S :=
    fun z _ ↦ (hasDerivAt_term f n _).differentiableAt.differentiableWithinAt
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
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 ℂ (F := ℂ) (fun (x : ℂ) ↦ term f x n) S
⊢ IsOpen S

Tactic:
have h₂ : IsOpen S := isOpen_lt continuous_const continuous_re
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
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 ℂ (F := ℂ) (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

Premises used: LT.lt.le, LT.lt.trans
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
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 ℂ (F := ℂ) (fun (x : ℂ) ↦ term f x n) S
h₂ : IsOpen S
⊢ ∀ (n : ℕ) (z : ℂ) (hz : z ∈ S), ‖term f z n‖ ≤ ‖term f (↑x : ℂ) n‖

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
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
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 ℂ (F := ℂ) (fun (x : ℂ) ↦ term f x n) S
h₂ : IsOpen S
h₃ : ∀ (n : ℕ) (z : ℂ) (hz : z ∈ S), ‖term f z n‖ ≤ ‖term f (↑x : ℂ) n‖
⊢ HasSum (α := ℂ) (fun (i : ℕ) ↦ deriv (fun (x : ℂ) ↦ term f x i) s) (deriv (fun (w : ℂ) ↦ ∑' (i : ℕ), term f w i) s)

Tactic:
have H := hasSum_deriv_of_summable_norm h₀ h₁ h₂ h₃ hys
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
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 ℂ (F := ℂ) (fun (x : ℂ) ↦ term f x n) S
h₂ : IsOpen S
h₃ : ∀ (n : ℕ) (z : ℂ) (hz : 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)
⊢ HasSum (α := ℂ) (fun (i : ℕ) ↦ -term (logMul f) s i) (deriv (fun (w : ℂ) ↦ ∑' (i : ℕ), term f w i) s)

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

Premises used: HasDerivAt.deriv, LSeries.hasDerivAt_term
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
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 ℂ (F := ℂ) (fun (x : ℂ) ↦ term f x n) S
h₂ : IsOpen S
h₃ : ∀ (n : ℕ) (z : ℂ) (hz : 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:
⟨summable_neg_iff.mp H.summable, ?_⟩

Premises used: HasSum.summable, And.intro, Iff.mp, summable_neg_iff
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
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 ℂ (F := ℂ) (fun (x : ℂ) ↦ term f x n) S
h₂ : IsOpen S
h₃ : ∀ (n : ℕ) (z : ℂ) (hz : 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)
refine : HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Tactic:
refine ⟨summable_neg_iff.mp H.summable, ?_⟩
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
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 ℂ (F := ℂ) (fun (x : ℂ) ↦ term f x n) S
h₂ : IsOpen S
h₃ : ∀ (n : ℕ) (z : ℂ) (hz : 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

Premises used: DifferentiableAt.hasDerivAt, DifferentiableOn.differentiableAt, HasSum.tsum_eq, tsum_neg, IsOpen.mem_nhds, Complex.differentiableOn_tsum_of_summable_norm
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
⊢ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Tactic:
(LSeriesSummable_logMul_and_hasDerivAt h).2

Premises used: And.right, _private.0.LSeries.LSeriesSummable_logMul_and_hasDerivAt
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
⊢ deriv (LSeries f) s = -LSeries (logMul f) s

Tactic:
(LSeries_hasDerivAt h).deriv

Premises used: HasDerivAt.deriv, LSeries_hasDerivAt
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
⊢ Set.EqOn (deriv (LSeries f)) (-LSeries (logMul f)) {s : ℂ | abscissaOfAbsConv f < (↑s.re : EReal)}

Tactic:
deriv_eqOn (isOpen_re_gt_EReal _) fun _ hs ↦ (LSeries_hasDerivAt hs).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, deriv_eqOn, LSeries_hasDerivAt, Complex.isOpen_re_gt_EReal
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
⊢ LSeriesSummable (logMul f) s

Tactic:
(LSeriesSummable_logMul_and_hasDerivAt h).1

Premises used: And.left, _private.0.LSeries.LSeriesSummable_logMul_and_hasDerivAt
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
a : abscissaOfAbsConv (logMul f) ≤ abscissaOfAbsConv f
a₁ : abscissaOfAbsConv f ≤ abscissaOfAbsConv (logMul f)
⊢ abscissaOfAbsConv (logMul f) = abscissaOfAbsConv f

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
⊢ abscissaOfAbsConv (logMul f) ≤ abscissaOfAbsConv f

Tactic:
abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' fun s hs ↦ ?_

Premises used: LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable'
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
a : ∀ (s : ℝ) (hs : abscissaOfAbsConv f < (↑s : EReal)), LSeriesSummable (logMul f) (↑s : ℂ)
⊢ abscissaOfAbsConv (logMul f) ≤ abscissaOfAbsConv f

Tactic:
refine abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' fun s hs ↦ ?_

Premises used: LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable'
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
⊢ abscissaOfAbsConv f ≤ abscissaOfAbsConv (logMul f)

Tactic:
abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' fun s hs ↦ ?_

Premises used: LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable'
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
a : ∀ (s : ℝ) (hs : abscissaOfAbsConv (logMul f) < (↑s : EReal)), LSeriesSummable f (↑s : ℂ)
⊢ abscissaOfAbsConv f ≤ abscissaOfAbsConv (logMul f)

Tactic:
refine abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' fun s hs ↦ ?_

Premises used: LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable'
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv f < (↑s : EReal)
⊢ abscissaOfAbsConv f < (↑(↑s : ℂ).re : EReal)

Tactic:
simp [hs]
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv f < (↑s : EReal)
⊢ LSeriesSummable (logMul f) (↑s : ℂ)

Tactic:
exact LSeriesSummable_logMul_of_lt_re <| by simp [hs]

Premises used: LSeriesSummable_logMul_of_lt_re
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < (↑s : EReal)
⊢ abscissaOfAbsConv (logMul f) < (↑(↑s : ℂ).re : EReal)

Tactic:
simp [hs]
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < (↑s : EReal)
a : ∀ᶠ (i : ℕ) in Filter.atTop, ‖term f (↑s : ℂ) i‖ ≤ (fun (n : ℕ) ↦ ‖term (logMul f) (↑s : ℂ) n‖) i
⊢ LSeriesSummable f (↑s : ℂ)

Tactic:
refine (LSeriesSummable_of_abscissaOfAbsConv_lt_re <| by simp [hs])
      |>.norm.of_norm_bounded_eventually_nat (g := fun n ↦ ‖term (logMul f) s n‖) ?_

Premises used: LSeriesSummable_of_abscissaOfAbsConv_lt_re, Summable.norm, Summable.of_norm_bounded_eventually_nat
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < (↑s : EReal)
h : ∀ (n : ℕ) (hn : max 1 ⌈Real.exp 1⌉₊ ≤ n), ‖term f (↑s : ℂ) n‖ ≤ ‖term (logMul f) (↑s : ℂ) n‖
⊢ ∀ᶠ (i : ℕ) in Filter.atTop, ‖term f (↑s : ℂ) i‖ ≤ (fun (n : ℕ) ↦ ‖term (logMul f) (↑s : ℂ) n‖) i

Tactic:
filter_upwards [Filter.eventually_ge_atTop <| max 1 (Nat.ceil (Real.exp 1))] with n hn

Premises used: Real.exp, Max.max, Nat.ceil, Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < (↑s : EReal)
n : ℕ
hn : max 1 ⌈Real.exp 1⌉₊ ≤ n
⊢ n ≠ 0

Tactic:
omega
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < (↑s : EReal)
n : ℕ
hn : max 1 ⌈Real.exp 1⌉₊ ≤ n
h : ‖f n / HPow.hPow (α := ℂ) (↑n : ℂ) (↑s : ℂ)‖ ≤ ‖Real.log (↑n : ℝ)‖ * ‖f n / HPow.hPow (α := ℂ) (↑n : ℂ) (↑s : ℂ)‖
⊢ ‖term f (↑s : ℂ) n‖ ≤ ‖term (logMul f) (↑s : ℂ) n‖

Tactic:
simp only [term_of_ne_zero (show n ≠ 0 by omega), logMul, norm_mul, mul_div_assoc,
      ← natCast_log, norm_real]

Premises used: mul_div_assoc, Complex.natCast_log, LSeries.term_of_ne_zero, norm_mul, Complex.norm_real, LSeries.logMul
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < (↑s : EReal)
n : ℕ
hn : max 1 ⌈Real.exp 1⌉₊ ≤ n
⊢ ‖f n / HPow.hPow (α := ℂ) (↑n : ℂ) (↑s : ℂ)‖ ≤ ‖Real.log (↑n : ℝ)‖ * ‖f n / HPow.hPow (α := ℂ) (↑n : ℂ) (↑s : ℂ)‖

Tactic:
le_mul_of_one_le_left (norm_nonneg _) (.trans ?_ <| Real.le_norm_self _)

Premises used: le_mul_of_one_le_left, Real.le_norm_self, LE.le.trans, norm_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < (↑s : EReal)
n : ℕ
hn : max 1 ⌈Real.exp 1⌉₊ ≤ n
h : 1 ≤ Real.log (↑n : ℝ)
⊢ ‖f n / HPow.hPow (α := ℂ) (↑n : ℂ) (↑s : ℂ)‖ ≤ ‖Real.log (↑n : ℝ)‖ * ‖f n / HPow.hPow (α := ℂ) (↑n : ℂ) (↑s : ℂ)‖

Tactic:
refine le_mul_of_one_le_left (norm_nonneg _) (.trans ?_ <| Real.le_norm_self _)

Premises used: le_mul_of_one_le_left, Real.le_norm_self, LE.le.trans, norm_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < (↑s : EReal)
n : ℕ
hn : max 1 ⌈Real.exp 1⌉₊ ≤ n
⊢ 1 ≤ Real.log (↑n : ℝ)

Tactic:
simpa using Real.log_le_log (Real.exp_pos 1) <| Nat.ceil_le.mp <| (le_max_right _ _).trans hn

Premises used: le_max_right, Real.log_le_log, Iff.mp, LE.le.trans, OfNat.ofNat, Nat.ceil_le, Real.exp_pos
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
⊢ abscissaOfAbsConv (logMul^[0] f) = abscissaOfAbsConv f

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
n : ℕ
ih : abscissaOfAbsConv (logMul^[n] f) = abscissaOfAbsConv f
⊢ abscissaOfAbsConv (logMul^[n + 1] f) = abscissaOfAbsConv f

Tactic:
simp [ih, Function.iterate_succ', Function.comp_def,
      -Function.comp_apply, -Function.iterate_succ]

Premises used: Function.iterate_succ, Function.iterate_succ', Function.comp_def, Function.comp_apply
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
m : ℕ
zero : abscissaOfAbsConv (logMul^[0] f) = abscissaOfAbsConv f
succ :
  ∀ (n : ℕ) (ih : abscissaOfAbsConv (logMul^[n] f) = abscissaOfAbsConv f),
    abscissaOfAbsConv (logMul^[n + 1] f) = abscissaOfAbsConv f
⊢ abscissaOfAbsConv (logMul^[m] f) = abscissaOfAbsConv f

Tactic:
induction m with
  | zero => simp
  | succ n ih => simp [ih, Function.iterate_succ', Function.comp_def,
      -Function.comp_apply, -Function.iterate_succ]

Premises used: Function.iterate_succ, Function.iterate_succ', Function.comp_def, Function.comp_apply
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
⊢ iteratedDeriv 0 (LSeries f) s = HPow.hPow (α := ℂ) (β := ℕ) (-1) 0 * LSeries (logMul^[0] f) s

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
m : ℕ
ih :
  ∀ {s : ℂ} (h : abscissaOfAbsConv f < (↑s.re : EReal)),
    iteratedDeriv m (LSeries f) s = HPow.hPow (α := ℂ) (-1) m * LSeries (logMul^[m] f) s
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
⊢ Set.EqOn (iteratedDeriv m (LSeries f)) (HPow.hPow (α := ℂ → ℂ) (-1) m * LSeries (logMul^[m] f))
    {s : ℂ | abscissaOfAbsConv f < (↑s.re : EReal)}

Tactic:
have ih' : {s | abscissaOfAbsConv f < re s}.EqOn (iteratedDeriv m (LSeries f))
        ((-1) ^ m * LSeries (logMul^[m] f)) := fun _ hs ↦ ih hs
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
m : ℕ
ih :
  ∀ {s : ℂ} (h : abscissaOfAbsConv f < (↑s.re : EReal)),
    iteratedDeriv m (LSeries f) s = HPow.hPow (α := ℂ) (-1) m * LSeries (logMul^[m] f) s
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
ih' :
  Set.EqOn (iteratedDeriv m (LSeries f)) (HPow.hPow (α := ℂ → ℂ) (-1) m * LSeries (logMul^[m] f))
    {s : ℂ | abscissaOfAbsConv f < (↑s.re : EReal)}
⊢ derivWithin (iteratedDeriv m (LSeries f)) {s : ℂ | abscissaOfAbsConv f < (↑s.re : EReal)} s =
    derivWithin (HPow.hPow (α := ℂ → ℂ) (-1) m * LSeries (logMul^[m] f)) {s : ℂ | abscissaOfAbsConv f < (↑s.re : EReal)}
      s

Tactic:
have := derivWithin_congr ih' (ih h)
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
m : ℕ
ih :
  ∀ {s : ℂ} (h : abscissaOfAbsConv f < (↑s.re : EReal)),
    iteratedDeriv m (LSeries f) s = HPow.hPow (α := ℂ) (-1) m * LSeries (logMul^[m] f) s
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
ih' :
  Set.EqOn (iteratedDeriv m (LSeries f)) (HPow.hPow (α := ℂ → ℂ) (-1) m * LSeries (logMul^[m] f))
    {s : ℂ | abscissaOfAbsConv f < (↑s.re : EReal)}
this :
  derivWithin (iteratedDeriv m (LSeries f)) {s : ℂ | abscissaOfAbsConv f < (↑s.re : EReal)} s =
    derivWithin (HPow.hPow (α := ℂ → ℂ) (-1) m * LSeries (logMul^[m] f)) {s : ℂ | abscissaOfAbsConv f < (↑s.re : EReal)}
      s
⊢ deriv (iteratedDeriv m (LSeries f)) s = deriv (HPow.hPow (α := ℂ → ℂ) (-1) m * LSeries (logMul^[m] f)) s

Tactic:
simp_rw [derivWithin_of_isOpen (isOpen_re_gt_EReal _) h] at this

Premises used: derivWithin_of_isOpen, Complex.isOpen_re_gt_EReal
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
m : ℕ
ih :
  ∀ {s : ℂ} (h : abscissaOfAbsConv f < (↑s.re : EReal)),
    iteratedDeriv m (LSeries f) s = HPow.hPow (α := ℂ) (-1) m * LSeries (logMul^[m] f) s
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
ih' :
  Set.EqOn (iteratedDeriv m (LSeries f)) (HPow.hPow (α := ℂ → ℂ) (-1) m * LSeries (logMul^[m] f))
    {s : ℂ | abscissaOfAbsConv f < (↑s.re : EReal)}
this : deriv (iteratedDeriv m (LSeries f)) s = deriv (HPow.hPow (α := ℂ → ℂ) (-1) m * LSeries (logMul^[m] f)) s
succ :
  deriv (HPow.hPow (α := ℂ → ℂ) (-1) m * LSeries (logMul^[m] f)) s =
    HPow.hPow (α := ℂ) (-1) (m + 1) * LSeries (logMul^[m + 1] f) s
⊢ iteratedDeriv (m + 1) (LSeries f) s = HPow.hPow (α := ℂ) (-1) (m + 1) * LSeries (logMul^[m + 1] f) s

Tactic:
rw [iteratedDeriv_succ, this]

Premises used: iteratedDeriv_succ
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
m : ℕ
ih :
  ∀ {s : ℂ} (h : abscissaOfAbsConv f < (↑s.re : EReal)),
    iteratedDeriv m (LSeries f) s = HPow.hPow (α := ℂ) (-1) m * LSeries (logMul^[m] f) s
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
ih' :
  Set.EqOn (iteratedDeriv m (LSeries f)) (HPow.hPow (α := ℂ → ℂ) (-1) m * LSeries (logMul^[m] f))
    {s : ℂ | abscissaOfAbsConv f < (↑s.re : EReal)}
this : deriv (iteratedDeriv m (LSeries f)) s = deriv (HPow.hPow (α := ℂ → ℂ) (-1) m * LSeries (logMul^[m] f)) s
⊢ deriv (HPow.hPow (α := ℂ → ℂ) (-1) m * LSeries (logMul^[m] f)) s =
    HPow.hPow (α := ℂ) (-1) (m + 1) * LSeries (logMul^[m + 1] f) s

Tactic:
simp [Pi.mul_def, pow_succ, Function.iterate_succ',
      LSeries_deriv <| absicssaOfAbsConv_logPowMul.symm ▸ h, -Function.iterate_succ]

Premises used: Function.iterate_succ, pow_succ, Function.iterate_succ', LSeries_deriv, Pi.mul_def
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
m : ℕ
s : ℂ
h : abscissaOfAbsConv f < (↑s.re : EReal)
zero :
  ∀ {s : ℂ} (h : abscissaOfAbsConv f < (↑s.re : EReal)),
    iteratedDeriv 0 (LSeries f) s = HPow.hPow (α := ℂ) (β := ℕ) (-1) 0 * LSeries (logMul^[0] f) s
succ :
  ∀ (m : ℕ)
    (ih :
      ∀ {s : ℂ} (h : abscissaOfAbsConv f < (↑s.re : EReal)),
        iteratedDeriv m (LSeries f) s = HPow.hPow (α := ℂ) (-1) m * LSeries (logMul^[m] f) s)
    {s : ℂ} (h : abscissaOfAbsConv f < (↑s.re : EReal)),
    iteratedDeriv (m + 1) (LSeries f) s = HPow.hPow (α := ℂ) (-1) (m + 1) * LSeries (logMul^[m + 1] f) s
⊢ iteratedDeriv m (LSeries f) s = HPow.hPow (α := ℂ) (-1) m * LSeries (logMul^[m] f) s

Tactic:
induction m generalizing s with
  | zero => simp
  | succ m ih =>
    have ih' : {s | abscissaOfAbsConv f < re s}.EqOn (iteratedDeriv m (LSeries f))
        ((-1) ^ m * LSeries (logMul^[m] f)) := fun _ hs ↦ ih hs
    have := derivWithin_congr ih' (ih h)
    simp_rw [derivWithin_of_isOpen (isOpen_re_gt_EReal _) h] at this
    rw [iteratedDeriv_succ, this]
    simp [Pi.mul_def, pow_succ, Function.iterate_succ',
      LSeries_deriv <| absicssaOfAbsConv_logPowMul.symm ▸ h, -Function.iterate_succ]

Premises used: iteratedDeriv_succ, Function.iterate_succ, pow_succ, Function.iterate_succ', LSeries_deriv, Pi.mul_def, derivWithin_of_isOpen, Complex.isOpen_re_gt_EReal
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
⊢ DifferentiableOn ℂ (LSeries f) {s : ℂ | abscissaOfAbsConv f < (↑s.re : EReal)}

Tactic:
fun _ hz ↦ (LSeries_hasDerivAt hz).differentiableAt.differentiableWithinAt

Premises used: HasDerivAt.differentiableAt, DifferentiableAt.differentiableWithinAt, DifferentiableOn, LSeries_hasDerivAt
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
⊢ AnalyticOnNhd ℂ (LSeries f) {s : ℂ | abscissaOfAbsConv f < (↑s.re : EReal)}

Tactic:
(LSeries_differentiableOn f).analyticOnNhd <| isOpen_re_gt_EReal _

Premises used: LSeries_differentiableOn, DifferentiableOn.analyticOnNhd, Complex.isOpen_re_gt_EReal
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
⊢ AnalyticOn ℂ (LSeries f) {s : ℂ | abscissaOfAbsConv f < (↑s.re : EReal)}

Tactic:
(LSeries_analyticOnNhd f).analyticOn

Premises used: LSeries_analyticOnNhd, AnalyticOnNhd.analyticOn
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
h : ∀ (x : ℕ), (1 : (a : ℕ) → ℂ) x = δ x
⊢ (fun (n : ℕ) ↦ (1 : (a : ℕ) → ℂ) n) = δ

Tactic:
ext
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
x : ℕ
⊢ (1 : (a : ℕ) → ℂ) x = δ x

Tactic:
simp [one_apply, LSeries.delta]

Premises used: LSeries.delta, ArithmeticFunction.one_apply
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
⊢ ¬LSeriesSummable (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) 1

Tactic:
fun h ↦ not_summable_one_div_on_primes <| summable_ofReal.mp <| .of_neg ?_

Premises used: Complex.summable_ofReal, Iff.mp, not_summable_one_div_on_primes, Summable.of_neg, Not
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
refine :
  ∀ (h : LSeriesSummable (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) 1),
    Summable (α := ℂ) fun (b : ℕ) ↦
      -(↑(Set.indicator {p : ℕ | Nat.Prime p} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) b) : ℂ)
⊢ ¬LSeriesSummable (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) 1

Tactic:
refine fun h ↦ not_summable_one_div_on_primes <| summable_ofReal.mp <| .of_neg ?_

Premises used: Complex.summable_ofReal, Iff.mp, not_summable_one_div_on_primes, Summable.of_neg
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
h : LSeriesSummable (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) 1
⊢ Summable (α := ℂ) fun (b : ℕ) ↦
    -(↑(Set.indicator {p : ℕ | Nat.Prime p} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) b) : ℂ)

Tactic:
(h.indicator {n | n.Prime}).congr fun n ↦ ?_

Premises used: Nat.Prime, setOf, Summable.congr, Summable.indicator
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
h : LSeriesSummable (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) 1
refine :
  ∀ (n : ℕ),
    Set.indicator {n : ℕ | Nat.Prime n} (term (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) 1) n =
      -(↑(Set.indicator {p : ℕ | Nat.Prime p} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) n) : ℂ)
⊢ Summable (α := ℂ) fun (b : ℕ) ↦
    -(↑(Set.indicator {p : ℕ | Nat.Prime p} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) b) : ℂ)

Tactic:
refine (h.indicator {n | n.Prime}).congr fun n ↦ ?_

Premises used: Nat.Prime, setOf, Summable.congr, Summable.indicator