-- Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
/-- As `x → 0`, we have `f x = x ^ (-P.k) • constant` up to a rapidly decaying error. -/
lemma hf_zero (P : WeakFEPair E) (r : ℝ) :
    (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) =O[𝓝[>] 0] (· ^ r)

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
⊢ ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖

Tactic:
simp_rw [Function.comp_apply, ← one_div, P.h_feq' _ hx] at hC'

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖(P.ε⁻¹ * ↑(x ^ P.k)) • P.f x - P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖
⊢ ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖

Proof state:
case h.e'_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖
⊢ ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ = ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖

Tactic:
congr 3

Result:
case h.e'_3.e_a.e_a.e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖
⊢ P.ε * ↑(x ^ (-P.k)) = (P.ε⁻¹ * ↑(x ^ P.k))⁻¹

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
x : ℝ
hC' : x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
hx : 0 < x
⊢ ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖

Tactic:
have h_nv2 : ↑(x ^ P.k) ≠ (0 : ℂ) := ofReal_ne_zero.mpr (rpow_pos_of_pos hx _).ne'

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
x : ℝ
hC' : x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
⊢ ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
x : ℝ
hC' : x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
⊢ ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖

Tactic:
have h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0 := mul_ne_zero P.symm.hε h_nv2

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
x : ℝ
hC' : x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
⊢ ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖

Proof state:
case h.e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖
⊢ ‖P.ε‖ * C * x ^ r * x ^ P.k = C * (x ^ r * x ^ P.k) * ‖P.ε‖

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖
⊢ ‖P.ε‖ * C * ‖x ^ r‖ = C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖

Tactic:
simp_rw [norm_mul, norm_real, one_div, inv_rpow hx.le, rpow_neg hx.le, inv_inv, norm_inv,
  norm_of_nonneg (rpow_pos_of_pos hx _).le, rpow_add hx]

Result:
case h.e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖
⊢ ‖P.ε‖ * C * x ^ r = C * (x ^ r * x ^ P.k) / (‖P.ε‖⁻¹ * x ^ P.k)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r : ℝ
this : ((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) =O[𝓝[>] 0] ((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹)
⊢ (fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) =O[𝓝[>] 0] fun x => x ^ r

Tactic:
simp_rw [IsBigO, IsBigOWith, eventually_nhdsWithin_iff] at this ⊢

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r : ℝ
this :
  ∃ c,
    ∀ᶠ (x : ℝ) in 𝓝 0,
      x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ c * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
⊢ ∃ c, ∀ᶠ (x : ℝ) in 𝓝 0, x ∈ Ioi 0 → ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ c * ‖x ^ r‖

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
⊢ ∀ᶠ (x : ℝ) in 𝓝 0, x ∈ Ioi 0 → ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖

Tactic:
filter_upwards [hC] with x hC' (hx : 0 < x)

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
x : ℝ
hC' : x ∈ Ioi 0 → ‖((fun x => P.g x - P.g₀) ∘ fun x => x⁻¹) x‖ ≤ C * ‖((fun x => x ^ (-(r + P.k))) ∘ fun x => x⁻¹) x‖
hx : 0 < x
⊢ ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