awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ Filter.EventuallyEq (β := ℂ) Filter.atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0

Tactic:
simpa only [H] using Filter.EventuallyEq.rfl

Premises used: Filter.EventuallyEq.rfl
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) fun (x : ℝ) ↦ LSeries g (↑x : ℂ)
rw :
  ∀ (h : ∃ (a : ℝ), ∀ b ≥ a, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)),
    ∃ (a : ℝ), ∀ b ≥ a, LSeries (f - g) (↑b : ℂ) = 0 b
⊢ EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries (f - g) (↑x : ℂ)) 0

Tactic:
rw [EventuallyEq, eventually_atTop] at h ⊢

Premises used: Filter.EventuallyEq, Filter.eventually_atTop
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : ∃ (a : ℝ), ∀ b ≥ a, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
obtain :
  ∀ (x₀ : ℝ) (hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)),
    ∃ (a : ℝ), ∀ b ≥ a, LSeries (f - g) (↑b : ℂ) = 0 b
⊢ ∃ (a : ℝ), ∀ b ≥ a, LSeries (f - g) (↑b : ℂ) = 0 b

Tactic:
obtain ⟨x₀, hx₀⟩ := h
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
obtain :
  ∀ (yf : EReal) (hyf₁ : abscissaOfAbsConv f < yf) (hyf₂ : yf < ⊤), ∃ (a : ℝ), ∀ b ≥ a, LSeries (f - g) (↑b : ℂ) = 0 b
⊢ ∃ (a : ℝ), ∀ b ≥ a, LSeries (f - g) (↑b : ℂ) = 0 b

Tactic:
obtain ⟨yf, hyf₁, hyf₂⟩ := exists_between hf

Premises used: exists_between
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : EReal
hyf₁ : abscissaOfAbsConv f < yf
hyf₂ : yf < ⊤
obtain :
  ∀ (yg : EReal) (hyg₁ : abscissaOfAbsConv g < yg) (hyg₂ : yg < ⊤), ∃ (a : ℝ), ∀ b ≥ a, LSeries (f - g) (↑b : ℂ) = 0 b
⊢ ∃ (a : ℝ), ∀ b ≥ a, LSeries (f - g) (↑b : ℂ) = 0 b

Tactic:
obtain ⟨yg, hyg₁, hyg₂⟩ := exists_between hg

Premises used: exists_between
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : EReal
hyf₁ : abscissaOfAbsConv f < yf
hyf₂ : yf < ⊤
yg : EReal
hyg₁ : abscissaOfAbsConv g < yg
hyg₂ : yg < ⊤
⊢ yf ≠ ⊤ ∧ yf ≠ ⊥

Tactic:
⟨hyf₂.ne, ((OrderBot.bot_le _).trans_lt hyf₁).ne'⟩

Premises used: LT.lt.ne', OrderBot.bot_le, And.intro, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : EReal
hyf₁ : abscissaOfAbsConv f < yf
hyf₂ : yf < ⊤
yg : EReal
hyg₁ : abscissaOfAbsConv g < yg
hyg₂ : yg < ⊤
lift :
  ∀ (yf : ℝ) (hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)) (hyf₂ : (↑yf : EReal) < ⊤),
    ∃ (a : ℝ), ∀ b ≥ a, LSeries (f - g) (↑b : ℂ) = 0 b
⊢ ∃ (a : ℝ), ∀ b ≥ a, LSeries (f - g) (↑b : ℂ) = 0 b

Tactic:
lift yf to ℝ using ⟨hyf₂.ne, ((OrderBot.bot_le _).trans_lt hyf₁).ne'⟩
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yg : EReal
hyg₁ : abscissaOfAbsConv g < yg
hyg₂ : yg < ⊤
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
⊢ yg ≠ ⊤ ∧ yg ≠ ⊥

Tactic:
⟨hyg₂.ne, ((OrderBot.bot_le _).trans_lt hyg₁).ne'⟩

Premises used: LT.lt.ne', OrderBot.bot_le, And.intro, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yg : EReal
hyg₁ : abscissaOfAbsConv g < yg
hyg₂ : yg < ⊤
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
lift :
  ∀ (yg : ℝ) (hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)) (hyg₂ : (↑yg : EReal) < ⊤),
    ∃ (a : ℝ), ∀ b ≥ a, LSeries (f - g) (↑b : ℂ) = 0 b
⊢ ∃ (a : ℝ), ∀ b ≥ a, LSeries (f - g) (↑b : ℂ) = 0 b

