awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
hf : f 0 = 0
s : ℂ
n : ℕ
pos : ∀ (h : n = 0), 0 = f n * HPow.hPow (α := ℂ) (↑n : ℂ) (-s)
neg : ∀ (h : ¬n = 0), f n / HPow.hPow (α := ℂ) (↑n : ℂ) s = f n * HPow.hPow (α := ℂ) (↑n : ℂ) (-s)
⊢ (if n = 0 then 0 else f n / HPow.hPow (α := ℂ) (↑n : ℂ) s) = f n * HPow.hPow (α := ℂ) (↑n : ℂ) (-s)

Tactic:
split_ifs with h
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
hf : f 0 = 0
s : ℂ
n : ℕ
h : n = 0
⊢ 0 = f n * HPow.hPow (α := ℂ) (↑n : ℂ) (-s)

Tactic:
simp [h, hf, cpow_neg, div_eq_inv_mul, mul_comm]

Premises used: Complex.cpow_neg, mul_comm, div_eq_inv_mul
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
hf : f 0 = 0
s : ℂ
n : ℕ
h : ¬n = 0
⊢ f n / HPow.hPow (α := ℂ) (↑n : ℂ) s = f n * HPow.hPow (α := ℂ) (↑n : ℂ) (-s)

Tactic:
simp [h, hf, cpow_neg, div_eq_inv_mul, mul_comm]

Premises used: Complex.cpow_neg, mul_comm, div_eq_inv_mul
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s : ℂ
⊢ term f s 0 = 0

Tactic:
rfl

Premises used: LSeries.term, rfl, ite
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
n : ℕ
hn : n ≠ 0
f : ℕ → ℂ
s : ℂ
⊢ term f s n = f n / HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
if_neg hn

Premises used: LSeries.term, if_neg
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
n : ℕ
inl : term f s 0 = f 0 / HPow.hPow (α := ℂ) (↑0 : ℂ) s
inr : ∀ (hn : n ≠ 0), term f s n = f n / HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ term f s n = f n / HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
inl : 0 = f 0 / HPow.hPow (α := ℂ) (↑0 : ℂ) s
inl₁ : 0 = f 0 / HPow.hPow (α := ℂ) 0 s
inl₂ : 0 = f 0 / 0
inl₃ inl₄ : Eq (α := ℂ) 0 0
⊢ term f s 0 = f 0 / HPow.hPow (α := ℂ) (↑0 : ℂ) s

Tactic:
rw [term_zero, Nat.cast_zero, zero_cpow hs, div_zero]

Premises used: Complex.zero_cpow, Nat.cast_zero, div_zero, LSeries.term_zero
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
n : ℕ
hn : n ≠ 0
inr inr₁ : f n / HPow.hPow (α := ℂ) (↑n : ℂ) s = f n / HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ term f s n = f n / HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
rw [term_of_ne_zero hn]

Premises used: LSeries.term_of_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
h : ∀ {n : ℕ}, n ≠ 0 → f n = g n
s : ℂ
n : ℕ
inl : ∀ (hn : n = 0), term f s n = term g s n
inr : ∀ (hn : n ≠ 0), term f s n = term g s n
⊢ term f s n = term g s n

Tactic:
rcases eq_or_ne n 0 with hn | hn

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
h : ∀ {n : ℕ}, n ≠ 0 → f n = g n
s : ℂ
n : ℕ
hn : n = 0
⊢ term f s n = term g s n

Tactic:
simp [hn, h]
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
h : ∀ {n : ℕ}, n ≠ 0 → f n = g n
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term f s n = term g s n

Tactic:
simp [hn, h]
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s : ℂ
n : ℕ
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ s * term f s (n + 1) = f (n + 1)

