awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h₁ : ‖HPow.hPow (α := ℝ) (↑n : ℝ) s.re‖ = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ ‖f n‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑n : ℝ) s.re‖

Tactic:
convert! hC n (Nat.pos_iff_ne_zero.mp hn) using 2

Premises used: Nat.pos_iff_ne_zero, Iff.mp
-- 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
h₁ : |HPow.hPow (α := ℝ) (↑n : ℝ) s.re| = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
h₂ : HPow.hPow (α := ℝ) |(↑n : ℝ)| s.re = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
h₃ h₄ : HPow.hPow (α := ℝ) (↑n : ℝ) s.re = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ ‖HPow.hPow (α := ℝ) (↑n : ℝ) s.re‖ = HPow.hPow (α := ℝ) (↑n : ℝ) s.re

Tactic:
rw [Real.norm_eq_abs, Real.abs_rpow_of_nonneg n.cast_nonneg, abs_of_nonneg n.cast_nonneg]

Premises used: Nat.cast_nonneg, Real.abs_rpow_of_nonneg, abs_of_nonneg, Real.norm_eq_abs
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
obtain : ∀ (C : ℝ) (hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)), LSeriesSummable f s
⊢ LSeriesSummable f s

Tactic:
obtain ⟨C, hC⟩ := h
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
⊢ ‖f 1‖ ≤ C

Tactic:
simpa using hC 1 one_ne_zero

Premises used: one_ne_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
⊢ 0 ≤ C

Tactic:
have hC₀ : 0 ≤ C := (norm_nonneg <| f 1).trans <| by simpa using hC 1 one_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
simp_rw : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ)‖ * ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-(s + (1 - (↑x : ℂ))))‖
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖

Tactic:
simp_rw [div_eq_mul_inv, norm_mul, ← cpow_neg]

Premises used: Complex.cpow_neg, norm_mul, div_eq_mul_inv
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
linarith : -1 ≤ -s.re + x - 1 → -1 - (-s.re + x - 1) + (x - s.re) = 0
⊢ -s.re + x - 1 < -1

Tactic:
linarith only [hs]
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
⊢ -s.re + x - 1 < -1

Tactic:
have hsx : -s.re + x - 1 < -1 := by linarith only [hs]
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ)‖ * ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-(s + (1 - (↑x : ℂ))))‖

Tactic:
Summable.mul_left _ <|
      Summable.of_norm_bounded_eventually_nat (g := fun n ↦ (n : ℝ) ^ (-s.re + x - 1)) ?_ ?_

Premises used: Summable.mul_left, Summable.of_norm_bounded_eventually_nat
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
refine_1 : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re + x - 1)
refine_2 :
  ∀ᶠ (i : ℕ) in Filter.atTop,
    ‖‖HPow.hPow (α := ℂ) (↑i : ℂ) (-(s + (1 - (↑x : ℂ))))‖‖ ≤
      (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re + x - 1)) i
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ)‖ * ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-(s + (1 - (↑x : ℂ))))‖

Tactic:
refine Summable.mul_left _ <|
      Summable.of_norm_bounded_eventually_nat (g := fun n ↦ (n : ℝ) ^ (-s.re + x - 1)) ?_ ?_

Premises used: Summable.mul_left, Summable.of_norm_bounded_eventually_nat
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re + x - 1)

Tactic:
simpa
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
refine_2 :
  ∃ (a : ℕ),
    ∀ b ≥ a, ‖HPow.hPow (α := ℂ) (↑b : ℂ) (-(s + (1 - (↑x : ℂ))))‖ ≤ HPow.hPow (α := ℝ) (↑b : ℝ) (-s.re + x - 1)
⊢ ∀ᶠ (i : ℕ) in Filter.atTop,
    ‖‖HPow.hPow (α := ℂ) (↑i : ℂ) (-(s + (1 - (↑x : ℂ))))‖‖ ≤
      (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re + x - 1)) i

Tactic:
simp only [norm_norm, Filter.eventually_atTop]

Premises used: norm_norm, Filter.eventually_atTop
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
⊢ ∃ (a : ℕ),
    ∀ b ≥ a, ‖HPow.hPow (α := ℂ) (↑b : ℂ) (-(s + (1 - (↑x : ℂ))))‖ ≤ HPow.hPow (α := ℝ) (↑b : ℝ) (-s.re + x - 1)

Tactic:
⟨1, fun n hn ↦ le_of_eq ?_⟩

Premises used: Exists.intro, le_of_eq, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
refine_2 :
  ∀ (n : ℕ) (hn : n ≥ 1),
    ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-(s + (1 - (↑x : ℂ))))‖ = HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re + x - 1)