Tactic:
lift yg to ℝ using ⟨hyg₂.ne, ((OrderBot.bot_le _).trans_lt hyg₁).ne'⟩
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
⊢ ∃ (a : ℝ), ∀ b ≥ a, LSeries (f - g) (↑b : ℂ) = 0 b

Tactic:
⟨max x₀ (max yf yg), fun x hx ↦ ?_⟩

Premises used: Max.max, Exists.intro
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
refine : ∀ (x : ℝ) (hx : x ≥ max x₀ (max yf yg)), LSeries (f - g) (↑x : ℂ) = 0 x
⊢ ∃ (a : ℝ), ∀ b ≥ a, LSeries (f - g) (↑b : ℂ) = 0 b

Tactic:
refine ⟨max x₀ (max yf yg), fun x hx ↦ ?_⟩
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
⊢ LSeriesSummable f (↑x : ℂ)

Tactic:
LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
      (ofReal_re x).symm ▸ hyf₁.trans_le (EReal.coe_le_coe_iff.mpr ?_)

Premises used: Iff.mpr, EReal.coe_le_coe_iff, Eq.rec, LSeriesSummable_of_abscissaOfAbsConv_lt_re, LT.lt.trans_le, Complex.ofReal_re, Eq.symm
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
refine : yf ≤ x
⊢ LSeriesSummable f (↑x : ℂ)

Tactic:
refine LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
      (ofReal_re x).symm ▸ hyf₁.trans_le (EReal.coe_le_coe_iff.mpr ?_)

Premises used: LSeriesSummable_of_abscissaOfAbsConv_lt_re
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
⊢ yf ≤ x

Tactic:
(le_max_left _ yg).trans <| (le_max_right x₀ _).trans hx

Premises used: le_max_right, LE.le.trans, le_max_left
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
⊢ yf ≤ x

Tactic:
exact (le_max_left _ yg).trans <| (le_max_right x₀ _).trans hx

Premises used: le_max_right, LE.le.trans, le_max_left
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
⊢ LSeriesSummable f (↑x : ℂ)

Tactic:
have Hf : LSeriesSummable f x := by
    refine LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
      (ofReal_re x).symm ▸ hyf₁.trans_le (EReal.coe_le_coe_iff.mpr ?_)
    exact (le_max_left _ yg).trans <| (le_max_right x₀ _).trans hx
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f (↑x : ℂ)
⊢ LSeriesSummable g (↑x : ℂ)

Tactic:
LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
      (ofReal_re x).symm ▸ hyg₁.trans_le (EReal.coe_le_coe_iff.mpr ?_)

Premises used: Iff.mpr, EReal.coe_le_coe_iff, Eq.rec, LSeriesSummable_of_abscissaOfAbsConv_lt_re, LT.lt.trans_le, Complex.ofReal_re, Eq.symm
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f (↑x : ℂ)
refine : yg ≤ x
⊢ LSeriesSummable g (↑x : ℂ)

Tactic:
refine LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
      (ofReal_re x).symm ▸ hyg₁.trans_le (EReal.coe_le_coe_iff.mpr ?_)

Premises used: LSeriesSummable_of_abscissaOfAbsConv_lt_re
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f (↑x : ℂ)
⊢ yg ≤ x

Tactic:
(le_max_right yf _).trans <| (le_max_right x₀ _).trans hx

Premises used: le_max_right, LE.le.trans
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f (↑x : ℂ)
⊢ yg ≤ x

Tactic:
exact (le_max_right yf _).trans <| (le_max_right x₀ _).trans hx

Premises used: le_max_right, LE.le.trans
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f (↑x : ℂ)
⊢ LSeriesSummable g (↑x : ℂ)

Tactic:
have Hg : LSeriesSummable g x := by
    refine LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
      (ofReal_re x).symm ▸ hyg₁.trans_le (EReal.coe_le_coe_iff.mpr ?_)
    exact (le_max_right yf _).trans <| (le_max_right x₀ _).trans hx
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f (↑b : ℂ) = LSeries g (↑b : ℂ)
yf : ℝ
hyf₁ : abscissaOfAbsConv f < (↑yf : EReal)
hyf₂ : (↑yf : EReal) < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < (↑yg : EReal)
hyg₂ : (↑yg : EReal) < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f (↑x : ℂ)
Hg : LSeriesSummable g (↑x : ℂ)
rw : LSeries f (↑x : ℂ) - LSeries g (↑x : ℂ) = 0 x
rw₁ : LSeries g (↑x : ℂ) - LSeries g (↑x : ℂ) = 0 x
rw₂ : Eq (α := ℂ) 0 (0 x)
rw₃ rw₄ : Eq (α := ℂ) 0 0
⊢ LSeries (f - g) (↑x : ℂ) = 0 x