Tactic:
simp [term, natCast_add_one_cpow_ne_zero n _, mul_div_assoc']

Premises used: Complex.natCast_add_one_cpow_ne_zero, mul_div_assoc', LSeries.term
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s : ℂ
n : ℕ
inl : ‖term f s 0‖ = if Eq (α := ℕ) 0 0 then 0 else ‖f 0‖ / HPow.hPow (α := ℝ) (↑0 : ℝ) s.re
inr : ∀ (hn : n ≠ 0), ‖term f s n‖ = if n = 0 then 0 else ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ ‖term f s n‖ = if n = 0 then 0 else ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s : ℂ
⊢ ‖term f s 0‖ = if Eq (α := ℕ) 0 0 then 0 else ‖f 0‖ / HPow.hPow (α := ℝ) (↑0 : ℝ) s.re

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ‖term f s n‖ = if n = 0 then 0 else ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re

Tactic:
simp [hn, norm_natCast_cpow_of_pos <| Nat.pos_of_ne_zero hn]

Premises used: Complex.norm_natCast_cpow_of_pos, Nat.pos_of_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
h : ‖f n‖ ≤ ‖g n‖
simp :
  (if n = 0 then 0 else ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re) ≤
    if n = 0 then 0 else ‖g n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ ‖term f s n‖ ≤ ‖term g s n‖

Tactic:
simp only [norm_term_eq]

Premises used: LSeries.norm_term_eq
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
h : ‖f n‖ ≤ ‖g n‖
isTrue : n = 0 → LE.le (α := ℝ) 0 0
isFalse : ¬n = 0 → ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re ≤ ‖g n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ (if n = 0 then 0 else ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re) ≤
    if n = 0 then 0 else ‖g n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re

Tactic:
split
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
h : ‖f n‖ ≤ ‖g n‖
h_1 : n = 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
h : ‖f n‖ ≤ ‖g n‖
h_1 : ¬n = 0
isFalse : 0 ≤ HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re ≤ ‖g n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
simp :
  (if n = 0 then 0 else ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s'.re) ≤
    if n = 0 then 0 else ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ ‖term f s' n‖ ≤ ‖term f s n‖

Tactic:
simp only [norm_term_eq]

Premises used: LSeries.norm_term_eq
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
split : n = 0 → LE.le (α := ℝ) 0 0
isFalse : ¬n = 0 → ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s'.re ≤ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ (if n = 0 then 0 else ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s'.re) ≤
    if n = 0 then 0 else ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re

Tactic:
split
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
h_1 : n = 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
h_1 : n = 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
next => rfl
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
hn : ¬n = 0
hdb : LE.le (α := ℝ) 1 (↑n : ℝ)
⊢ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s'.re ≤ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
hn : ¬n = 0
⊢ LE.le (α := ℝ) 1 (↑n : ℝ)

Tactic:
Nat.one_le_cast.mpr <| Nat.one_le_iff_ne_zero.mpr hn

Premises used: Iff.mpr, Nat.one_le_cast, Nat.one_le_iff_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
hn : ¬n = 0
⊢ LE.le (α := ℝ) 1 (↑n : ℝ)

Tactic:
exact Nat.one_le_cast.mpr <| Nat.one_le_iff_ne_zero.mpr hn

Premises used: Iff.mpr, Nat.one_le_cast, Nat.one_le_iff_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
a : ℕ → ℂ
n : ℕ
h : 0 ≤ a n
x : ℝ
pos : ∀ (hn : n = 0), LE.le (α := ℂ) 0 0
neg : ∀ (hn : ¬n = 0), 0 ≤ a n / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ)
⊢ 0 ≤ if n = 0 then 0 else a n / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ)

Tactic:
split_ifs with hn
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
a : ℕ → ℂ
n : ℕ
h : 0 ≤ a n
x : ℝ
hn : n = 0
⊢ LE.le (α := ℂ) 0 0

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
a : ℕ → ℂ
n : ℕ
h : 0 ≤ a n
x : ℝ
hn : ¬n = 0
⊢ 0 ≤ a n / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ)

Tactic:
mul_nonneg h (inv_natCast_cpow_ofReal_pos hn x).le

Premises used: mul_nonneg, LT.lt.le, Complex.inv_natCast_cpow_ofReal_pos
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
a : ℕ → ℂ
n : ℕ
h : 0 ≤ a n
x : ℝ
hn : n = 0
⊢ LE.le (α := ℂ) 0 0

Tactic:
exacts [le_rfl, mul_nonneg h (inv_natCast_cpow_ofReal_pos hn x).le]

Premises used: le_rfl
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
a : ℕ → ℂ
n : ℕ
hn : n ≠ 0
h : 0 < a n
x : ℝ
⊢ 0 < term a (↑x : ℂ) n

Tactic:
simpa only [term_of_ne_zero hn] using mul_pos h <| inv_natCast_cpow_ofReal_pos hn x

Premises used: LSeries.term_of_ne_zero, Complex.inv_natCast_cpow_ofReal_pos, mul_pos
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
h : ∀ {n : ℕ}, n ≠ 0 → f n = g n
s : ℂ
⊢ LSeries f s = LSeries g s

