awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact mem_image.mpr ⟨n, mem_range.mpr hn, rfl⟩

Premises used: Iff.mpr, Finset.mem_image, Finset.mem_range, And.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
m : ℝ
h : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ m
s : ℂ
hs : 1 < s.re
n : ℕ
hn : n ≠ 0
⊢ ‖f n‖ ≤ m * HPow.hPow (α := ℝ) (↑n : ℝ) (HSub.hSub (α := ℝ) 1 1)

Tactic:
simp [h n hn]
-- Module: Mathlib.NumberTheory.LSeries.Basic
Goal:
f : ℕ → ℂ
m : ℝ
h : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ m
s : ℝ
hs : 1 < s
⊢ 1 < (↑s : ℂ).re

Tactic:
simp [hs]
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f g : ℕ → ℂ
h : ∀ {n : ℕ}, n ≠ 0 → f n = g n
⊢ abscissaOfAbsConv f = abscissaOfAbsConv g

Tactic:
congr_arg sInf <| congr_arg _ <| Set.ext fun x ↦ LSeriesSummable_congr x h

Premises used: Set.ext, LSeriesSummable_congr, Complex.ofReal, congr_arg, InfSet.sInf, LSeries.abscissaOfAbsConv
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f g : ℕ → ℂ
h : f =ᶠ[atTop] g
⊢ abscissaOfAbsConv f = abscissaOfAbsConv g

Tactic:
congr_arg sInf <| congr_arg _ <| Set.ext fun x ↦ LSeriesSummable_congr' x h

Premises used: Set.ext, LSeriesSummable_congr', Complex.ofReal, congr_arg, InfSet.sInf, LSeries.abscissaOfAbsConv
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
s : ℂ
hs : abscissaOfAbsConv f < (↑s.re : EReal)
⊢ ∃ (a : ℝ), LSeriesSummable f (↑a : ℂ) ∧ a < s.re

Tactic:
simpa [abscissaOfAbsConv, sInf_lt_iff] using hs

Premises used: sInf_lt_iff, LSeries.abscissaOfAbsConv
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
s : ℂ
hs : abscissaOfAbsConv f < (↑s.re : EReal)
obtain : ∀ (y : ℝ) (hy : LSeriesSummable f (↑y : ℂ)) (hys : y < s.re), LSeriesSummable f s
⊢ LSeriesSummable f s

Tactic:
obtain ⟨y, hy, hys⟩ : ∃ a : ℝ, LSeriesSummable f a ∧ a < s.re := by
    simpa [abscissaOfAbsConv, sInf_lt_iff] using hs

Premises used: Complex.re
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
s : ℂ
hs : abscissaOfAbsConv f < (↑s.re : EReal)
y : ℝ
hy : LSeriesSummable f (↑y : ℂ)
hys : y < s.re
⊢ LSeriesSummable f s

Tactic:
hy.of_re_le_re <| ofReal_re y ▸ hys.le

Premises used: LSeriesSummable.of_re_le_re
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
s : ℂ
hs : abscissaOfAbsConv f < (↑s.re : EReal)
y : ℝ
hy : LSeriesSummable f (↑y : ℂ)
hys : y < s.re
⊢ LSeriesSummable f s

Tactic:
exact hy.of_re_le_re <| ofReal_re y ▸ hys.le

Premises used: LSeriesSummable.of_re_le_re
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
s : ℂ
hs : abscissaOfAbsConv f < (↑s.re : EReal)
obtain :
  ∀ (x : ℝ) (hx₁ : abscissaOfAbsConv f < (↑x : EReal)) (hx₂ : (↑x : EReal) < (↑s.re : EReal)),
    ∃ x < s.re, LSeriesSummable f (↑x : ℂ)
⊢ ∃ x < s.re, LSeriesSummable f (↑x : ℂ)

Tactic:
obtain ⟨x, hx₁, hx₂⟩ := EReal.exists_between_coe_real hs

Premises used: EReal.exists_between_coe_real
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
s : ℂ
hs : abscissaOfAbsConv f < (↑s.re : EReal)
x : ℝ
hx₁ : abscissaOfAbsConv f < (↑x : EReal)
hx₂ : (↑x : EReal) < (↑s.re : EReal)
⊢ x < s.re