Tactic:
rw [LSeries_sub Hf Hg, hx₀ x <| (le_max_left ..).trans hx, sub_self, Pi.zero_apply]

Premises used: sub_self, LSeries_sub, Pi.zero_apply, LE.le.trans, le_max_left
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) fun (x : ℝ) ↦ LSeries g (↑x : ℂ)
n : ℕ
hn : n ≠ 0
⊢ EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries (f - g) (↑x : ℂ)) 0

Tactic:
have hsub : (fun x : ℝ ↦ LSeries (f - g) x) =ᶠ[atTop] (0 : ℝ → ℂ) :=
    LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq hf hg h
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) fun (x : ℝ) ↦ LSeries g (↑x : ℂ)
n : ℕ
hn : n ≠ 0
hsub : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries (f - g) (↑x : ℂ)) 0
⊢ abscissaOfAbsConv (f - g) ≠ ⊤

Tactic:
have ha : abscissaOfAbsConv (f - g) ≠ ⊤ :=
    lt_top_iff_ne_top.mp <| (abscissaOfAbsConv_sub_le f g).trans_lt <| max_lt hf hg
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) fun (x : ℝ) ↦ LSeries g (↑x : ℂ)
n : ℕ
hn : n ≠ 0
hsub : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries (f - g) (↑x : ℂ)) 0
ha : abscissaOfAbsConv (f - g) ≠ ⊤
⊢ f n = g n

Tactic:
simpa only [Pi.sub_apply, sub_eq_zero]
    using (LSeries_eventually_eq_zero_iff'.mp hsub).resolve_right ha n hn

Premises used: LSeries_eventually_eq_zero_iff', sub_eq_zero, Iff.mp, Or.resolve_right, Pi.sub_apply
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
⊢ LSeries f = LSeries g ↔ ∀ (n : ℕ), n ≠ 0 → f n = g n

Tactic:
⟨fun H n hn ↦ ?_, fun H ↦ funext (LSeries_congr fun {n} ↦ H n)⟩

Premises used: LSeries_congr, funext, Iff.intro
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
refine : ∀ (H : LSeries f = LSeries g) (n : ℕ) (hn : n ≠ 0), f n = g n
⊢ LSeries f = LSeries g ↔ ∀ (n : ℕ), n ≠ 0 → f n = g n

Tactic:
refine ⟨fun H n hn ↦ ?_, fun H ↦ funext (LSeries_congr fun {n} ↦ H n)⟩
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
H : LSeries f = LSeries g
n : ℕ
hn : n ≠ 0
⊢ f n = g n

Tactic:
eq_of_LSeries_eventually_eq hf hg ?_ hn

Premises used: LSeries.eq_of_LSeries_eventually_eq
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
H : LSeries f = LSeries g
n : ℕ
hn : n ≠ 0
refine : Filter.EventuallyEq (β := ℂ) Filter.atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) fun (x : ℝ) ↦ LSeries g (↑x : ℂ)
⊢ f n = g n

Tactic:
refine eq_of_LSeries_eventually_eq hf hg ?_ hn

Premises used: LSeries.eq_of_LSeries_eventually_eq
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
H : LSeries f = LSeries g
n : ℕ
hn : n ≠ 0
⊢ Filter.EventuallyEq (β := ℂ) Filter.atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) fun (x : ℝ) ↦ LSeries g (↑x : ℂ)

Tactic:
Filter.Eventually.of_forall fun x ↦ congr_fun H x

Premises used: Filter.EventuallyEq, Filter.Eventually.of_forall, Complex.ofReal, congr_fun
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
H : LSeries f = LSeries g
n : ℕ
hn : n ≠ 0
⊢ Filter.EventuallyEq (β := ℂ) Filter.atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) fun (x : ℝ) ↦ LSeries g (↑x : ℂ)

Tactic:
exact Filter.Eventually.of_forall fun x ↦ congr_fun H x

Premises used: Filter.Eventually.of_forall, congr_fun
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
g : ℕ → ℂ
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
h : LSeries f = LSeries g
⊢ ∀ (n : ℕ), n ≠ 0 → f n = g n

