From 72a3e56a4322298f82a2e62fbd2c39f5e0ee8e2c Mon Sep 17 00:00:00 2001
From: L Lllvvuu <git@llllvvuu.dev>
Date: Wed, 31 Jan 2024 22:55:13 -0800
Subject: [PATCH 1/2] feat: `limitOfConstant`

Variant of `tendsto_const_nhds_iff` for `T1Space`
---
 PrimeNumberTheoremAnd/MellinCalculus.lean | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/PrimeNumberTheoremAnd/MellinCalculus.lean b/PrimeNumberTheoremAnd/MellinCalculus.lean
index 68c3a767..b37fd030 100644
--- a/PrimeNumberTheoremAnd/MellinCalculus.lean
+++ b/PrimeNumberTheoremAnd/MellinCalculus.lean
@@ -150,17 +150,17 @@ $\sigma, \sigma'>0$, we have $a(\sigma')=a(\sigma)$, and that
 $\lim_{\sigma\to\infty}a(\sigma)=0$. Then $a(\sigma)=0$.
 \end{lemma}
 %%-/
-lemma limitOfConstant {a : ℝ → ℂ} {σ : ℝ} (σpos : 0 < σ) (ha : ∀ (σ' : ℝ) (σ'' : ℝ) (σ'pos : 0 < σ')
-    (σ''pos : 0 < σ''), a σ' = a σ'') (ha' : Tendsto (fun σ' => a σ') atTop (𝓝 0)) : a σ = 0 := by
-  sorry
+lemma limitOfConstant {a : ℝ → ℂ} {σ : ℝ} (σpos : 0 < σ)
+    (ha : ∀ (σ' : ℝ) (σ'' : ℝ) (_ : 0 < σ') (_ : 0 < σ''), a σ' = a σ'')
+    (ha' : Tendsto a atTop (𝓝 0)) : a σ = 0 := by
 /-%%
-\begin{proof}
-To show that $a(\sigma)=0$, we show that $a(\sigma)< \epsilon$ for all $\epsilon>0$. Let $\epsilon>0$.
-The fact that $\lim_{\sigma\to\infty}a(\sigma)=0$ means that there exists $\sigma_0>0$ such that
-$|a(\sigma)|<\epsilon$ for all $\sigma>\sigma_0$. Now let $\sigma>0$. Then $a(\sigma)=a(\sigma_0)$, and
-so $|a(\sigma)|=|a(\sigma_0)|<\epsilon$, as required.
-\end{proof}
+\begin{proof}\begin{align*}
+\lim_{\sigma'\to\infty}a(\sigma) &= \lim_{\sigma'\to\infty}a(\sigma') \\
 %%-/
+  have := eventuallyEq_of_mem (mem_atTop σ) fun σ' h ↦ ha σ' σ (σpos.trans_le h) σpos
+--%% &= 0
+  exact tendsto_const_nhds_iff.mp (ha'.congr' this)
+--%%\end{align*}\end{proof}
 
 /-%%
 \begin{lemma}\label{tendsto_Realpow_atTop_nhds_0_of_norm_lt_1}\lean{tendsto_Realpow_atTop_nhds_0_of_norm_lt_1}\leanok

From f989c7b8c408648dc3505a81762935b7634bb673 Mon Sep 17 00:00:00 2001
From: L <git@llllvvuu.dev>
Date: Thu, 1 Feb 2024 01:25:18 -0800
Subject: [PATCH 2/2] leanok

---
 PrimeNumberTheoremAnd/MellinCalculus.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/PrimeNumberTheoremAnd/MellinCalculus.lean b/PrimeNumberTheoremAnd/MellinCalculus.lean
index b37fd030..b66461a2 100644
--- a/PrimeNumberTheoremAnd/MellinCalculus.lean
+++ b/PrimeNumberTheoremAnd/MellinCalculus.lean
@@ -154,7 +154,7 @@ lemma limitOfConstant {a : ℝ → ℂ} {σ : ℝ} (σpos : 0 < σ)
     (ha : ∀ (σ' : ℝ) (σ'' : ℝ) (_ : 0 < σ') (_ : 0 < σ''), a σ' = a σ'')
     (ha' : Tendsto a atTop (𝓝 0)) : a σ = 0 := by
 /-%%
-\begin{proof}\begin{align*}
+\begin{proof}\leanok\begin{align*}
 \lim_{\sigma'\to\infty}a(\sigma) &= \lim_{\sigma'\to\infty}a(\sigma') \\
 %%-/
   have := eventuallyEq_of_mem (mem_atTop σ) fun σ' h ↦ ha σ' σ (σpos.trans_le h) σpos