Tactic:
tsum_congr <| term_congr h s

Premises used: LSeries.term_congr, tsum_congr, LSeries
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
s : ℂ
h : ∀ {n : ℕ}, n ≠ 0 → f n = g n
⊢ LSeriesSummable f s ↔ LSeriesSummable g s

Tactic:
summable_congr <| term_congr h s

Premises used: LSeries.term_congr, summable_congr, LSeriesSummable
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[atTop] g
hf : LSeriesSummable f s
⊢ f =ᶠ[cofinite] g

Tactic:
rw [← Nat.cofinite_eq_atTop] at h

Premises used: Nat.cofinite_eq_atTop
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[atTop] g
hf : LSeriesSummable f s
h₁ : f =ᶠ[cofinite] g
⊢ LSeriesSummable f s

Tactic:
rw [← Nat.cofinite_eq_atTop] at h

Premises used: Nat.cofinite_eq_atTop
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
⊢ LSeriesSummable g s

Tactic:
(summable_norm_iff.mpr hf).of_norm_bounded_eventually ?_

Premises used: Iff.mpr, summable_norm_iff, Summable.of_norm_bounded_eventually, LSeriesSummable
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
refine : ∀ᶠ (i : ℕ) in cofinite, ‖term g s i‖ ≤ ‖term f s i‖
⊢ LSeriesSummable g s

Tactic:
refine (summable_norm_iff.mpr hf).of_norm_bounded_eventually ?_

Premises used: Iff.mpr, summable_norm_iff, Summable.of_norm_bounded_eventually
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
rw :
  ∀ (h : ∃ (s : Set ℕ), Membership.mem (γ := Filter ℕ) cofinite s ∧ Set.EqOn f g s) (hf : LSeriesSummable f s),
    ∃ (s_1 : Set ℕ), Membership.mem (γ := Filter ℕ) cofinite s_1 ∧ Set.EqOn (term f s) (term g s) s_1
⊢ term f s =ᶠ[cofinite] term g s

Tactic:
rw [eventuallyEq_iff_exists_mem] at h ⊢

