awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ (↑P.k : ℂ) ∨ P.g₀ = 0
⊢ DifferentiableAt ℂ P.Λ s
have refine_1 : DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (1 / s) • P.f₀) s
Tactic: refine ((P.differentiable_Λ₀ s).sub ?_).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
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ (↑P.k : ℂ) ∨ P.g₀ = 0
refine_1 : DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (1 / s) • P.f₀) s
⊢ DifferentiableAt ℂ P.Λ s
have refine_2 : DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) s
Tactic: refine ((P.differentiable_Λ₀ s).sub ?_).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
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ (↑P.k : ℂ) ∨ P.g₀ = 0
⊢ DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (1 / s) • P.f₀) s
have refine_1 : ∀ (hs : s ≠ 0), DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (1 / s) • P.f₀) s
Tactic: rcases hs with hs | hs
Cleared hypotheses: hs
-- 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
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ (↑P.k : ℂ) ∨ P.g₀ = 0
refine_1 : ∀ (hs : s ≠ 0), DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (1 / s) • P.f₀) s
⊢ DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (1 / s) • P.f₀) s
have refine_1₁ : ∀ (hs : P.f₀ = 0), DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (1 / s) • P.f₀) s
Tactic: rcases hs with hs | hs
Cleared hypotheses: hs
-- 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
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ (↑P.k : ℂ) ∨ P.g₀ = 0
⊢ DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) s
have refine_2 : ∀ (hs' : s ≠ (↑P.k : ℂ)), DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) s
Tactic: rcases hs' with hs' | hs'
Cleared hypotheses: hs'
-- 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
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ (↑P.k : ℂ) ∨ P.g₀ = 0
refine_2 :
  ∀ (hs' : s ≠ (↑P.k : ℂ)), DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) s
⊢ DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) s
have refine_2₁ : ∀ (hs' : P.g₀ = 0), DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) s
Tactic: rcases hs' with hs' | hs'
Cleared hypotheses: hs'
-- 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
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ (↑P.k : ℂ)
⊢ DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) s
have refine_2 : DifferentiableAt ℂ (F := ℂ) (fun (y : ℂ) ↦ P.ε / ((↑P.k : ℂ) - y)) s
Tactic: apply DifferentiableAt.smul_const
-- 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
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ (↑P.k : ℂ)
⊢ DifferentiableAt ℂ (F := ℂ) (fun (y : ℂ) ↦ P.ε / ((↑P.k : ℂ) - y)) s
have refine_2 : (↑P.k : ℂ) - s ≠ 0
Tactic: apply (differentiableAt_const _).div ((differentiableAt_const _).sub (differentiable_id _))
-- 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
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
⊢ HasMellin (fun (x : ℝ) ↦ P.f x - P.f₀) s (P.Λ s)
have hc1 : MellinConvergent.{u_1} (E := E) (fun (x : ℝ) ↦ P.f x - P.f₀) s
Tactic: have hc1 : MellinConvergent (P.f · - P.f₀) s :=
    let ⟨_, ht⟩ := exists_gt s.re
    mellinConvergent_of_isBigO_rpow (P.hf_int.sub (locallyIntegrableOn_const _)) (P.hf_top _) ht
      P.hf_zero' hs
-- 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
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent.{u_1} (E := E) (fun (x : ℝ) ↦ P.f x - P.f₀) s
⊢ HasMellin (fun (x : ℝ) ↦ P.f x - P.f₀) s (P.Λ s)
have refine : mellin (fun (x : ℝ) ↦ P.f x - P.f₀) s = P.Λ s
Tactic: refine ⟨hc1, ?_⟩
-- 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
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent.{u_1} (E := E) (fun (x : ℝ) ↦ P.f x - P.f₀) s
⊢ mellin (fun (x : ℝ) ↦ P.f x - P.f₀) s = P.Λ s
have hc2 : HasMellin P.f_modif s (P.Λ₀ s)
Tactic: have hc2 : HasMellin P.f_modif s (P.Λ₀ s) := P.toStrongFEPair.hasMellin s
-- 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
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent.{u_1} (E := E) (fun (x : ℝ) ↦ P.f x - P.f₀) s
hc2 : HasMellin P.f_modif s (P.Λ₀ s)
⊢ mellin (fun (x : ℝ) ↦ P.f x - P.f₀) s = P.Λ s
have hc3 : mellin (fun (x : ℝ) ↦ P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
Tactic: have hc3 : mellin (fun x ↦ f_modif P x - f P x + P.f₀) s =
    (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀ := P.f_modif_aux2 hs
-- 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
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent.{u_1} (E := E) (fun (x : ℝ) ↦ P.f x - P.f₀) s
hc2 : HasMellin P.f_modif s (P.Λ₀ s)
hc3 : mellin (fun (x : ℝ) ↦ P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
⊢ mellin (fun (x : ℝ) ↦ P.f x - P.f₀) s = P.Λ s
have this : mellin (fun (t : ℝ) ↦ P.f_modif t - (P.f t - P.f₀)) s = mellin P.f_modif s - mellin (fun (x : ℝ) ↦ P.f x - P.f₀) s
Tactic: have := (hasMellin_sub hc2.1 hc1).2
-- 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
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent.{u_1} (E := E) (fun (x : ℝ) ↦ P.f x - P.f₀) s
hc2 : HasMellin P.f_modif s (P.Λ₀ s)
hc3 : mellin (fun (x : ℝ) ↦ P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
this :
  mellin (fun (t : ℝ) ↦ P.f_modif t - (P.f t - P.f₀)) s = mellin P.f_modif s - mellin (fun (x : ℝ) ↦ P.f x - P.f₀) s
⊢ mellin (fun (x : ℝ) ↦ P.f x - P.f₀) s = P.Λ s
have this₁ : mellin (fun (x : ℝ) ↦ P.f x - P.f₀) s = mellin P.f_modif s - (1 / s) • P.f₀ - (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
Tactic: simp_rw [← sub_add, hc3, eq_sub_iff_add_eq, ← eq_sub_iff_add_eq', ← sub_sub] at this
Cleared hypotheses: this
-- 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
s : ℂ
⊢ P.Λ ((↑P.k : ℂ) - s) = P.ε • P.symm.Λ s
have a : P.Λ ((↑P.k : ℂ) - s) +
      (P.ε • P.symm.Λ₀ s + P.Λ₀ ((↑P.k : ℂ) - s) +
          P.ε • (P.symm.Λ s + (1 / s) • P.g₀ + (P.ε⁻¹ / ((↑P.k : ℂ) - s)) • P.f₀) +
        (1 / ((↑P.k : ℂ) - s)) • P.f₀) -
    (P.ε • P.symm.Λ s +
      (P.Λ₀ ((↑P.k : ℂ) - s) +
            (P.Λ ((↑P.k : ℂ) - s) + (1 / ((↑P.k : ℂ) - s)) • P.f₀ + (P.ε / ((↑P.k : ℂ) - ((↑P.k : ℂ) - s))) • P.g₀) +
          P.ε • P.symm.Λ₀ s +
        (P.ε * P.ε⁻¹ / ((↑P.k : ℂ) - s)) • P.f₀)) =
  0
Tactic: linear_combination (norm := module) P.functional_equation₀ s - P.Λ₀_eq (P.k - s)
    + congr(P.ε • $(P.symm_Λ₀_eq s)) + congr(($(mul_inv_cancel₀ P.hε) / ((P.k:ℂ) - s)) • 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
⊢ Tendsto (fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • P.Λ s) (𝓝[≠] (↑P.k : ℂ)) (𝓝 (P.ε • P.g₀))
have simp_rw : Tendsto
  (fun (s : ℂ) ↦
    (s - (↑P.k : ℂ)) • P.Λ₀ s - (s - (↑P.k : ℂ)) • (1 / s) • P.f₀ - (s - (↑P.k : ℂ)) • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀)
  (𝓝[≠] (↑P.k : ℂ)) (𝓝 (HSub.hSub (α := E) 0 0 - -P.ε • P.g₀))
Tactic: simp_rw [Λ, smul_sub, (by simp : 𝓝 (P.ε • P.g₀) = 𝓝 (0 - 0 - -P.ε • P.g₀))]
-- 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
⊢ Tendsto
    (fun (s : ℂ) ↦
      (s - (↑P.k : ℂ)) • P.Λ₀ s - (s - (↑P.k : ℂ)) • (1 / s) • P.f₀ -
        (s - (↑P.k : ℂ)) • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀)
    (𝓝[≠] (↑P.k : ℂ)) (𝓝 (HSub.hSub (α := E) 0 0 - -P.ε • P.g₀))
have refine_1 : Tendsto.{0, u_1} (β := E) (fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • P.Λ₀ s) (𝓝 (↑P.k : ℂ)) (𝓝 0)
Tactic: refine ((Tendsto.sub ?_ ?_).mono_left nhdsWithin_le_nhds).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 : Tendsto.{0, u_1} (β := E) (fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • P.Λ₀ s) (𝓝 (↑P.k : ℂ)) (𝓝 0)
⊢ Tendsto
    (fun (s : ℂ) ↦
      (s - (↑P.k : ℂ)) • P.Λ₀ s - (s - (↑P.k : ℂ)) • (1 / s) • P.f₀ -
        (s - (↑P.k : ℂ)) • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀)
    (𝓝[≠] (↑P.k : ℂ)) (𝓝 (HSub.hSub (α := E) 0 0 - -P.ε • P.g₀))
have refine_2 : Tendsto.{0, u_1} (β := E) (fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • (1 / s) • P.f₀) (𝓝 (↑P.k : ℂ)) (𝓝 0)
Tactic: refine ((Tendsto.sub ?_ ?_).mono_left nhdsWithin_le_nhds).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 : Tendsto.{0, u_1} (β := E) (fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • P.Λ₀ s) (𝓝 (↑P.k : ℂ)) (𝓝 0)
refine_2 : Tendsto.{0, u_1} (β := E) (fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • (1 / s) • P.f₀) (𝓝 (↑P.k : ℂ)) (𝓝 0)
⊢ Tendsto
    (fun (s : ℂ) ↦
      (s - (↑P.k : ℂ)) • P.Λ₀ s - (s - (↑P.k : ℂ)) • (1 / s) • P.f₀ -
        (s - (↑P.k : ℂ)) • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀)
    (𝓝[≠] (↑P.k : ℂ)) (𝓝 (HSub.hSub (α := E) 0 0 - -P.ε • P.g₀))
have refine_3 : Tendsto (fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) (𝓝[≠] (↑P.k : ℂ)) (𝓝 (-P.ε • P.g₀))
Tactic: refine ((Tendsto.sub ?_ ?_).mono_left nhdsWithin_le_nhds).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
⊢ 𝓝 0 = 𝓝 (((↑P.k : ℂ) - (↑P.k : ℂ)) • P.Λ₀ (↑P.k : ℂ))
have rw : 𝓝 0 = 𝓝 (HSMul.hSMul (α := ℂ) 0 (P.Λ₀ (↑P.k : ℂ)))
Tactic: rw [sub_self, zero_smul]
-- 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
rw : 𝓝 0 = 𝓝 (HSMul.hSMul (α := ℂ) 0 (P.Λ₀ (↑P.k : ℂ)))
⊢ 𝓝 0 = 𝓝 (((↑P.k : ℂ) - (↑P.k : ℂ)) • P.Λ₀ (↑P.k : ℂ))
have rw₁ : Eq.{u_1 + 1} (α := Filter E) (𝓝 0) (𝓝 0)
Tactic: rw [sub_self, zero_smul]
-- 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
⊢ Tendsto.{0, u_1} (β := E) (fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • P.Λ₀ s) (𝓝 (↑P.k : ℂ)) (𝓝 0)
have refine_1 : Tendsto (fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • P.Λ₀ s) (𝓝 (↑P.k : ℂ)) (𝓝 (((↑P.k : ℂ) - (↑P.k : ℂ)) • P.Λ₀ (↑P.k : ℂ)))
Tactic: rw [(by rw [sub_self, zero_smul] : 𝓝 0 = 𝓝 ((P.k - P.k : ℂ) • P.Λ₀ P.k))]
-- 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
⊢ 𝓝 0 = 𝓝 (((↑P.k : ℂ) - (↑P.k : ℂ)) • (1 / (↑P.k : ℂ)) • P.f₀)
have rw : 𝓝 0 = 𝓝 (HSMul.hSMul (α := ℂ) 0 ((1 / (↑P.k : ℂ)) • P.f₀))
Tactic: rw [sub_self, zero_smul]
-- 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
rw : 𝓝 0 = 𝓝 (HSMul.hSMul (α := ℂ) 0 ((1 / (↑P.k : ℂ)) • P.f₀))
⊢ 𝓝 0 = 𝓝 (((↑P.k : ℂ) - (↑P.k : ℂ)) • (1 / (↑P.k : ℂ)) • P.f₀)
have rw₁ : Eq.{u_1 + 1} (α := Filter E) (𝓝 0) (𝓝 0)
Tactic: rw [sub_self, zero_smul]
-- 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
⊢ Tendsto.{0, u_1} (β := E) (fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • (1 / s) • P.f₀) (𝓝 (↑P.k : ℂ)) (𝓝 0)
have refine_2 : Tendsto (fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • (1 / s) • P.f₀) (𝓝 (↑P.k : ℂ))
  (𝓝 (((↑P.k : ℂ) - (↑P.k : ℂ)) • (1 / (↑P.k : ℂ)) • P.f₀))
Tactic: rw [(by rw [sub_self, zero_smul] : 𝓝 0 = 𝓝 ((P.k - P.k : ℂ) • (1 / P.k : ℂ) • 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
⊢ Tendsto (fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • (1 / s) • P.f₀) (𝓝 (↑P.k : ℂ))
    (𝓝 (((↑P.k : ℂ) - (↑P.k : ℂ)) • (1 / (↑P.k : ℂ)) • P.f₀))
have refine_2 : ContinuousAt (HDiv.hDiv (α := ℂ) 1) (↑P.k : ℂ)
Tactic: refine (continuous_sub_right _).continuousAt.smul (ContinuousAt.smul ?_ continuousAt_const)
-- 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
⊢ ContinuousAt (HDiv.hDiv (α := ℂ) 1) (↑P.k : ℂ)
have this : (↑P.k : ℂ) ≠ 0
Tactic: have := ofReal_ne_zero.mpr P.hk.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
⊢ Tendsto (fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) (𝓝[≠] (↑P.k : ℂ)) (𝓝 (-P.ε • P.g₀))
have refine_3 : EventuallyEq.{0, u_1} (β := E) (𝓝[≠] (↑P.k : ℂ)) (fun (x : ℂ) ↦ -P.ε • P.g₀) fun (s : ℂ) ↦
  (s - (↑P.k : ℂ)) • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
Tactic: refine (tendsto_const_nhds.mono_left nhdsWithin_le_nhds).congr' ?_
-- 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
⊢ EventuallyEq.{0, u_1} (β := E) (𝓝[≠] (↑P.k : ℂ)) (fun (x : ℂ) ↦ -P.ε • P.g₀) fun (s : ℂ) ↦
    (s - (↑P.k : ℂ)) • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
have refine_3 : ∀ (s : ℂ) (hs : s ≠ (↑P.k : ℂ)),
  Eq.{u_1 + 1} (α := E) ((fun (x : ℂ) ↦ -P.ε • P.g₀) s)
    ((fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) s)
Tactic: refine eventually_nhdsWithin_of_forall (fun s (hs : s ≠ P.k) ↦ ?_)
-- 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
s : ℂ
hs : s ≠ (↑P.k : ℂ)
⊢ Eq.{u_1 + 1} (α := E) ((fun (x : ℂ) ↦ -P.ε • P.g₀) s)
    ((fun (s : ℂ) ↦ (s - (↑P.k : ℂ)) • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) s)
have match_scalars : -P.ε * 1 = (s - (↑P.k : ℂ)) * (P.ε / ((↑P.k : ℂ) - s) * 1)
Tactic: match_scalars
-- 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
⊢ Tendsto (fun (s : ℂ) ↦ s • P.Λ s) (𝓝[≠] 0) (𝓝 (-P.f₀))
have simp_rw : Tendsto (fun (s : ℂ) ↦ s • P.Λ₀ s - s • (1 / s) • P.f₀ - s • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) (𝓝[≠] 0)
  (𝓝 (HSMul.hSMul (α := ℂ) 0 (P.Λ₀ 0) - P.f₀ - 0))
Tactic: simp_rw [Λ, smul_sub, (by simp : 𝓝 (-P.f₀) = 𝓝 (((0 : ℂ) • P.Λ₀ 0) - P.f₀ - 0))]
-- 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
⊢ Tendsto (fun (s : ℂ) ↦ s • P.Λ₀ s - s • (1 / s) • P.f₀ - s • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) (𝓝[≠] 0)
    (𝓝 (HSMul.hSMul (α := ℂ) 0 (P.Λ₀ 0) - P.f₀ - 0))
have refine_1 : Tendsto (fun (s : ℂ) ↦ s • P.Λ₀ s) (𝓝 0) (𝓝 (HSMul.hSMul (α := ℂ) 0 (P.Λ₀ 0)))
Tactic: refine ((Tendsto.mono_left ?_ nhdsWithin_le_nhds).sub ?_).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 : Tendsto (fun (s : ℂ) ↦ s • P.Λ₀ s) (𝓝 0) (𝓝 (HSMul.hSMul (α := ℂ) 0 (P.Λ₀ 0)))
⊢ Tendsto (fun (s : ℂ) ↦ s • P.Λ₀ s - s • (1 / s) • P.f₀ - s • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) (𝓝[≠] 0)
    (𝓝 (HSMul.hSMul (α := ℂ) 0 (P.Λ₀ 0) - P.f₀ - 0))
have refine_2 : Tendsto (fun (s : ℂ) ↦ s • (1 / s) • P.f₀) (𝓝[≠] 0) (𝓝 P.f₀)
Tactic: refine ((Tendsto.mono_left ?_ nhdsWithin_le_nhds).sub ?_).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 : Tendsto (fun (s : ℂ) ↦ s • P.Λ₀ s) (𝓝 0) (𝓝 (HSMul.hSMul (α := ℂ) 0 (P.Λ₀ 0)))
refine_2 : Tendsto (fun (s : ℂ) ↦ s • (1 / s) • P.f₀) (𝓝[≠] 0) (𝓝 P.f₀)
⊢ Tendsto (fun (s : ℂ) ↦ s • P.Λ₀ s - s • (1 / s) • P.f₀ - s • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) (𝓝[≠] 0)
    (𝓝 (HSMul.hSMul (α := ℂ) 0 (P.Λ₀ 0) - P.f₀ - 0))
have refine_3 : Tendsto.{0, u_1} (β := E) (fun (s : ℂ) ↦ s • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) (𝓝[≠] 0) (𝓝 0)
Tactic: refine ((Tendsto.mono_left ?_ nhdsWithin_le_nhds).sub ?_).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
⊢ Tendsto (fun (s : ℂ) ↦ s • (1 / s) • P.f₀) (𝓝[≠] 0) (𝓝 P.f₀)
have refine_2 : EventuallyEq.{0, u_1} (β := E) (𝓝[≠] 0) (fun (x : ℂ) ↦ P.f₀) fun (s : ℂ) ↦ s • (1 / s) • P.f₀
Tactic: refine (tendsto_const_nhds.mono_left nhdsWithin_le_nhds).congr' ?_
-- 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
⊢ EventuallyEq.{0, u_1} (β := E) (𝓝[≠] 0) (fun (x : ℂ) ↦ P.f₀) fun (s : ℂ) ↦ s • (1 / s) • P.f₀
have refine_2 : ∀ (s : ℂ) (hs : s ≠ 0), Eq.{u_1 + 1} (α := E) ((fun (x : ℂ) ↦ P.f₀) s) ((fun (s : ℂ) ↦ s • (1 / s) • P.f₀) s)
Tactic: refine eventually_nhdsWithin_of_forall (fun s (hs : s ≠ 0) ↦ ?_)
-- 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
s : ℂ
hs : s ≠ 0
⊢ Eq.{u_1 + 1} (α := E) ((fun (x : ℂ) ↦ P.f₀) s) ((fun (s : ℂ) ↦ s • (1 / s) • P.f₀) s)
have match_scalars : 1 = s * (1 / s * 1)
Tactic: match_scalars
-- 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
⊢ 𝓝 0 = 𝓝 (HSMul.hSMul (α := ℂ) 0 ((P.ε / ((↑P.k : ℂ) - 0)) • P.g₀))
have rw : Eq.{u_1 + 1} (α := Filter E) (𝓝 0) (𝓝 0)
Tactic: rw [zero_smul]
-- 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
⊢ Tendsto.{0, u_1} (β := E) (fun (s : ℂ) ↦ s • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) (𝓝[≠] 0) (𝓝 0)
have refine_3 : Tendsto (fun (s : ℂ) ↦ s • (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) (𝓝[≠] 0)
  (𝓝 (HSMul.hSMul (α := ℂ) 0 ((P.ε / ((↑P.k : ℂ) - 0)) • P.g₀)))
Tactic: rw [show 𝓝 0 = 𝓝 ((0 : ℂ) • (P.ε / (P.k - 0 : ℂ)) • P.g₀) by rw [zero_smul]]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
s : ℂ
n : ℕ
⊢ (if n = 0 then 0 else f n / HPow.hPow (α := ℂ) (↑n : ℂ) s) = f n * HPow.hPow (α := ℂ) (↑n : ℂ) (-s)
have pos : ∀ (h : n = 0), 0 = f n * HPow.hPow (α := ℂ) (↑n : ℂ) (-s)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
s : ℂ
n : ℕ
pos : ∀ (h : n = 0), 0 = f n * HPow.hPow (α := ℂ) (↑n : ℂ) (-s)
⊢ (if n = 0 then 0 else f n / HPow.hPow (α := ℂ) (↑n : ℂ) s) = f n * HPow.hPow (α := ℂ) (↑n : ℂ) (-s)
have neg : ∀ (h : ¬n = 0), f n / HPow.hPow (α := ℂ) (↑n : ℂ) s = f n * HPow.hPow (α := ℂ) (↑n : ℂ) (-s)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
n : ℕ
⊢ term f s n = f n / HPow.hPow (α := ℂ) (↑n : ℂ) s
have inl : term f s 0 = f 0 / HPow.hPow (α := ℂ) (↑0 : ℂ) s
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
n : ℕ
inl : term f s 0 = f 0 / HPow.hPow (α := ℂ) (↑0 : ℂ) s
⊢ term f s n = f n / HPow.hPow (α := ℂ) (↑n : ℂ) s
have inr : ∀ (hn : n ≠ 0), term f s n = f n / HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
⊢ term f s 0 = f 0 / HPow.hPow (α := ℂ) (↑0 : ℂ) s
have inl : 0 = f 0 / HPow.hPow (α := ℂ) (↑0 : ℂ) s
Tactic: rw [term_zero, Nat.cast_zero, zero_cpow hs, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
inl : 0 = f 0 / HPow.hPow (α := ℂ) (↑0 : ℂ) s
⊢ term f s 0 = f 0 / HPow.hPow (α := ℂ) (↑0 : ℂ) s
have inl₁ : 0 = f 0 / HPow.hPow (α := ℂ) 0 s
Tactic: rw [term_zero, Nat.cast_zero, zero_cpow hs, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
inl : 0 = f 0 / HPow.hPow (α := ℂ) (↑0 : ℂ) s
inl₁ : 0 = f 0 / HPow.hPow (α := ℂ) 0 s
⊢ term f s 0 = f 0 / HPow.hPow (α := ℂ) (↑0 : ℂ) s
have inl₂ : 0 = f 0 / 0
Tactic: rw [term_zero, Nat.cast_zero, zero_cpow hs, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
inl : 0 = f 0 / HPow.hPow (α := ℂ) (↑0 : ℂ) s
inl₁ : 0 = f 0 / HPow.hPow (α := ℂ) 0 s
inl₂ : 0 = f 0 / 0
⊢ term f s 0 = f 0 / HPow.hPow (α := ℂ) (↑0 : ℂ) s
have inl₃ : Eq (α := ℂ) 0 0
Tactic: rw [term_zero, Nat.cast_zero, zero_cpow hs, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
n : ℕ
hn : n ≠ 0
⊢ term f s n = f n / HPow.hPow (α := ℂ) (↑n : ℂ) s
have inr : f n / HPow.hPow (α := ℂ) (↑n : ℂ) s = f n / HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: rw [term_of_ne_zero hn]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f g : ℕ → ℂ
h : ∀ {n : ℕ}, n ≠ 0 → f n = g n
s : ℂ
n : ℕ
⊢ term f s n = term g s n
have inl : ∀ (hn : n = 0), term f s n = term g s n
Tactic: rcases eq_or_ne n 0 with hn | hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f g : ℕ → ℂ
h : ∀ {n : ℕ}, n ≠ 0 → f n = g n
s : ℂ
n : ℕ
inl : ∀ (hn : n = 0), term f s n = term g s n
⊢ term f s n = term g s n
have inr : ∀ (hn : n ≠ 0), term f s n = term g s n
Tactic: rcases eq_or_ne n 0 with hn | hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
s : ℂ
n : ℕ
⊢ ‖term f s n‖ = if n = 0 then 0 else ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re
have inl : ‖term f s 0‖ = if Eq (α := ℕ) 0 0 then 0 else ‖f 0‖ / HPow.hPow (α := ℝ) (↑0 : ℝ) s.re
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
s : ℂ
n : ℕ
inl : ‖term f s 0‖ = if Eq (α := ℕ) 0 0 then 0 else ‖f 0‖ / HPow.hPow (α := ℝ) (↑0 : ℝ) s.re
⊢ ‖term f s n‖ = if n = 0 then 0 else ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re
have inr : ∀ (hn : n ≠ 0), ‖term f s n‖ = if n = 0 then 0 else ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
h : ‖f n‖ ≤ ‖g n‖
⊢ ‖term f s n‖ ≤ ‖term g s n‖
have simp : (if n = 0 then 0 else ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re) ≤
  if n = 0 then 0 else ‖g n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re
Tactic: simp only [norm_term_eq]