⊢ ∃ (a : ℕ),
    ∀ b ≥ a, ‖HPow.hPow (α := ℂ) (↑b : ℂ) (-(s + (1 - (↑x : ℂ))))‖ ≤ HPow.hPow (α := ℝ) (↑b : ℝ) (-s.re + x - 1)

Tactic:
refine ⟨1, fun n hn ↦ le_of_eq ?_⟩
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
n : ℕ
hn : n ≥ 1
refine_2 : HPow.hPow (α := ℝ) (↑n : ℝ) (-(s.re + (1 - x))) = HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re + x - 1)
⊢ ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-(s + (1 - (↑x : ℂ))))‖ = HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re + x - 1)

Tactic:
simp only [norm_natCast_cpow_of_pos hn, add_re, sub_re, neg_re, ofReal_re, one_re]

Premises used: Complex.sub_re, Complex.add_re, Complex.norm_natCast_cpow_of_pos, Complex.neg_re, Complex.ofReal_re, Complex.one_re
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
n : ℕ
hn : n ≥ 1
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (-(s.re + (1 - x))) = HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re + x - 1)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖

Tactic:
have hsum : Summable fun n : ℕ ↦ ‖(C : ℂ) / n ^ (s + (1 - x))‖ := by
    simp_rw [div_eq_mul_inv, norm_mul, ← cpow_neg]
    have hsx : -s.re + x - 1 < -1 := by linarith only [hs]
    refine Summable.mul_left _ <|
      Summable.of_norm_bounded_eventually_nat (g := fun n ↦ (n : ℝ) ^ (-s.re + x - 1)) ?_ ?_
    · simpa
    · simp only [norm_norm, Filter.eventually_atTop]
      refine ⟨1, fun n hn ↦ le_of_eq ?_⟩
      simp only [norm_natCast_cpow_of_pos hn, add_re, sub_re, neg_re, ofReal_re, one_re]
      ring_nf
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsum : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
⊢ LSeriesSummable f s

Tactic:
Summable.of_norm <| hsum.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun n ↦ ?_)

Premises used: Summable.of_norm, Summable.of_nonneg_of_le, LSeries.term, norm_nonneg, LSeriesSummable
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsum : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
refine : ∀ (n : ℕ), ‖term f s n‖ ≤ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
⊢ LSeriesSummable f s

Tactic:
refine Summable.of_norm <| hsum.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun n ↦ ?_)

Premises used: Summable.of_norm, Summable.of_nonneg_of_le, norm_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsum : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
n : ℕ
inl : ‖term f s 0‖ ≤ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑0 : ℂ) (s + (1 - (↑x : ℂ)))‖
inr : ∀ (hn : n > 0), ‖term f s n‖ ≤ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
⊢ ‖term f s n‖ ≤ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖

Tactic:
rcases n.eq_zero_or_pos with rfl | hn

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsum : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
⊢ ‖term f s 0‖ ≤ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑0 : ℂ) (s + (1 - (↑x : ℂ)))‖

Tactic:
simpa only [term_zero, norm_zero] using norm_nonneg _

Premises used: norm_zero, norm_nonneg, LSeries.term_zero
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsum : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
n : ℕ
hn : n > 0
⊢ 0 < HPow.hPow (α := ℝ) (↑n : ℝ) s.re

Tactic:
have hn' : 0 < (n : ℝ) ^ s.re := Real.rpow_pos_of_pos (Nat.cast_pos.mpr hn) _
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsum : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
n : ℕ
hn : n > 0
hn' : 0 < HPow.hPow (α := ℝ) (↑n : ℝ) s.re
inr : ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (-(s + (1 - (↑x : ℂ))).re + s.re)
⊢ ‖term f s n‖ ≤ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖

Tactic:
simp_rw [term_of_ne_zero hn.ne', norm_div, norm_natCast_cpow_of_pos hn, div_le_iff₀ hn',
    norm_real, Real.norm_of_nonneg hC₀, div_eq_mul_inv, mul_assoc,
    ← Real.rpow_neg <| Nat.cast_nonneg _, ← Real.rpow_add <| Nat.cast_pos.mpr hn]

Premises used: Iff.mpr, div_le_iff₀, Nat.cast_pos, Nat.cast_nonneg, mul_assoc, LSeries.term_of_ne_zero, Complex.norm_real, div_eq_mul_inv, LT.lt.ne', Complex.norm_natCast_cpow_of_pos, norm_div, Real.rpow_add, Real.rpow_neg, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsum : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
n : ℕ
hn : n > 0
hn' : 0 < HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (-(s + (1 - (↑x : ℂ))).re + s.re)

Tactic:
simpa using hC n <| Nat.pos_iff_ne_zero.mp hn

Premises used: Nat.pos_iff_ne_zero, Iff.mp
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
obtain :
  ∀ (C : ℝ) (hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖), LSeriesSummable f s
⊢ LSeriesSummable f s