Tactic:
simpa using hx₂
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
s : ℂ
hs : abscissaOfAbsConv f < (↑s.re : EReal)
x : ℝ
hx₁ : abscissaOfAbsConv f < (↑x : EReal)
hx₂ : (↑x : EReal) < (↑s.re : EReal)
⊢ ∃ x < s.re, LSeriesSummable f (↑x : ℂ)

Tactic:
exact ⟨x, by simpa using hx₂, LSeriesSummable_of_abscissaOfAbsConv_lt_re hx₁⟩
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ s.re ≤ (↑s.re : ℂ).re

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ (↑s.re : EReal) ∈ Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)}

Tactic:
simpa using h.of_re_le_re (by simp)

Premises used: LSeriesSummable.of_re_le_re
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f (↑y : ℂ)
⊢ abscissaOfAbsConv f ≤ (↑x : EReal)

Tactic:
sInf_le_iff.mpr fun y hy ↦ le_of_forall_gt_imp_ge_of_dense fun a ↦ ?_

Premises used: Iff.mpr, le_of_forall_gt_imp_ge_of_dense, LSeries.abscissaOfAbsConv, sInf_le_iff
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f (↑y : ℂ)
refine :
  ∀ (y : EReal) (hy : y ∈ lowerBounds (Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)})) (a : EReal),
    (↑x : EReal) < a → y ≤ a
⊢ abscissaOfAbsConv f ≤ (↑x : EReal)

Tactic:
refine sInf_le_iff.mpr fun y hy ↦ le_of_forall_gt_imp_ge_of_dense fun a ↦ ?_

Premises used: Iff.mpr, sInf_le_iff
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f (↑y : ℂ)
y : EReal
hy : y ∈ lowerBounds (Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)})
a : EReal
⊢ ∀ (a : ℝ), LSeriesSummable f (↑a : ℂ) → y ≤ (↑a : EReal)

Tactic:
simpa [mem_lowerBounds] using hy

Premises used: mem_lowerBounds
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f (↑y : ℂ)
y : EReal
hy : y ∈ lowerBounds (Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)})
a : EReal
⊢ ∀ (a : ℝ), LSeriesSummable f (↑a : ℂ) → y ≤ (↑a : EReal)

Tactic:
replace hy : ∀ (a : ℝ), LSeriesSummable f a → y ≤ a := by simpa [mem_lowerBounds] using hy
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f (↑y : ℂ)
y : EReal
hy : ∀ (a : ℝ), LSeriesSummable f (↑a : ℂ) → y ≤ (↑a : EReal)
a₀ : ℝ
⊢ (↑x : EReal) < (↑a₀ : EReal) → y ≤ (↑a₀ : EReal)

Tactic:
exact_mod_cast fun ha ↦ hy a₀ (h a₀ ha)
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f (↑y : ℂ)
y : EReal
hy : ∀ (a : ℝ), LSeriesSummable f (↑a : ℂ) → y ≤ (↑a : EReal)
⊢ (↑x : EReal) < ⊥ → y ≤ ⊥

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f (↑y : ℂ)
y : EReal
hy : ∀ (a : ℝ), LSeriesSummable f (↑a : ℂ) → y ≤ (↑a : EReal)
⊢ (↑x : EReal) < ⊤ → y ≤ ⊤

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f (↑y : ℂ)
y a : EReal
hy : ∀ (a : ℝ), LSeriesSummable f (↑a : ℂ) → y ≤ (↑a : EReal)
coe : ∀ (a₀ : ℝ), (↑x : EReal) < (↑a₀ : EReal) → y ≤ (↑a₀ : EReal)
bot : (↑x : EReal) < ⊥ → y ≤ ⊥
top : (↑x : EReal) < ⊤ → y ≤ ⊤
⊢ (↑x : EReal) < a → y ≤ a

