awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
x : ℝ
hC' :
  Membership.mem (γ := Set ℝ) (Ioi 0) x →
    Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
      C * Norm.norm (E := ℝ) (((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‖
have hC'₁ : Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
  C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
Tactic: specialize hC' hx
Cleared hypotheses: hC'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((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' :
  Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
    C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
⊢ ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
have hC'₁ : ‖(P.ε⁻¹ * (↑(x ^ P.k) : ℂ)) • P.f x - P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖
Tactic: simp_rw [Function.comp_apply, ← one_div, P.h_feq' _ hx] at hC'
Cleared hypotheses: hC'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((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‖
have hC'₁ : ‖P.f x - (P.ε⁻¹ * (↑(x ^ P.k) : ℂ))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * (↑(x ^ P.k) : ℂ)‖
Tactic: rw [← ((mul_inv_cancel₀ h_nv).symm ▸ one_smul ℂ P.g₀ :), mul_smul _ _ P.g₀, ← smul_sub, norm_smul,
    ← le_div_iff₀' (lt_of_le_of_ne (norm_nonneg _) (norm_ne_zero_iff.mpr h_nv).symm)] at hC'
Cleared hypotheses: hC'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((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.ε‖ * C * ‖x ^ r‖
have h : ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ = ‖P.f x - (P.ε⁻¹ * (↑(x ^ P.k) : ℂ))⁻¹ • P.g₀‖
Tactic: convert! hC' using 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((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) : ℂ)‖
h : ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ = ‖P.f x - (P.ε⁻¹ * (↑(x ^ P.k) : ℂ))⁻¹ • P.g₀‖
⊢ ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
have h₁ : ‖P.ε‖ * C * ‖x ^ r‖ = C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * (↑(x ^ P.k) : ℂ)‖
Tactic: convert! hC' using 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((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₀‖
have h : P.ε * (↑(x ^ (-P.k)) : ℂ) = (P.ε⁻¹ * (↑(x ^ P.k) : ℂ))⁻¹
Tactic: congr 3
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((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) : ℂ))⁻¹
have h : P.ε * (↑(x ^ P.k)⁻¹ : ℂ) = (P.ε⁻¹ * (↑(x ^ P.k) : ℂ))⁻¹
Tactic: rw [rpow_neg hx.le]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((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) : ℂ)‖
have h : ‖P.ε‖ * C * x ^ r = C * (x ^ r * x ^ 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ P.f x - P.f₀) fun (x : ℝ) ↦ x ^ (-P.k)
have simp_rw : IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0)
  (fun (x : ℝ) ↦ P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀ + ((P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀ - P.f₀)) fun (x : ℝ) ↦
  x ^ (-P.k)
Tactic: simp_rw [← fun x ↦ sub_add_sub_cancel (P.f x) ((P.ε * ↑(x ^ (-P.k))) • P.g₀) P.f₀]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0)
    (fun (x : ℝ) ↦ P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀ + ((P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀ - P.f₀))
    fun (x : ℝ) ↦ x ^ (-P.k)
have refine_1 : IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) fun (x : ℝ) ↦
  x ^ (-P.k)
Tactic: refine (P.hf_zero _).add (IsBigO.sub ?_ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
refine_1 :
  IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) fun (x : ℝ) ↦
    x ^ (-P.k)
⊢ IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0)
    (fun (x : ℝ) ↦ P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀ + ((P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀ - P.f₀))
    fun (x : ℝ) ↦ x ^ (-P.k)
have refine_2 : IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ P.f₀) fun (x : ℝ) ↦ x ^ (-P.k)
Tactic: refine (P.hf_zero _).add (IsBigO.sub ?_ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) fun (x : ℝ) ↦
    x ^ (-P.k)
have refine_1 : IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ ‖(P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖) fun (x : ℝ) ↦ ‖x ^ (-P.k)‖
Tactic: rw [← isBigO_norm_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ ‖(P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖) fun (x : ℝ) ↦ ‖x ^ (-P.k)‖
have refine_1 : IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ ‖P.ε‖ * ‖P.g₀‖ * ‖x ^ (-P.k)‖) fun (x : ℝ) ↦ ‖x ^ (-P.k)‖
Tactic: simp_rw [mul_smul, norm_smul, mul_comm _ ‖P.g₀‖, ← mul_assoc, norm_real]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ P.f₀) fun (x : ℝ) ↦ x ^ (-P.k)
have refine_2 : ∀ᶠ (x : ℝ) in 𝓝 0, Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖P.f₀‖ ≤ ‖P.f₀‖ * ‖x ^ (-P.k)‖
Tactic: refine IsBigO.of_bound ‖P.f₀‖ (eventually_nhdsWithin_iff.mpr ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx' : x ≤ 1
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖P.f₀‖ ≤ ‖P.f₀‖ * ‖x ^ (-P.k)‖
have h : ∀ (hx : 0 < x), ‖P.f₀‖ ≤ ‖P.f₀‖ * ‖x ^ (-P.k)‖
Tactic: (hx : 0 < x)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ ∀ᶠ (x : ℝ) in 𝓝 0, Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖P.f₀‖ ≤ ‖P.f₀‖ * ‖x ^ (-P.k)‖
have h : ∀ (x : ℝ) (hx' : x ≤ 1) (hx : 0 < x), ‖P.f₀‖ ≤ ‖P.f₀‖ * ‖x ^ (-P.k)‖
Tactic: filter_upwards [eventually_le_nhds zero_lt_one] with x hx' (hx : 0 < x)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx' : x ≤ 1
hx : 0 < x
⊢ ‖P.f₀‖ ≤ ‖P.f₀‖ * ‖x ^ (-P.k)‖
have h : 1 ≤ ‖x ^ (-P.k)‖
Tactic: apply le_mul_of_one_le_right (norm_nonneg _)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx' : x ≤ 1
hx : 0 < x
⊢ 1 ≤ ‖x ^ (-P.k)‖
have h : 1 ≤ (x ^ P.k)⁻¹
Tactic: rw [norm_of_nonneg (rpow_pos_of_pos hx _).le, rpow_neg hx.le]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
⊢ P.Λ ((↑P.k : ℂ) - s) = P.ε • P.symm.Λ s
have rw : mellin P.f ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
Tactic: rw [P.Λ_eq, P.symm_Λ_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
⊢ mellin P.f ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
have step1 : mellin (fun (t : ℝ) ↦ P.g (HPow.hPow (β := ℝ) t (-1))) (-s) =
  HSMul.hSMul (α := ℝ) |(-1)|⁻¹ (mellin P.g (-s / (↑(-1) : ℂ)))
Tactic: have step1 := mellin_comp_rpow P.g (-s) (-1)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 :
  mellin (fun (t : ℝ) ↦ P.g (HPow.hPow (β := ℝ) t (-1))) (-s) =
    HSMul.hSMul (α := ℝ) |(-1)|⁻¹ (mellin P.g (-s / (↑(-1) : ℂ)))
⊢ mellin P.f ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
have step1₁ : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
Tactic: simp_rw [abs_neg, abs_one, inv_one, one_smul, ofReal_neg, ofReal_one, div_neg, div_one, neg_neg,
    rpow_neg_one, ← one_div] at step1
Cleared hypotheses: step1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
⊢ mellin P.f ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
have step2 : Eq.{u_1 + 1} (α := E) (mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s))
  (mellin (fun (t : ℝ) ↦ P.g (1 / t)) ((↑P.k : ℂ) - s + -(↑P.k : ℂ)))
Tactic: have step2 := mellin_cpow_smul (fun t ↦ P.g (1 / t)) (P.k - s) (-P.k)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 :
  Eq.{u_1 + 1} (α := E) (mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s))
    (mellin (fun (t : ℝ) ↦ P.g (1 / t)) ((↑P.k : ℂ) - s + -(↑P.k : ℂ)))
⊢ mellin P.f ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
have step2₁ : mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = mellin P.g s
Tactic: rw [← sub_eq_add_neg, sub_right_comm, sub_self, zero_sub, step1] at step2
Cleared hypotheses: step2
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = mellin P.g s
⊢ mellin P.f ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
have step3 : mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) =
  HSMul.hSMul (β := E) P.ε (mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s))