Tactic:
replace h := (LSeries_eq_iff_of_abscissaOfAbsConv_lt_top hf.2 hg.2).mp h
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
g : ℕ → ℂ
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
h : ∀ (n : ℕ), n ≠ 0 → f n = g n
h₁ : ∀ (n : ℕ), f n = g n
⊢ f = g

Tactic:
ext1 n
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
g : ℕ → ℂ
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
h : ∀ (n : ℕ), n ≠ 0 → f n = g n
⊢ f 0 = g 0

Tactic:
hf.1.trans hg.1.symm

Premises used: And.left, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
g : ℕ → ℂ
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
h : ∀ (n : ℕ), n ≠ 0 → f n = g n
⊢ f 0 = g 0

Tactic:
exact hf.1.trans hg.1.symm

Premises used: And.left, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
g : ℕ → ℂ
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
h : ∀ (n : ℕ), n ≠ 0 → f n = g n
n : ℕ
⊢ f (n + 1) = g (n + 1)

Tactic:
h _ n.zero_ne_add_one.symm

Premises used: Ne.symm, Nat.zero_ne_add_one
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
g : ℕ → ℂ
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
h : ∀ (n : ℕ), n ≠ 0 → f n = g n
n : ℕ
⊢ f (n + 1) = g (n + 1)

Tactic:
exact h _ n.zero_ne_add_one.symm

Premises used: Ne.symm, Nat.zero_ne_add_one
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
g : ℕ → ℂ
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
h : ∀ (n : ℕ), n ≠ 0 → f n = g n
n : ℕ
h₁ : f 0 = g 0
h₂ : ∀ (n : ℕ), f (n + 1) = g (n + 1)
⊢ f n = g n

Tactic:
cases n with
  | zero => exact hf.1.trans hg.1.symm
  | succ n => exact h _ n.zero_ne_add_one.symm

Premises used: Ne.symm, And.left, Eq.symm, Eq.trans, Nat.zero_ne_add_one
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f g : ℕ → ℂ
s : ℂ
h : term (f + g) s 0 = (term f s + term g s) 0
h₁ : ∀ (n : ℕ), term (f + g) s (n + 1) = (term f s + term g s) (n + 1)
⊢ term (f + g) s = term f s + term g s

Tactic:
ext ⟨- | n⟩
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f g : ℕ → ℂ
s : ℂ
⊢ term (f + g) s 0 = (term f s + term g s) 0

Tactic:
simp [add_div]

Premises used: add_div
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term (f + g) s (n + 1) = (term f s + term g s) (n + 1)

Tactic:
simp [add_div]

Premises used: add_div
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term (f + g) s n = term f s n + term g s n

Tactic:
simp [term_add]

Premises used: LSeries.term_add
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f g : ℕ → ℂ
s a b : ℂ
hf : LSeriesHasSum f s a
hg : LSeriesHasSum g s b
⊢ LSeriesHasSum (f + g) s (a + b)

Tactic:
simpa [LSeriesHasSum, term_add] using HasSum.add hf hg

Premises used: HasSum.add, LSeriesHasSum, LSeries.term_add
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ LSeriesSummable (f + g) s

Tactic:
simpa [LSeriesSummable, ← term_add_apply] using Summable.add hf hg

Premises used: Summable.add, LSeries.term_add_apply, LSeriesSummable
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ LSeries (f + g) s = LSeries f s + LSeries g s

Tactic:
simpa [LSeries, term_add] using hf.tsum_add hg

Premises used: LSeries, LSeries.term_add, Summable.tsum_add
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f : ℕ → ℂ
s : ℂ
h : term (-f) s 0 = (-term f s) 0
h₁ : ∀ (n : ℕ), term (-f) s (n + 1) = (-term f s) (n + 1)
⊢ term (-f) s = -term f s

Tactic:
ext ⟨- | n⟩
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f : ℕ → ℂ
s : ℂ
⊢ term (-f) s 0 = (-term f s) 0

Tactic:
simp [neg_div]

Premises used: neg_div
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term (-f) s (n + 1) = (-term f s) (n + 1)

Tactic:
simp [neg_div]

Premises used: neg_div
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term (-f) s n = -term f s n

Tactic:
simp [term_neg]

Premises used: LSeries.term_neg
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f : ℕ → ℂ
s a : ℂ
hf : LSeriesHasSum f s a
⊢ LSeriesHasSum (-f) s (-a)