Tactic:
cases a with
  | coe a₀ => exact_mod_cast fun ha ↦ hy a₀ (h a₀ ha)
  | bot => simp
  | top => simp
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
a : ℝ
h : ∀ (y : ℝ), (↑a : EReal) < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)
⊢ abscissaOfAbsConv f ≤ (↑a : EReal)

Tactic:
abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable <| mod_cast h

Premises used: cast, EReal.coe_lt_coe_iff._simp_1, LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable, Complex.ofReal, implies_congr, Eq.refl, LSeriesSummable, forall_congr
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
a : ℝ
h : ∀ (y : ℝ), (↑a : EReal) < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)
⊢ abscissaOfAbsConv f ≤ (↑a : EReal)

Tactic:
exact abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable <| mod_cast h

Premises used: LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊤ < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)
⊢ abscissaOfAbsConv f ≤ ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊤ < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)
⊢ abscissaOfAbsConv f ≤ ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊥ < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)
⊢ abscissaOfAbsConv f ≤ ⊥

Tactic:
le_of_eq <| sInf_eq_bot.mpr fun y hy ↦ ?_

Premises used: Iff.mpr, le_of_eq, sInf_eq_bot
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊥ < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)
bot : ∀ (y : EReal) (hy : ⊥ < y), ∃ a ∈ Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)}, a < y
⊢ abscissaOfAbsConv f ≤ ⊥

Tactic:
refine le_of_eq <| sInf_eq_bot.mpr fun y hy ↦ ?_

Premises used: Iff.mpr, le_of_eq, sInf_eq_bot
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊥ < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)
hy : LT.lt (α := EReal) ⊥ ⊥
⊢ ∃ a ∈ Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)}, a < ⊥

Tactic:
simp at hy
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊥ < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)
y : ℝ
hy : ⊥ < (↑y : EReal)
⊢ ∃ a ∈ Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)}, a < (↑y : EReal)

Tactic:
⟨_, ⟨_, h _ <| EReal.bot_lt_coe _, rfl⟩, mod_cast sub_one_lt y⟩

Premises used: EReal.bot_lt_coe, And.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊥ < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)
y : ℝ
hy : ⊥ < (↑y : EReal)
⊢ ∃ a ∈ Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)}, a < (↑y : EReal)

Tactic:
exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe _, rfl⟩, mod_cast sub_one_lt y⟩
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊥ < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)
hy : LT.lt (α := EReal) ⊥ ⊤
⊢ ∃ a ∈ Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)}, a < ⊤

Tactic:
⟨_, ⟨_, h _ <| EReal.bot_lt_coe 0, rfl⟩, EReal.zero_lt_top⟩

Premises used: EReal.bot_lt_coe, And.intro, Exists.intro, EReal.zero_lt_top, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊥ < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)
hy : LT.lt (α := EReal) ⊥ ⊤
⊢ ∃ a ∈ Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)}, a < ⊤

Tactic:
exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe 0, rfl⟩, EReal.zero_lt_top⟩
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊥ < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)
y : EReal
hy : ⊥ < y
bot : ∀ (hy : LT.lt (α := EReal) ⊥ ⊥), ∃ a ∈ Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)}, a < ⊥
bot₁ : ∀ (y : ℝ) (hy : ⊥ < (↑y : EReal)), ∃ a ∈ Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)}, a < (↑y : EReal)
bot₂ : ∀ (hy : LT.lt (α := EReal) ⊥ ⊤), ∃ a ∈ Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)}, a < ⊤
⊢ ∃ a ∈ Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)}, a < y

Tactic:
cases y with
    | bot => simp at hy
    | coe y => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe _, rfl⟩, mod_cast sub_one_lt y⟩
    | top => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe 0, rfl⟩, EReal.zero_lt_top⟩
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
x : EReal
h : ∀ (y : ℝ), x < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)
coe :
  ∀ (a : ℝ) (h : ∀ (y : ℝ), (↑a : EReal) < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)),
    abscissaOfAbsConv f ≤ (↑a : EReal)
top : ∀ (h : ∀ (y : ℝ), ⊤ < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)), abscissaOfAbsConv f ≤ ⊤
bot : ∀ (h : ∀ (y : ℝ), ⊥ < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)), abscissaOfAbsConv f ≤ ⊥
⊢ abscissaOfAbsConv f ≤ x