Tactic: have step3 := mellin_const_smul (fun t ↦ (t : ℂ) ^ (-P.k : ℂ) • P.g (1 / t)) (P.k - s) P.ε
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = mellin P.g s
step3 :
  mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) =
    HSMul.hSMul (β := E) P.ε (mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s))
⊢ mellin P.f ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
have step3₁ : mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
Tactic: rw [step2] at step3
Cleared hypotheses: step3
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = mellin P.g s
step3 : mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
⊢ mellin P.f ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
have rw : mellin P.f ((↑P.k : ℂ) - s) = mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s)
Tactic: rw [← step3]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = mellin P.g s
step3 : mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
⊢ mellin P.f ((↑P.k : ℂ) - s) = mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s)
have refine : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
  (↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1) • P.f t =
    HSMul.hSMul (β := E) ((↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1))
      ((fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) t)
Tactic: refine setIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = mellin P.g s
step3 : mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ (↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1) • P.f t =
    HSMul.hSMul (β := E) ((↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1))
      ((fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) t)
have simp_rw : (↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1) • P.f t =
  ((↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1) * (P.ε * ((↑t : ℂ) ^ (-(↑P.k : ℂ)) * (P.ε⁻¹ * (↑(t ^ P.k) : ℂ))))) • P.f t
Tactic: simp_rw [P.h_feq' t ht, ← mul_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = mellin P.g s
step3 : mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ (↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1) • P.f t =
    ((↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1) * (P.ε * ((↑t : ℂ) ^ (-(↑P.k : ℂ)) * (P.ε⁻¹ * (↑(t ^ P.k) : ℂ))))) • P.f t
have rw : (↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1) • P.f t =
  ((↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1) * (P.ε * (((↑t : ℂ) ^ (↑P.k : ℂ))⁻¹ * (P.ε⁻¹ * (↑t : ℂ) ^ (↑P.k : ℂ))))) • P.f t
Tactic: rw [cpow_neg, ofReal_cpow (le_of_lt ht)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = mellin P.g s
step3 : mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ (↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1) • P.f t =
    ((↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1) * (P.ε * (((↑t : ℂ) ^ (↑P.k : ℂ))⁻¹ * (P.ε⁻¹ * (↑t : ℂ) ^ (↑P.k : ℂ))))) • P.f t
have this : (↑t : ℂ) ^ (↑P.k : ℂ) ≠ 0
Tactic: have : (t : ℂ) ^ (P.k : ℂ) ≠ 0 := by simpa [← ofReal_cpow ht.le] using (rpow_pos_of_pos ht _).ne'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ LocallyIntegrableOn.{0, u_1} (ε := E) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) (Ioi 0) volume
have refine : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) (Ioi 0)
Tactic: refine ContinuousOn.locallyIntegrableOn ?_ measurableSet_Ioi
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) (Ioi 0)
have refine : ∀ (x : ℝ) (hx : 0 < x), ContinuousAt.{0, u_1} (Y := E) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) x
Tactic: refine continuousOn_of_forall_continuousAt (fun x (hx : 0 < x) ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
⊢ ContinuousAt.{0, u_1} (Y := E) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) x
have this : x ≠ 0 ∨ 0 ≤ -P.k
Tactic: have : x ≠ 0 ∨ 0 ≤ -P.k := Or.inl hx.ne'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ LocallyIntegrableOn P.f_modif (Ioi 0) volume
have this : LocallyIntegrableOn.{0, u_1} (ε := E) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) (Ioi 0) volume
Tactic: have : LocallyIntegrableOn (fun x : ℝ ↦ (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) := by
    refine ContinuousOn.locallyIntegrableOn ?_ measurableSet_Ioi
    refine continuousOn_of_forall_continuousAt (fun x (hx : 0 < x) ↦ ?_)
    have : x ≠ 0 ∨ 0 ≤ -P.k := Or.inl hx.ne'
    fun_prop
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn.{0, u_1} (ε := E) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) (Ioi 0) volume
⊢ LocallyIntegrableOn P.f_modif (Ioi 0) volume
have refine_1 : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
  IntegrableAtFilter.{0, u_1} (ε := E) (mα := Real.measurableSpace) (indicator (Ioi 1) fun (x : ℝ) ↦ P.f x - P.f₀)
    (𝓝[Ioi 0] x) volume