Tactic:
simpa [LSeriesHasSum, term_neg] using HasSum.neg hf

Premises used: LSeriesHasSum, LSeries.term_neg, HasSum.neg
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
⊢ LSeriesSummable (-f) s

Tactic:
simpa [LSeriesSummable, term_neg] using Summable.neg hf

Premises used: Summable.neg, LSeries.term_neg, LSeriesSummable
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f : ℕ → ℂ
s : ℂ
⊢ LSeriesSummable (-f) s ↔ LSeriesSummable f s

Tactic:
⟨fun H ↦ neg_neg f ▸ H.neg, .neg⟩

Premises used: Eq.rec, neg_neg, Iff.intro, LSeriesSummable.neg
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f : ℕ → ℂ
s : ℂ
⊢ LSeries (-f) s = -LSeries f s

Tactic:
simp [LSeries, term_neg_apply, tsum_neg]

Premises used: LSeries, LSeries.term_neg_apply, tsum_neg
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f g : ℕ → ℂ
s : ℂ
simp_rw : term (f + -g) s = term f s + -term g s
simp_rw₁ : term f s + term (-g) s = term f s + -term g s
⊢ term (f - g) s = term f s - term g s

Tactic:
simp_rw [sub_eq_add_neg, term_add, term_neg]

Premises used: sub_eq_add_neg, LSeries.term_neg, LSeries.term_add
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
rw : (term f s - term g s) n = term f s n - term g s n
rw₁ rw₂ : term f s n - term g s n = term f s n - term g s n
⊢ term (f - g) s n = term f s n - term g s n

Tactic:
rw [term_sub, Pi.sub_apply]

Premises used: LSeries.term_sub, Pi.sub_apply
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f g : ℕ → ℂ
s a b : ℂ
hf : LSeriesHasSum f s a
hg : LSeriesHasSum g s b
⊢ LSeriesHasSum (f - g) s (a - b)

Tactic:
simpa [LSeriesHasSum, term_sub] using HasSum.sub hf hg

Premises used: LSeries.term_sub, LSeriesHasSum, HasSum.sub
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ LSeriesSummable (f - g) s

Tactic:
simpa [LSeriesSummable, ← term_sub_apply] using Summable.sub hf hg

Premises used: Summable.sub, LSeries.term_sub_apply, LSeriesSummable
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ LSeries (f - g) s = LSeries f s - LSeries g s

Tactic:
simpa [LSeries, term_sub] using hf.tsum_sub hg

Premises used: LSeries.term_sub, LSeries, Summable.tsum_sub
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f : ℕ → ℂ
c s : ℂ
h : term (c • f) s 0 = (c • term f s) 0
h₁ : ∀ (n : ℕ), term (c • f) s (n + 1) = (c • term f s) (n + 1)
⊢ term (c • f) s = c • term f s

Tactic:
ext ⟨- | n⟩
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f : ℕ → ℂ
c s : ℂ
⊢ term (c • f) s 0 = (c • term f s) 0

Tactic:
simp [mul_div_assoc]

Premises used: mul_div_assoc
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f : ℕ → ℂ
c s : ℂ
n : ℕ
⊢ term (c • f) s (n + 1) = (c • term f s) (n + 1)

Tactic:
simp [mul_div_assoc]

Premises used: mul_div_assoc
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f : ℕ → ℂ
c s : ℂ
n : ℕ
⊢ term (c • f) s n = c * term f s n

Tactic:
simp [term_smul]

Premises used: LSeries.term_smul
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f : ℕ → ℂ
c s a : ℂ
hf : LSeriesHasSum f s a
⊢ LSeriesHasSum (c • f) s (c * a)

Tactic:
simpa [LSeriesHasSum, term_smul] using hf.const_smul c

Premises used: LSeriesHasSum, LSeries.term_smul, HasSum.const_smul
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f : ℕ → ℂ
c s : ℂ
hf : LSeriesSummable f s
⊢ LSeriesSummable (c • f) s

Tactic:
simpa [LSeriesSummable, term_smul] using hf.const_smul c

Premises used: Summable.const_smul, LSeries.term_smul, LSeriesSummable
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f : ℕ → ℂ
c s : ℂ
hc : c ≠ 0
hf : LSeriesSummable (c • f) s
⊢ LSeriesSummable f s

Tactic:
simpa [hc] using hf.smul (c⁻¹)

Premises used: LSeriesSummable.smul, Inv.inv