Tactic:
obtain ⟨C, hC⟩ := Asymptotics.isBigO_iff.mp h

Premises used: Asymptotics.isBigO_iff, Iff.mp
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
obtain : ∀ (m : ℕ) (hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖), LSeriesSummable f s
⊢ LSeriesSummable f s

Tactic:
obtain ⟨m, hm⟩ := eventually_atTop.mp hC

Premises used: Iff.mp, Filter.eventually_atTop
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
⊢ 0 ≤ C'

Tactic:
have hC'₀ : 0 ≤ C' := (le_max' _ _ (mem_insert.mpr (Or.inl rfl))).trans <| le_max_right ..
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
⊢ C ≤ C'

Tactic:
have hCC' : C ≤ C' := le_max_left ..
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
⊢ LSeriesSummable f s

Tactic:
LSeriesSummable_of_le_const_mul_rpow hs ⟨C', fun n hn₀ ↦ ?_⟩

Premises used: LSeriesSummable_of_le_const_mul_rpow, Exists.intro
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
refine : ∀ (n : ℕ) (hn₀ : n ≠ 0), ‖f n‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
⊢ LSeriesSummable f s

Tactic:
refine LSeriesSummable_of_le_const_mul_rpow hs ⟨C', fun n hn₀ ↦ ?_⟩

Premises used: LSeriesSummable_of_le_const_mul_rpow, Exists.intro
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
inl : ∀ (hn : m ≤ n), ‖f n‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
inr : ∀ (hn : n < m), ‖f n‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
⊢ ‖f n‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)

Tactic:
rcases le_or_gt m n with hn | hn

Premises used: le_or_gt
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
hn : m ≤ n
⊢ ‖f n‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)

Tactic:
(hm n hn).trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
hn : m ≤ n
inl : C * ‖HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
⊢ ‖f n‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)

Tactic:
refine (hm n hn).trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
hn : m ≤ n
⊢ LE.le (α := ℝ) 0 (↑n : ℝ)

Tactic:
have hn₀ : (0 : ℝ) ≤ n := cast_nonneg _
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀_1 : n ≠ 0
hn : m ≤ n
hn₀ : LE.le (α := ℝ) 0 (↑n : ℝ)
inl : ‖HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)‖ ≤ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
⊢ C * ‖HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀_1 : n ≠ 0
hn : m ≤ n
hn₀ : LE.le (α := ℝ) 0 (↑n : ℝ)
inl : |HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)| ≤ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
inl₁ : HPow.hPow (α := ℝ) |(↑n : ℝ)| (x - 1) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
inl₂ inl₃ : HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
⊢ ‖HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)‖ ≤ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)

Tactic:
rw [Real.norm_eq_abs, abs_rpow_of_nonneg hn₀, abs_of_nonneg hn₀]

Premises used: Real.abs_rpow_of_nonneg, abs_of_nonneg, Real.norm_eq_abs
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
hn : n < m
⊢ 0 < n

Tactic:
have hn' : 0 < n := Nat.pos_of_ne_zero hn₀
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
hn : n < m
hn' : 0 < n
⊢ ‖f n‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)

Tactic:
(div_le_iff₀ <| rpow_pos_of_pos (cast_pos.mpr hn') _).mp ?_

Premises used: Iff.mpr, div_le_iff₀, Real.rpow_pos_of_pos, Nat.cast_pos, Iff.mp
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
hn : n < m
hn' : 0 < n
inr : ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1) ≤ C'
⊢ ‖f n‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)

Tactic:
refine (div_le_iff₀ <| rpow_pos_of_pos (cast_pos.mpr hn') _).mp ?_

Premises used: Iff.mpr, div_le_iff₀, Real.rpow_pos_of_pos, Nat.cast_pos, Iff.mp
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
hn : n < m
hn' : 0 < n
⊢ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1) ≤ C'

Tactic:
(le_max' _ _ <| mem_insert_of_mem ?_).trans <| le_max_right ..

Premises used: le_max_right, Finset.mem_insert_of_mem, Finset.le_max', LE.le.trans
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
hn : n < m
hn' : 0 < n
inr :
  Membership.mem (γ := Finset ℝ) (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))
    (‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1))
⊢ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1) ≤ C'

Tactic:
refine (le_max' _ _ <| mem_insert_of_mem ?_).trans <| le_max_right ..

Premises used: le_max_right, Finset.mem_insert_of_mem, Finset.le_max', LE.le.trans
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
hn : n < m
hn' : 0 < n
⊢ Membership.mem (γ := Finset ℝ) (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))
    (‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1))

Tactic:
mem_image.mpr ⟨n, mem_range.mpr hn, rfl⟩

Premises used: Iff.mpr, Finset.mem_image, Finset.mem_range, And.intro, Exists.intro, rfl