-- Mathlib/NumberTheory/LSeries/Injectivity.lean
/-- If the `LSeries` of `f` and of `g` converge somewhere and agree on large real arguments,
then the L-series of `f - g` is zero for large real arguments. -/
lemma LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq {f g : ℕ → ℂ}
    (hf : abscissaOfAbsConv f < ⊤) (hg : abscissaOfAbsConv g < ⊤)
    (h : (fun x : ℝ ↦ LSeries f x) =ᶠ[atTop] fun x ↦ LSeries g x) :
    (fun x : ℝ ↦ LSeries (f - g) x) =ᶠ[atTop] (0 : ℝ → ℂ)

Proof state:
case intro.intro.intro.intro.intro.intro
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
hyf₂ : ↑yf < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b

Tactic:
lift yg to ℝ using ⟨hyg₂.ne, ((OrderBot.bot_le _).trans_lt hyg₁).ne'⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b

Proof state:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : ∃ a, ∀ b ≥ a, LSeries f ↑b = LSeries g ↑b
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b

Tactic:
obtain ⟨x₀, hx₀⟩ := h

Result:
case intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b

Proof state:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x => LSeries f ↑x) =ᶠ[atTop] fun x => LSeries g ↑x
⊢ (fun x => LSeries (f - g) ↑x) =ᶠ[atTop] 0

Tactic:
rw [EventuallyEq, eventually_atTop] at h ⊢

Result:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : ∃ a, ∀ b ≥ a, LSeries f ↑b = LSeries g ↑b
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b

Proof state:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ x₀ ⊔ (yf ⊔ yg)
⊢ LSeriesSummable f ↑x

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

Result:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ x₀ ⊔ (yf ⊔ yg)
⊢ yf ≤ x

Proof state:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ x₀ ⊔ (yf ⊔ yg)
Hf : LSeriesSummable f ↑x
⊢ yg ≤ x

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

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
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 < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b

Tactic:
lift yf to ℝ using ⟨hyf₂.ne, ((OrderBot.bot_le _).trans_lt hyf₁).ne'⟩

Result:
case intro.intro.intro.intro.intro.intro
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
hyf₂ : ↑yf < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b

Proof state:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ x₀ ⊔ (yf ⊔ yg)
Hf : LSeriesSummable f ↑x
⊢ LSeriesSummable g ↑x

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

Result:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ x₀ ⊔ (yf ⊔ yg)
Hf : LSeriesSummable f ↑x
⊢ yg ≤ x

Proof state:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ x₀ ⊔ (yf ⊔ yg)
Hf : LSeriesSummable f ↑x
⊢ LSeries (f - g) ↑x = 0 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

Result:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ x₀ ⊔ (yf ⊔ yg)
Hf : LSeriesSummable f ↑x
Hg : LSeriesSummable g ↑x
⊢ LSeries (f - g) ↑x = 0 x

Proof state:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ x₀ ⊔ (yf ⊔ yg)
Hf : LSeriesSummable f ↑x
Hg : LSeriesSummable g ↑x
⊢ LSeries (f - g) ↑x = 0 x

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

Result:
no goals

Proof state:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ x₀ ⊔ (yf ⊔ yg)
⊢ yf ≤ x

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

Result:
no goals

Proof state:
case intro.intro.intro
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 < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b

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

Result:
case intro.intro.intro.intro.intro
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 < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b