Tactic:
cases x with
  | coe => exact abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable <| mod_cast h
  | top => exact le_top
  | bot =>
    refine le_of_eq <| sInf_eq_bot.mpr fun y hy ↦ ?_
    cases y with
    | bot => simp at hy
    | coe y => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe _, rfl⟩, mod_cast sub_one_lt y⟩
    | top => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe 0, rfl⟩, EReal.zero_lt_top⟩

Premises used: Iff.mpr, LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable, le_top, le_of_eq, sInf_eq_bot
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
x : ℝ
h : ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) x
⊢ x = x + 1 - 1

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
x : ℝ
h : ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) x
⊢ ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x + 1 - 1)

Tactic:
rw [show x = x + 1 - 1 by ring] at h
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
x : ℝ
h : ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x + 1 - 1)
by_contra! : ∀ (H : (↑x : EReal) + 1 < abscissaOfAbsConv f), False
⊢ abscissaOfAbsConv f ≤ (↑x : EReal) + 1

Tactic:
by_contra! H
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
x : ℝ
h : ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x + 1 - 1)
H : (↑x : EReal) + 1 < abscissaOfAbsConv f
obtain : ∀ (y : ℝ) (hy₁ : (↑x : EReal) + 1 < (↑y : EReal)) (hy₂ : (↑y : EReal) < abscissaOfAbsConv f), False
⊢ False

Tactic:
obtain ⟨y, hy₁, hy₂⟩ := EReal.exists_between_coe_real H

Premises used: EReal.exists_between_coe_real
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
x : ℝ
h : ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x + 1 - 1)
H : (↑x : EReal) + 1 < abscissaOfAbsConv f
y : ℝ
hy₁ : (↑x : EReal) + 1 < (↑y : EReal)
hy₂ : (↑y : EReal) < abscissaOfAbsConv f
⊢ False

Tactic:
(LSeriesSummable_of_le_const_mul_rpow (s := y) (EReal.coe_lt_coe_iff.mp hy₁) h
    |>.abscissaOfAbsConv_le.trans_lt hy₂).false

Premises used: LSeriesSummable_of_le_const_mul_rpow, LSeriesSummable.abscissaOfAbsConv_le, Iff.mp, LT.lt.false, LE.le.trans_lt, EReal.coe_lt_coe_iff
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
x : ℝ
h : ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x + 1 - 1)
H : (↑x : EReal) + 1 < abscissaOfAbsConv f
y : ℝ
hy₁ : (↑x : EReal) + 1 < (↑y : EReal)
hy₂ : (↑y : EReal) < abscissaOfAbsConv f
⊢ False

Tactic:
exact (LSeriesSummable_of_le_const_mul_rpow (s := y) (EReal.coe_lt_coe_iff.mp hy₁) h
    |>.abscissaOfAbsConv_le.trans_lt hy₂).false

Premises used: LSeriesSummable_of_le_const_mul_rpow, LSeriesSummable.abscissaOfAbsConv_le, Iff.mp, LT.lt.false, LE.le.trans_lt, EReal.coe_lt_coe_iff
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
x : ℝ
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) x
⊢ x = x + 1 - 1

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
x : ℝ
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) x
⊢ Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x + 1 - 1)

Tactic:
rw [show x = x + 1 - 1 by ring] at h
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
x : ℝ
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x + 1 - 1)
by_contra! : ∀ (H : (↑x : EReal) + 1 < abscissaOfAbsConv f), False
⊢ abscissaOfAbsConv f ≤ (↑x : EReal) + 1

Tactic:
by_contra! H
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
x : ℝ
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x + 1 - 1)
H : (↑x : EReal) + 1 < abscissaOfAbsConv f
obtain : ∀ (y : ℝ) (hy₁ : (↑x : EReal) + 1 < (↑y : EReal)) (hy₂ : (↑y : EReal) < abscissaOfAbsConv f), False
⊢ False

Tactic:
obtain ⟨y, hy₁, hy₂⟩ := EReal.exists_between_coe_real H