Tactic: refine LocallyIntegrableOn.add (fun x hx ↦ ?_) (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn.{0, u_1} (ε := E) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) (Ioi 0) volume
refine_1 :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
    IntegrableAtFilter.{0, u_1} (ε := E) (mα := Real.measurableSpace) (indicator (Ioi 1) fun (x : ℝ) ↦ P.f x - P.f₀)
      (𝓝[Ioi 0] x) volume
⊢ LocallyIntegrableOn P.f_modif (Ioi 0) volume
have refine_2 : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
  IntegrableAtFilter.{0, u_1} (ε := E) (mα := Real.measurableSpace)
    (indicator (Ioo 0 1) fun (x : ℝ) ↦ P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) (𝓝[Ioi 0] x) volume
Tactic: refine LocallyIntegrableOn.add (fun x hx ↦ ?_) (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn.{0, u_1} (ε := E) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) (Ioi 0) volume
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ IntegrableAtFilter.{0, u_1} (ε := E) (mα := Real.measurableSpace) (indicator (Ioi 1) fun (x : ℝ) ↦ P.f x - P.f₀)
    (𝓝[Ioi 0] x) volume
have refine_1 : ∀ (s : Set ℝ) (hs : s ∈ 𝓝[Ioi 0] x)
  (hs' : IntegrableOn (mα := Real.measurableSpace) (P.f - fun (x : ℝ) ↦ P.f₀) s volume),
  IntegrableAtFilter.{0, u_1} (ε := E) (mα := Real.measurableSpace) (indicator (Ioi 1) fun (x : ℝ) ↦ P.f x - P.f₀)
    (𝓝[Ioi 0] x) volume
Tactic: obtain ⟨s, hs, hs'⟩ := P.hf_int.sub (locallyIntegrableOn_const _) x hx