Premises used: Filter.eventuallyEq_iff_exists_mem
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
s : ℂ
h : ∃ (s : Set ℕ), Membership.mem (γ := Filter ℕ) cofinite s ∧ Set.EqOn f g s
hf : LSeriesSummable f s
obtain :
  ∀ (S : Set ℕ) (hS : Membership.mem (γ := Filter ℕ) cofinite S) (hS' : Set.EqOn f g S),
    ∃ (s_1 : Set ℕ), Membership.mem (γ := Filter ℕ) cofinite s_1 ∧ Set.EqOn (term f s) (term g s) s_1
⊢ ∃ (s_1 : Set ℕ), Membership.mem (γ := Filter ℕ) cofinite s_1 ∧ Set.EqOn (term f s) (term g s) s_1

Tactic:
obtain ⟨S, hS, hS'⟩ := h
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
S : Set ℕ
hS : Membership.mem (γ := Filter ℕ) cofinite S
hS' : Set.EqOn f g S
⊢ ∃ (s_1 : Set ℕ), Membership.mem (γ := Filter ℕ) cofinite s_1 ∧ Set.EqOn (term f s) (term g s) s_1

Tactic:
⟨S \ {0}, diff_mem hS <| (Set.finite_singleton 0).compl_mem_cofinite, fun n hn ↦ ?_⟩

Premises used: SDiff.sdiff, Filter.diff_mem, Set.Finite.compl_mem_cofinite, And.intro, Exists.intro, Singleton.singleton, OfNat.ofNat, Set.finite_singleton
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
S : Set ℕ
hS : Membership.mem (γ := Filter ℕ) cofinite S
hS' : Set.EqOn f g S
refine : ∀ (n : ℕ) (hn : n ∈ S \ {0}), term f s n = term g s n
⊢ ∃ (s_1 : Set ℕ), Membership.mem (γ := Filter ℕ) cofinite s_1 ∧ Set.EqOn (term f s) (term g s) s_1

Tactic:
refine ⟨S \ {0}, diff_mem hS <| (Set.finite_singleton 0).compl_mem_cofinite, fun n hn ↦ ?_⟩
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
S : Set ℕ
hS : Membership.mem (γ := Filter ℕ) cofinite S
hS' : Set.EqOn f g S
n : ℕ
hn : n ∈ S \ {0}
⊢ n ∈ S ∧ ¬n = 0

Tactic:
rw [Set.mem_diff, Set.mem_singleton_iff] at hn

Premises used: Set.mem_singleton_iff, Set.mem_diff
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
S : Set ℕ
hS : Membership.mem (γ := Filter ℕ) cofinite S
hS' : Set.EqOn f g S
n : ℕ
hn : n ∈ S ∧ ¬n = 0
⊢ term f s n = term g s n

Tactic:
simp [hn.2, hS' hn.1]

Premises used: And.right, And.left
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
⊢ term f s =ᶠ[cofinite] term g s

Tactic:
have : term f s =ᶠ[cofinite] term g s := by
    rw [eventuallyEq_iff_exists_mem] at h ⊢
    obtain ⟨S, hS, hS'⟩ := h
    refine ⟨S \ {0}, diff_mem hS <| (Set.finite_singleton 0).compl_mem_cofinite, fun n hn ↦ ?_⟩
    rw [Set.mem_diff, Set.mem_singleton_iff] at hn
    simp [hn.2, hS' hn.1]
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
this : term f s =ᶠ[cofinite] term g s
n : ℕ
hn : term g s n = term f s n
⊢ ‖term g s n‖ ≤ ‖term f s n‖

Tactic:
simp [hn]
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
this : term f s =ᶠ[cofinite] term g s
⊢ ∀ᶠ (i : ℕ) in cofinite, ‖term g s i‖ ≤ ‖term f s i‖

Tactic:
exact this.symm.mono fun n hn ↦ by simp [hn]

Premises used: Filter.Eventually.mono, Filter.EventuallyEq.symm
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[atTop] g
⊢ LSeriesSummable f s ↔ LSeriesSummable g s

Tactic:
⟨fun H ↦ H.congr' s h, fun H ↦ H.congr' s h.symm⟩

Premises used: LSeriesSummable.congr', Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s : ℂ
⊢ ¬LSeriesSummable f s → LSeries f s = 0

Tactic:
tsum_eq_zero_of_not_summable

Premises used: LSeries, tsum_eq_zero_of_not_summable, LSeriesSummable
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
s : ℂ
⊢ LSeriesSummable 0 s

Tactic:
simp [LSeriesSummable, funext (term_def 0 s), summable_zero]

Premises used: LSeries.term_def, funext, summable_zero, OfNat.ofNat, LSeriesSummable
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s a : ℂ
h : LSeriesHasSum f s a
⊢ _root_.LSeriesSummable f s

Tactic:
h.summable

Premises used: HasSum.summable, LSeriesSummable
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s a : ℂ
h : LSeriesHasSum f s a
⊢ LSeries f s = a

Tactic:
h.tsum_eq

Premises used: LSeries, HasSum.tsum_eq
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ _root_.LSeriesHasSum f s (LSeries f s)

Tactic:
h.hasSum

Premises used: LSeriesHasSum, LSeries, Summable.hasSum
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s a : ℂ
⊢ LSeriesHasSum f s a ↔ LSeriesSummable f s ∧ LSeries f s = a

Tactic:
⟨fun H ↦ ⟨H.LSeriesSummable, H.LSeries_eq⟩, fun ⟨H₁, H₂⟩ ↦ H₂ ▸ H₁.LSeriesHasSum⟩

Premises used: Eq.rec, LSeriesHasSum, LSeriesSummable.LSeriesHasSum, And.intro, Iff.intro, _private.0.LSeriesHasSum_iff.match_1, LSeriesHasSum.LSeriesSummable, LSeriesHasSum.LSeries_eq
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f g : ℕ → ℂ
s a : ℂ
h : ∀ {n : ℕ}, n ≠ 0 → f n = g n
⊢ LSeriesHasSum f s a ↔ LSeriesHasSum g s a

Tactic:
simp [LSeriesHasSum_iff, LSeriesSummable_congr s h, LSeries_congr h s]

Premises used: LSeries_congr, LSeriesSummable_congr, LSeriesHasSum_iff
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
hf : LSeriesSummable f s
rw : ∀ (hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term f s x‖), Summable (α := ℝ) fun (x : ℕ) ↦ ‖term f s' x‖
⊢ LSeriesSummable f s'

Tactic:
rw [LSeriesSummable, ← summable_norm_iff] at hf ⊢

Premises used: summable_norm_iff, LSeriesSummable
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term f s x‖
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ ‖term f s' x‖

Tactic:
hf.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (norm_term_le_of_re_le_re f h)

Premises used: Summable.of_nonneg_of_le, LSeries.term, norm_nonneg, LSeries.norm_term_le_of_re_le_re
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term f s x‖
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ ‖term f s' x‖

Tactic:
exact hf.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (norm_term_le_of_re_le_re f h)

Premises used: Summable.of_nonneg_of_le, norm_nonneg, LSeries.norm_term_le_of_re_le_re
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s s' : ℂ
h : s.re = s'.re
⊢ LSeriesSummable f s ↔ LSeriesSummable f s'

Tactic:
⟨fun H ↦ H.of_re_le_re h.le, fun H ↦ H.of_re_le_re h.symm.le⟩

Premises used: Eq.le, Iff.intro, LSeriesSummable.of_re_le_re, Eq.symm
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
h : ∀ (x : ℂ), LSeries 0 x = 0 x
⊢ LSeries 0 = 0

Tactic:
ext
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
x : ℂ
⊢ LSeries 0 x = 0 x

Tactic:
simp [LSeries, LSeries.term]

Premises used: LSeries, LSeries.term
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
s : ℂ
n : ℕ
inl : term δ s 0 = if Eq (α := ℕ) 0 1 then 1 else 0
inr : ∀ (hn : n ≠ 0), term δ s n = if n = 1 then 1 else 0
⊢ term δ s n = if n = 1 then 1 else 0

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
s : ℂ
⊢ term δ s 0 = if Eq (α := ℕ) 0 1 then 1 else 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
inr : ∀ (hn' : n = 1), term δ s n = if n = 1 then 1 else 0
inr₁ : ∀ (hn' : n ≠ 1), term δ s n = if n = 1 then 1 else 0
⊢ term δ s n = if n = 1 then 1 else 0

Tactic:
rcases eq_or_ne n 1 with hn' | hn'

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
hn' : n = 1
⊢ term δ s n = if n = 1 then 1 else 0

Tactic:
simp [hn, hn', delta]

Premises used: LSeries.delta
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
hn' : n ≠ 1
⊢ term δ s n = if n = 1 then 1 else 0

Tactic:
simp [hn, hn', delta]

Premises used: LSeries.delta
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
h : ∀ (n : ℕ), (f * δ) n = (f 1 • δ) n
⊢ f * δ = f 1 • δ

Tactic:
ext n
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
n : ℕ
pos : ∀ (hn : n = 1), (f * δ) n = (f 1 • δ) n
neg : ∀ (hn : ¬n = 1), (f * δ) n = (f 1 • δ) n
⊢ (f * δ) n = (f 1 • δ) n

Tactic:
by_cases hn : n = 1
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
n : ℕ
hn : n = 1
⊢ (f * δ) n = (f 1 • δ) n

Tactic:
simp [hn, delta]

Premises used: LSeries.delta
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
n : ℕ
hn : ¬n = 1
⊢ (f * δ) n = (f 1 • δ) n

Tactic:
simp [hn, delta]

Premises used: LSeries.delta
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
h : f 1 = 1
rw : f 1 • δ = δ
rw₁ : HSMul.hSMul (α := ℂ) 1 δ = δ
rw₂ rw₃ : δ = δ
⊢ f * δ = δ

Tactic:
rw [mul_delta_eq_smul_delta, h, one_smul]

Premises used: one_smul, LSeries.mul_delta_eq_smul_delta
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
⊢ δ * f = f 1 • δ

Tactic:
mul_comm δ f ▸ mul_delta_eq_smul_delta

Premises used: LSeries.delta, Eq.rec, LSeries.mul_delta_eq_smul_delta, mul_comm, Eq.symm
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
h : f 1 = 1
⊢ δ * f = δ

Tactic:
mul_comm δ f ▸ mul_delta h

Premises used: LSeries.delta, Eq.rec, LSeries.mul_delta, mul_comm, Eq.symm
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
h : ∀ (x : ℂ), L δ x = 1 x
⊢ L δ = 1

Tactic:
ext
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
x : ℂ
⊢ L δ x = 1 x

Tactic:
simp [LSeries, LSeries.term_delta]

Premises used: LSeries, LSeries.term_delta
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ ‖term f s x‖

Tactic:
replace h := h.norm
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s : ℂ
h : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term f s x‖
h₁ : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ (∑' (n : ℕ), ‖term f s n‖) * HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) s.re

Tactic:
use tsum fun n ↦ ‖term f s n‖

Premises used: Norm.norm, tsum, LSeries.term, SummationFilter.unconditional
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s : ℂ
h : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term f s x‖
h₁ : ∀ (n : ℕ) (hn₀ : n ≠ 0) (hn : (∑' (n : ℕ), ‖term f s n‖) * HPow.hPow (α := ℝ) (↑n : ℝ) s.re < ‖f n‖), False
⊢ ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ (∑' (n : ℕ), ‖term f s n‖) * HPow.hPow (α := ℝ) (↑n : ℝ) s.re

Tactic:
by_contra! ⟨n, hn₀, hn⟩
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s : ℂ
h : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term f s x‖
n : ℕ
hn₀ : n ≠ 0
hn : (∑' (n : ℕ), ‖term f s n‖) * HPow.hPow (α := ℝ) (↑n : ℝ) s.re < ‖f n‖
⊢ ‖term f s n‖ ≤ ∑' (i : ℕ), ‖term f s i‖

Tactic:
have := h.le_tsum n fun _ _ ↦ norm_nonneg _
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s : ℂ
h : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term f s x‖
n : ℕ
hn₀ : n ≠ 0
hn : (∑' (n : ℕ), ‖term f s n‖) * HPow.hPow (α := ℝ) (↑n : ℝ) s.re < ‖f n‖
this : ‖term f s n‖ ≤ ∑' (i : ℕ), ‖term f s i‖
⊢ ‖f n‖ ≤ (∑' (i : ℕ), ‖term f s i‖) * HPow.hPow (α := ℝ) (↑n : ℝ) s.re

Tactic:
rw [norm_term_eq, if_neg hn₀,
    div_le_iff₀ <| Real.rpow_pos_of_pos (Nat.cast_pos.mpr <| Nat.pos_of_ne_zero hn₀) _] at this

Premises used: Iff.mpr, div_le_iff₀, Real.rpow_pos_of_pos, Nat.cast_pos, LSeries.norm_term_eq, Nat.pos_of_ne_zero, if_neg
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s : ℂ
h : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term f s x‖
n : ℕ
hn₀ : n ≠ 0
hn : (∑' (n : ℕ), ‖term f s n‖) * HPow.hPow (α := ℝ) (↑n : ℝ) s.re < ‖f n‖
this : ‖f n‖ ≤ (∑' (i : ℕ), ‖term f s i‖) * HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ False

Tactic:
(this.trans_lt hn).false.elim

Premises used: False.elim, LT.lt.false, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s : ℂ
h : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term f s x‖
n : ℕ
hn₀ : n ≠ 0
hn : (∑' (n : ℕ), ‖term f s n‖) * HPow.hPow (α := ℝ) (↑n : ℝ) s.re < ‖f n‖
this : ‖f n‖ ≤ (∑' (i : ℕ), ‖term f s i‖) * HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ False

Tactic:
exact (this.trans_lt hn).false.elim

Premises used: False.elim, LT.lt.false, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
obtain :
  ∀ (C : ℝ) (hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) s.re),
    Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) s.re

Tactic:
obtain ⟨C, hC⟩ := h.le_const_mul_rpow

Premises used: LSeriesSummable.le_const_mul_rpow
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) s.re

Tactic:
Asymptotics.IsBigO.of_bound C <| eventually_atTop.mpr ⟨1, fun n hn ↦ ?_⟩

Premises used: Iff.mpr, Exists.intro, Asymptotics.IsBigO.of_bound, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) s.re
refine : ∀ (n : ℕ) (hn : n ≥ 1), ‖f n‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑n : ℝ) s.re‖
⊢ Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) s.re

Tactic:
refine Asymptotics.IsBigO.of_bound C <| eventually_atTop.mpr ⟨1, fun n hn ↦ ?_⟩

Premises used: Iff.mpr, Exists.intro, Asymptotics.IsBigO.of_bound, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) s.re
n : ℕ
hn : n ≥ 1
⊢ ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) s.re

Tactic:
hC n (Nat.pos_iff_ne_zero.mp hn)

Premises used: Nat.pos_iff_ne_zero, Iff.mp