Premises used: EReal.exists_between_coe_real
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
x : ℝ
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x + 1 - 1)
H : (↑x : EReal) + 1 < abscissaOfAbsConv f
y : ℝ
hy₁ : (↑x : EReal) + 1 < (↑y : EReal)
hy₂ : (↑y : EReal) < abscissaOfAbsConv f
⊢ False

Tactic:
(LSeriesSummable_of_isBigO_rpow (s := y) (EReal.coe_lt_coe_iff.mp hy₁) h
    |>.abscissaOfAbsConv_le.trans_lt hy₂).false

Premises used: LSeriesSummable.abscissaOfAbsConv_le, LSeriesSummable_of_isBigO_rpow, Iff.mp, LT.lt.false, LE.le.trans_lt, EReal.coe_lt_coe_iff
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
x : ℝ
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x + 1 - 1)
H : (↑x : EReal) + 1 < abscissaOfAbsConv f
y : ℝ
hy₁ : (↑x : EReal) + 1 < (↑y : EReal)
hy₂ : (↑y : EReal) < abscissaOfAbsConv f
⊢ False

Tactic:
exact (LSeriesSummable_of_isBigO_rpow (s := y) (EReal.coe_lt_coe_iff.mp hy₁) h
    |>.abscissaOfAbsConv_le.trans_lt hy₂).false

Premises used: LSeriesSummable.abscissaOfAbsConv_le, LSeriesSummable_of_isBigO_rpow, Iff.mp, LT.lt.false, LE.le.trans_lt, EReal.coe_lt_coe_iff
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
h : ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C
⊢ ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 0

Tactic:
simpa using h
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
h : ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C
⊢ abscissaOfAbsConv f ≤ 1

Tactic:
simpa using abscissaOfAbsConv_le_of_le_const_mul_rpow (x := 0) (by simpa using h)

Premises used: LSeries.abscissaOfAbsConv_le_of_le_const_mul_rpow
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ 1
⊢ Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 0

Tactic:
simpa using h
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℂ
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ 1
⊢ abscissaOfAbsConv f ≤ 1

Tactic:
simpa using abscissaOfAbsConv_le_of_isBigO_rpow (x := 0) (by simpa using h)

Premises used: LSeries.abscissaOfAbsConv_le_of_isBigO_rpow
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun (x : ℕ) ↦ (↑(f x) : ℂ)) < (↑x : EReal)
h₁ :
  ∀ (n : ℕ),
    term (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ) n = (↑(if n = 0 then 0 else f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)
⊢ term (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ) = fun (n : ℕ) ↦
    (↑(if n = 0 then 0 else f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)

Tactic:
ext n
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun (x : ℕ) ↦ (↑(f x) : ℂ)) < (↑x : EReal)
n : ℕ
⊢ term (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ) n = (↑(if n = 0 then 0 else f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)

Tactic:
simp [term_def, apply_ite ((↑) : ℝ → ℂ), ofReal_cpow n.cast_nonneg]

Premises used: Nat.cast_nonneg, LSeries.term_def, Complex.ofReal_cpow, apply_ite, Complex.ofReal
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun (x : ℕ) ↦ (↑(f x) : ℂ)) < (↑x : EReal)
⊢ term (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ) = fun (n : ℕ) ↦
    (↑(if n = 0 then 0 else f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)

Tactic:
have aux : term (f ·) x = fun n ↦ ↑(if n = 0 then 0 else f n / (n : ℝ) ^ x) := by
    ext n
    simp [term_def, apply_ite ((↑) : ℝ → ℂ), ofReal_cpow n.cast_nonneg]
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun (x : ℕ) ↦ (↑(f x) : ℂ)) < (↑x : EReal)
aux :
  term (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ) = fun (n : ℕ) ↦
    (↑(if n = 0 then 0 else f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)
⊢ LSeriesSummable (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ)

Tactic:
have := LSeriesSummable_of_abscissaOfAbsConv_lt_re (ofReal_re x ▸ h)
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun (x : ℕ) ↦ (↑(f x) : ℂ)) < (↑x : EReal)
aux :
  term (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ) = fun (n : ℕ) ↦
    (↑(if n = 0 then 0 else f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)
this : LSeriesSummable (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ)
⊢ Summable (α := ℝ) fun (x_1 : ℕ) ↦ if x_1 = 0 then 0 else f x_1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) x

Tactic:
simp only [LSeriesSummable, aux, summable_ofReal] at this

Premises used: Complex.summable_ofReal, LSeriesSummable
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun (x : ℕ) ↦ (↑(f x) : ℂ)) < (↑x : EReal)
aux :
  term (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ) = fun (n : ℕ) ↦
    (↑(if n = 0 then 0 else f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)
this : Summable (α := ℝ) fun (x_1 : ℕ) ↦ if x_1 = 0 then 0 else f x_1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) x
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ f n / HPow.hPow (α := ℝ) (↑n : ℝ) x

Tactic:
this.congr_cofinite ?_

Premises used: Summable.congr_cofinite
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun (x : ℕ) ↦ (↑(f x) : ℂ)) < (↑x : EReal)
aux :
  term (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ) = fun (n : ℕ) ↦
    (↑(if n = 0 then 0 else f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)
this : Summable (α := ℝ) fun (x_1 : ℕ) ↦ if x_1 = 0 then 0 else f x_1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) x
refine :
  Filter.EventuallyEq (β := ℝ) Filter.cofinite
    (fun (x_1 : ℕ) ↦ if x_1 = 0 then 0 else f x_1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) x) fun (n : ℕ) ↦
    f n / HPow.hPow (α := ℝ) (↑n : ℝ) x
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ f n / HPow.hPow (α := ℝ) (↑n : ℝ) x

Tactic:
refine this.congr_cofinite ?_

Premises used: Summable.congr_cofinite
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun (x : ℕ) ↦ (↑(f x) : ℂ)) < (↑x : EReal)
aux :
  term (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ) = fun (n : ℕ) ↦
    (↑(if n = 0 then 0 else f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)
this : Summable (α := ℝ) fun (x_1 : ℕ) ↦ if x_1 = 0 then 0 else f x_1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) x
n : ℕ
hn : Membership.mem (γ := Set ℕ) {0}ᶜ n
⊢ ¬n = 0

Tactic:
simpa using hn
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun (x : ℕ) ↦ (↑(f x) : ℂ)) < (↑x : EReal)
aux :
  term (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ) = fun (n : ℕ) ↦
    (↑(if n = 0 then 0 else f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)
this : Summable (α := ℝ) fun (x_1 : ℕ) ↦ if x_1 = 0 then 0 else f x_1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) x
h₁ :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x_1 : ℕ |
        Membership.mem (γ := Set ℕ) {0}ᶜ x_1 →
          Membership.mem (γ := Set ℕ)
            {x_2 : ℕ |
              (fun (x_3 : ℕ) ↦
                  Eq (α := ℝ) ((fun (x_4 : ℕ) ↦ if x_4 = 0 then 0 else f x_4 / HPow.hPow (α := ℝ) (↑x_4 : ℝ) x) x_3)
                    ((fun (n : ℕ) ↦ f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) x_3))
                x_2}
            x_1}
      a
h₂ h₃ :
  ∀ (n : ℕ) (hn : Membership.mem (γ := Set ℕ) {0}ᶜ n),
    (if n = 0 then 0 else f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) = f n / HPow.hPow (α := ℝ) (↑n : ℝ) x
⊢ Filter.EventuallyEq (β := ℝ) Filter.cofinite
    (fun (x_1 : ℕ) ↦ if x_1 = 0 then 0 else f x_1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) x) fun (n : ℕ) ↦
    f n / HPow.hPow (α := ℝ) (↑n : ℝ) x

Tactic:
filter_upwards [(Set.finite_singleton 0).compl_mem_cofinite] with n hn
    using if_neg (by simpa using hn)

Premises used: Set.Finite.compl_mem_cofinite, OfNat.ofNat, if_neg, Set.finite_singleton
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
⊢ abscissaOfAbsConv (F f g) ≤ max (abscissaOfAbsConv f) (abscissaOfAbsConv g)

Tactic:
abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' fun x hx ↦ hF ?_ ?_

Premises used: LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable'