diff --git a/PrimeNumberTheoremAnd/Consequences.lean b/PrimeNumberTheoremAnd/Consequences.lean
index ab36c054..d14b930d 100644
--- a/PrimeNumberTheoremAnd/Consequences.lean
+++ b/PrimeNumberTheoremAnd/Consequences.lean
@@ -579,7 +579,7 @@ lemma sum_von_mangoldt_as_double_sum (x : ℝ) (hx: 0 ≤ x) :
             . simp at hp'
               have : (k' = k ∧ p' = p) := by
                 have := eq_of_prime_pow_eq h1.prime hp'.2.prime h2 h
-                rw [<-this, pow_right_inj] at h
+                rw [<-this, pow_right_inj₀] at h
                 . exact ⟨ h.symm, this.symm ⟩
                 . exact Prime.pos h1
                 exact Nat.Prime.ne_one h1
@@ -738,7 +738,7 @@ Filter.Tendsto (fun x ↦ log x ^ b / x^a) Filter.atTop (nhds 0) := by
     have h1 : 1 ≤ log x := by
       rwa [le_log_iff_exp_le h0]
     rw [div_rpow _ (le_of_lt h0)]
-    . rw [div_le_div_right (rpow_pos_of_pos h0 _), <-rpow_natCast, <-rpow_mul (zero_le_one.trans h1)]
+    . rw [div_le_div_iff_of_pos_right (rpow_pos_of_pos h0 _), <-rpow_natCast, <-rpow_mul (zero_le_one.trans h1)]
       apply rpow_le_rpow_of_exponent_le h1
       rw [<-div_le_iff₀ ha]
       exact le_ceil _
@@ -1530,7 +1530,7 @@ theorem pi_asymp'' :
     have ineq (x : ℝ) (hx : 2 < x) :
         |const| / |∫ (t : ℝ) in Set.Icc 2 x, (log t)⁻¹| ≤
         |const| / ((x - 2) * (log x)⁻¹) := by
-      apply div_le_div
+      apply div_le_div₀
       · exact abs_nonneg _
       · rfl
       · apply mul_pos
@@ -1630,7 +1630,7 @@ theorem pi_asymp'' :
         |C ε hε| / (∫ (t : ℝ) in Set.Icc 2 x, (log t)⁻¹) := by
         apply _root_.add_le_add (h₂ := le_rfl)
         apply _root_.add_le_add (h₂ := le_rfl)
-        apply div_le_div
+        apply div_le_div₀
         · apply mul_nonneg <;> try apply mul_nonneg <;> try linarith
           norm_num; exact log_nonneg <| by linarith
         · exact ineq1 ε hε (1/2) (by linarith) x (by simpa using ⟨by linarith, by linarith, by linarith⟩)
@@ -1643,7 +1643,7 @@ theorem pi_asymp'' :
         |C ε hε| / (∫ (t : ℝ) in Set.Icc 2 x, (log t)⁻¹) := by
         apply _root_.add_le_add (h₂ := le_rfl)
         apply _root_.add_le_add (h₁ := le_rfl)
-        apply div_le_div
+        apply div_le_div₀
         · exact le_trans (abs_nonneg _) <|
             hD ε hε (1/2) (by linarith) x (by simpa using ⟨by linarith, by linarith, by linarith⟩)
           -- apply mul_nonneg <;> try apply mul_nonneg <;> try linarith
@@ -1676,7 +1676,7 @@ theorem pi_asymp'' :
       linarith
     _ ≤ (1/2) * ε + (|D ε hε (1/2) (by linarith)| + |C ε hε|) / (∫ (t : ℝ) in Set.Icc 2 x, (log t)⁻¹) := by
       apply _root_.add_le_add (h₁ := le_rfl)
-      apply div_le_div
+      apply div_le_div₀
       · apply add_nonneg <;> exact abs_nonneg _
       · apply _root_.add_le_add (h₂ := le_rfl); exact le_abs_self _
       · apply integral_log_inv_pos; linarith
@@ -1754,7 +1754,7 @@ lemma pi_alt_Oaux1 : ∃ c, ∀ᶠ (x : ℝ) in atTop,
       · intro x hx
         simp only [Set.mem_Icc] at hx
         rw [inv_le_inv₀]
-        · apply pow_le_pow_left
+        · apply pow_le_pow_left₀
           · apply log_nonneg (by linarith)
           · rw [log_le_log_iff] <;> linarith
         · apply pow_pos
@@ -1800,7 +1800,7 @@ lemma pi_alt_Oaux2 : ∃ c, ∀ᶠ (x : ℝ) in atTop,
       · intro x hx
         simp only [Set.mem_Icc] at hx
         rw [inv_le_inv₀]
-        · apply pow_le_pow_left
+        · apply pow_le_pow_left₀
           · apply log_nonneg (by linarith)
           · rw [log_le_log_iff] <;> linarith
         · apply pow_pos
diff --git a/PrimeNumberTheoremAnd/Fourier.lean b/PrimeNumberTheoremAnd/Fourier.lean
index f3e26af7..c3c85e21 100644
--- a/PrimeNumberTheoremAnd/Fourier.lean
+++ b/PrimeNumberTheoremAnd/Fourier.lean
@@ -1,6 +1,6 @@
 import Mathlib.Analysis.Distribution.SchwartzSpace
 import Mathlib.MeasureTheory.Integral.IntegralEqImproper
-import Mathlib.Topology.ContinuousMap.Bounded
+import Mathlib.Topology.ContinuousMap.Bounded.Basic
 import Mathlib.Order.Filter.ZeroAndBoundedAtFilter
 import Mathlib.Analysis.Fourier.Inversion
 import Mathlib.Analysis.Fourier.FourierTransformDeriv
diff --git a/PrimeNumberTheoremAnd/GeneralMeromorphic.lean b/PrimeNumberTheoremAnd/GeneralMeromorphic.lean
index e1439535..df3cb104 100644
--- a/PrimeNumberTheoremAnd/GeneralMeromorphic.lean
+++ b/PrimeNumberTheoremAnd/GeneralMeromorphic.lean
@@ -10,7 +10,7 @@ open scoped Interval
 
 /-%%
 \begin{definition}\label{MeromorphicOnRectangle}\lean{MeromorphicOnRectangle}\leanok
-\uses{Rectangle, RectangleBorder, RectangleIntegral}
+\uses{RectangleBorder, RectangleIntegral}
 A function $f$ is Meromorphic on a rectangle with corners $z$ and $w$ if it is holomorphic off a
 (finite) set of poles, none of which are on the boundary of the rectangle.
 [Note: Might be overkill, can just work explicitly with the functions that arise. Of course would be nice to have the general theory as well...]
diff --git a/PrimeNumberTheoremAnd/Mathlib/Data/Nat/FinMulAntidiagonal.lean b/PrimeNumberTheoremAnd/Mathlib/Data/Nat/FinMulAntidiagonal.lean
index b934269a..688c01de 100644
--- a/PrimeNumberTheoremAnd/Mathlib/Data/Nat/FinMulAntidiagonal.lean
+++ b/PrimeNumberTheoremAnd/Mathlib/Data/Nat/FinMulAntidiagonal.lean
@@ -306,7 +306,7 @@ private theorem f_surj {n : ℕ} (hn : n ≠ 0) :
     rw [mem_filter, Finset.mem_product] at hb
     refine ⟨?_, hn⟩
     · rw [Fin.prod_univ_three a]
-      unfold_let a
+      unfold a
       simp only [Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons, Matrix.cons_val_two,
         Matrix.tail_cons]
       rw [Nat.mul_div_cancel_left' (Nat.gcd_dvd_left _ _), ←hb.2, lcm,
diff --git a/PrimeNumberTheoremAnd/MediumPNT.lean b/PrimeNumberTheoremAnd/MediumPNT.lean
index 3941cb9d..e8dec6ce 100644
--- a/PrimeNumberTheoremAnd/MediumPNT.lean
+++ b/PrimeNumberTheoremAnd/MediumPNT.lean
@@ -1,5 +1,4 @@
 import PrimeNumberTheoremAnd.ZetaBounds
-import EulerProducts.PNT
 import Mathlib.Algebra.Group.Support
 
 set_option lang.lemmaCmd true
@@ -386,7 +385,7 @@ X^{s}ds = \frac{X^{1}}{1}\mathcal{M}(\widetilde{1_{\epsilon}})(1)
 
 /-%%
 \begin{proof}
-\uses{ZeroFreeBox, Rectangle, RectangleBorder, RectangleIntegral, ResidueOfLogDerivative,
+\uses{ZeroFreeBox, RectangleBorder, RectangleIntegral, ResidueOfLogDerivative,
 MellinOfSmooth1a, MellinOfSmooth1b, MellinOfSmooth1c, MellinOfDeltaSpikeAt1,
 SmoothedChebyshevPull1}
 Residue calculus / the argument principle.
diff --git a/PrimeNumberTheoremAnd/MellinCalculus.lean b/PrimeNumberTheoremAnd/MellinCalculus.lean
index f97f82af..6875e2a1 100644
--- a/PrimeNumberTheoremAnd/MellinCalculus.lean
+++ b/PrimeNumberTheoremAnd/MellinCalculus.lean
@@ -1,7 +1,10 @@
+import EulerProducts.Auxiliary
 import Mathlib.Analysis.MellinInversion
 import PrimeNumberTheoremAnd.PerronFormula
 import Mathlib.Algebra.GroupWithZero.Units.Basic
 
+open scoped ContDiff
+
 set_option lang.lemmaCmd true
 
 -- TODO: move near `MeasureTheory.setIntegral_prod`
@@ -651,9 +654,9 @@ $$
 
 attribute [- simp] one_div in
 
-lemma SmoothExistence : ∃ (Ψ : ℝ → ℝ), (ContDiff ℝ ⊤ Ψ) ∧ (∀ x, 0 ≤ Ψ x) ∧
+lemma SmoothExistence : ∃ (Ψ : ℝ → ℝ), (ContDiff ℝ ∞ Ψ) ∧ (∀ x, 0 ≤ Ψ x) ∧
     Ψ.support ⊆ Icc (1 / 2) 2 ∧ ∫ x in Ici 0, Ψ x / x = 1 := by
-  suffices h : ∃ (Ψ : ℝ → ℝ), (ContDiff ℝ ⊤ Ψ) ∧ (∀ x, 0 ≤ Ψ x) ∧
+  suffices h : ∃ (Ψ : ℝ → ℝ), (ContDiff ℝ ∞ Ψ) ∧ (∀ x, 0 ≤ Ψ x) ∧
       Ψ.support ⊆ Set.Icc (1 / 2) 2 ∧ 0 < ∫ x in Set.Ici 0, Ψ x / x by
     rcases h with ⟨Ψ, hΨ, hΨnonneg, hΨsupp, hΨpos⟩
     let c := (∫ x in Ici 0, Ψ x / x)
diff --git a/PrimeNumberTheoremAnd/PerronFormula.lean b/PrimeNumberTheoremAnd/PerronFormula.lean
index 8c199d34..a1cda540 100644
--- a/PrimeNumberTheoremAnd/PerronFormula.lean
+++ b/PrimeNumberTheoremAnd/PerronFormula.lean
@@ -492,7 +492,7 @@ theorem isTheta_uniformlyOn_uIcc {x : ℝ} (xpos : 0 < x) (σ' σ'' : ℝ) :
 
 theorem isTheta_uniformlyOn_uIoc {x : ℝ} (xpos : 0 < x) (σ' σ'' : ℝ) :
     (fun (σ, (y : ℝ)) ↦ f x (σ + y * I)) =Θ[𝓟 (uIoc σ' σ'') ×ˢ (atBot ⊔ atTop)]
-    fun (σ, y) ↦ 1 / y^2 := by
+    fun (_, y) ↦ 1 / y^2 := by
   refine (𝓟 (uIoc σ' σ'')).eq_or_neBot.casesOn (fun hbot ↦ by simp [hbot]) (fun _ ↦ ?_)
   haveI : NeBot (atBot (α := ℝ) ⊔ atTop) := sup_neBot.mpr (Or.inl atBot_neBot)
   exact (isTheta_uniformlyOn_uIcc xpos σ' σ'').mono (by simpa using Ioc_subset_Icc_self)
@@ -698,7 +698,7 @@ variable  {α β : Type*} [LinearOrder β] [NoMaxOrder β] [TopologicalSpace β]
 lemma _root_.Filter.Tendsto.eventually_bddAbove {f : α → β} (hf : Tendsto f l (𝓝 y)) :
     ∀ᶠ s in l.smallSets, BddAbove (f '' s) := by
   obtain ⟨y', hy'⟩ := exists_gt y
-  obtain ⟨s, hsl, hs⟩ := (eventually_le_of_tendsto_lt hy' hf).exists_mem
+  obtain ⟨s, hsl, hs⟩ := (Tendsto.eventually_le_const hy' hf).exists_mem
   simp_rw [Filter.eventually_smallSets, bddAbove_def]
   refine ⟨s, hsl, fun t ht ↦ ⟨y', fun y hy ↦ ?_⟩⟩
   obtain ⟨x, hxt, hxy⟩ := hy
diff --git a/PrimeNumberTheoremAnd/Rectangle.lean b/PrimeNumberTheoremAnd/Rectangle.lean
index d961d133..8669df5d 100644
--- a/PrimeNumberTheoremAnd/Rectangle.lean
+++ b/PrimeNumberTheoremAnd/Rectangle.lean
@@ -11,14 +11,6 @@ variable {z w : ℂ} {c : ℝ}
 This files gathers definitions and basic properties about rectangles.
 %%-/
 
-/-%%
-\begin{definition}\label{Rectangle}\lean{Rectangle}\leanok
-A Rectangle has corners $z$ and $w \in \C$.
-\end{definition}
-%%-/
-/-- A `Rectangle` has corners `z` and `w`. -/
-def Rectangle (z w : ℂ) : Set ℂ := [[z.re, w.re]] ×ℂ [[z.im, w.im]]
-
 namespace Rectangle
 
 lemma symm : Rectangle z w = Rectangle w z := by
@@ -45,9 +37,6 @@ lemma Square_apply (p : ℂ) (cpos : c > 0) :
   rw [Square, Rectangle, uIcc_of_le (by simp; linarith), uIcc_of_le (by simp; linarith)]
   simp
 
--- From PR #9598
-/-- The preimage under `equivRealProd` of `s ×ˢ t` is `s ×ℂ t`. -/
-lemma preimage_equivRealProd_prod (s t : Set ℝ) : equivRealProd ⁻¹' (s ×ˢ t) = s ×ℂ t := rfl
 
 @[simp]
 theorem preimage_equivRealProdCLM_reProdIm (s t : Set ℝ) :
@@ -62,17 +51,6 @@ theorem ContinuousLinearEquiv.coe_toLinearEquiv_symm {R : Type*} {S : Type*} [Se
     ⇑e.toLinearEquiv.symm = e.symm :=
   rfl
 
--- From PR #9598
-/-- The inequality `s × t ⊆ s₁ × t₁` holds in `ℂ` iff it holds in `ℝ × ℝ`. -/
-lemma reProdIm_subset_iff {s s₁ t t₁ : Set ℝ} : s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁ := by
-  simp_rw [← preimage_equivRealProd_prod, equivRealProd.preimage_subset]
-
--- From PR #9598
-/-- If `s ⊆ s₁ ⊆ ℝ` and `t ⊆ t₁ ⊆ ℝ`, then `s × t ⊆ s₁ × t₁` in `ℂ`. -/
-lemma reProdIm_subset_iff' {s s₁ t t₁ : Set ℝ} :
-    s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅ :=
-  reProdIm_subset_iff.trans prod_subset_prod_iff
-
 /-- The axis-parallel complex rectangle with opposite corners `z` and `w` is complex product
   of two intervals, which is also the convex hull of the four corners. Golfed from mathlib4\#9598.-/
 lemma segment_reProdIm_segment_eq_convexHull (z w : ℂ) :
@@ -96,11 +74,6 @@ lemma mem_Rect {z w : ℂ} (zRe_lt_wRe : z.re ≤ w.re) (zIm_lt_wIm : z.im ≤ w
 lemma square_neg (p : ℂ) (c : ℝ) : Square p (-c) = Square p c := by
   simpa [Square] using Rectangle.symm
 
-def Set.uIoo {α : Type*} [Lattice α] (a b : α) : Set α := Ioo (a ⊓ b) (a ⊔ b)
-
-@[simp]
-theorem uIoo_of_le {α : Type*} [Lattice α] {a b : α} (h : a ≤ b) : Set.uIoo a b = Ioo a b := by
-  rw [uIoo, inf_eq_left.2 h, sup_eq_right.2 h]
 
 theorem Set.left_not_mem_uIoo {a b : ℝ} : a ∉ Set.uIoo a b :=
   fun ⟨h1, h2⟩ ↦ (left_lt_sup.mp h2) (le_of_not_le (inf_lt_left.mp h1))
@@ -191,20 +164,6 @@ lemma rectangle_mem_nhds_iff {z w p : ℂ} : Rectangle z w ∈ 𝓝 p ↔
     p ∈ (Set.uIoo z.re w.re) ×ℂ (Set.uIoo z.im w.im) := by
   simp_rw [← mem_interior_iff_mem_nhds, Rectangle, Complex.interior_reProdIm, uIoo, uIcc, interior_Icc]
 
-/-- A real segment `[a₁, a₂]` translated by `b * I` is the complex line segment.
-Golfed from mathlib\#9598.-/
-lemma horizontalSegment_eq (a₁ a₂ b : ℝ) :
-    (fun (x : ℝ) ↦ x + b * I) '' [[a₁, a₂]] = [[a₁, a₂]] ×ℂ {b} :=
-  Set.ext fun _ => ⟨fun hx ↦ hx.casesOn fun _ ⟨_, hx⟩ ↦ by simpa [← hx, reProdIm],
-    fun hx ↦ hx.casesOn (by simp_all [Complex.ext_iff])⟩
-
-/-- A vertical segment `[b₁, b₂]` translated by `a` is the complex line segment.
-Golfed from mathlib\#9598.-/
-lemma verticalSegment_eq (a b₁ b₂ : ℝ) :
-    (fun (y : ℝ) ↦ a + y * I) '' [[b₁, b₂]] = {a} ×ℂ [[b₁, b₂]] :=
-  Set.ext fun _ => ⟨fun hx ↦ hx.casesOn fun _ ⟨_, hx⟩ ↦ by simpa [← hx, reProdIm],
-    fun hx ↦ hx.casesOn (by simp_all [Complex.ext_iff])⟩
-
 lemma mapsTo_rectangle_left_re (z w : ℂ) :
     MapsTo (fun (y : ℝ) => ↑z.re + ↑y * I) [[z.im, w.im]] (Rectangle z w) :=
   fun _ hx ↦ ⟨by simp, by simp [hx]⟩
diff --git a/PrimeNumberTheoremAnd/Sobolev.lean b/PrimeNumberTheoremAnd/Sobolev.lean
index 0808343b..5192a733 100644
--- a/PrimeNumberTheoremAnd/Sobolev.lean
+++ b/PrimeNumberTheoremAnd/Sobolev.lean
@@ -3,6 +3,7 @@ import Mathlib.Analysis.Distribution.SchwartzSpace
 import Mathlib.Order.Filter.ZeroAndBoundedAtFilter
 
 open Real Complex MeasureTheory Filter Topology BoundedContinuousFunction SchwartzMap  BigOperators
+open scoped ContDiff
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ}
 
@@ -26,10 +27,10 @@ section lemmas
 
 noncomputable def funscale {E : Type*} (g : ℝ → E) (R x : ℝ) : E := g (R⁻¹ • x)
 
-lemma contDiff_ofReal : ContDiff ℝ ⊤ ofReal := by
+lemma contDiff_ofReal : ContDiff ℝ ∞ ofReal := by
   have key x : HasDerivAt ofReal 1 x := hasDerivAt_id x |>.ofReal_comp
   have key' : deriv ofReal = fun _ => 1 := by ext x ; exact (key x).deriv
-  refine contDiff_top_iff_deriv.mpr ⟨fun x => (key x).differentiableAt, ?_⟩
+  refine contDiff_infty_iff_deriv.mpr ⟨fun x => (key x).differentiableAt, ?_⟩
   simpa [key'] using contDiff_const
 
 omit [NormedSpace ℝ E] in
@@ -46,7 +47,7 @@ variable {f : CS n E} {R x v : ℝ}
 instance : CoeFun (CS n E) (fun _ => ℝ → E) where coe := CS.toFun
 
 instance : Coe (CS n ℝ) (CS n ℂ) where coe f := ⟨fun x => f x,
-  contDiff_ofReal.of_le le_top |>.comp f.h1, f.h2.comp_left (g := ofReal) rfl⟩
+  contDiff_ofReal.of_le (mod_cast le_top) |>.comp f.h1, f.h2.comp_left (g := ofReal) rfl⟩
 
 def neg (f : CS n E) : CS n E where
   toFun := -f
@@ -67,7 +68,7 @@ lemma continuous (f : CS n E) : Continuous f := f.h1.continuous
 
 noncomputable def deriv (f : CS (n + 1) E) : CS n E where
   toFun := _root_.deriv f
-  h1 := (contDiff_succ_iff_deriv.mp f.h1).2
+  h1 := (contDiff_succ_iff_deriv.mp f.h1).2.2
   h2 := f.h2.deriv
 
 lemma hasDerivAt (f : CS (n + 1) E) (x : ℝ) : HasDerivAt f (f.deriv x) x :=
@@ -150,7 +151,7 @@ lemma iteratedDeriv_sub {f g : ℝ → E} (hf : ContDiff ℝ n f) (hg : ContDiff
 
 noncomputable def deriv (f : W1 (n + 1) E) : W1 n E where
   toFun := _root_.deriv f
-  smooth := contDiff_succ_iff_deriv.mp f.smooth |>.2
+  smooth := contDiff_succ_iff_deriv.mp f.smooth |>.2.2
   integrable k hk := by
     simpa [iteratedDeriv_succ'] using f.integrable (Nat.succ_le_succ hk)
 
diff --git a/PrimeNumberTheoremAnd/Wiener.lean b/PrimeNumberTheoremAnd/Wiener.lean
index 1b984ba4..0bfb0e56 100644
--- a/PrimeNumberTheoremAnd/Wiener.lean
+++ b/PrimeNumberTheoremAnd/Wiener.lean
@@ -1,8 +1,8 @@
-import EulerProducts.PNT
 import Mathlib.Analysis.Fourier.FourierTransform
 import Mathlib.Analysis.Fourier.FourierTransformDeriv
 import Mathlib.NumberTheory.ArithmeticFunction
-import Mathlib.Topology.Support
+import Mathlib.NumberTheory.LSeries.PrimesInAP
+import Mathlib.Topology.Algebra.Support
 import Mathlib.Analysis.Calculus.ContDiff.Defs
 import Mathlib.Geometry.Manifold.PartitionOfUnity
 import Mathlib.Tactic.FunProp
@@ -31,12 +31,13 @@ set_option lang.lemmaCmd true
 open Real BigOperators ArithmeticFunction MeasureTheory Filter Set FourierTransform LSeries Asymptotics SchwartzMap
 open Complex hiding log
 open scoped Topology
+open scoped ContDiff
 
 variable {n : ℕ} {A a b c d u x y t σ' : ℝ} {ψ Ψ : ℝ → ℂ} {F G : ℂ → ℂ} {f : ℕ → ℂ} {𝕜 : Type} [RCLike 𝕜]
 
 -- This version makes the support of Ψ explicit, and this is easier for some later proofs
 lemma smooth_urysohn_support_Ioo (h1 : a < b) (h3: c < d) :
-    ∃ Ψ : ℝ → ℝ, (ContDiff ℝ ⊤ Ψ) ∧ (HasCompactSupport Ψ) ∧ Set.indicator (Set.Icc b c) 1 ≤ Ψ ∧
+    ∃ Ψ : ℝ → ℝ, (ContDiff ℝ ∞ Ψ) ∧ (HasCompactSupport Ψ) ∧ Set.indicator (Set.Icc b c) 1 ≤ Ψ ∧
     Ψ ≤ Set.indicator (Set.Ioo a d) 1 ∧ (Function.support Ψ = Set.Ioo a d) := by
 
   have := exists_msmooth_zero_iff_one_iff_of_isClosed
@@ -256,7 +257,7 @@ lemma second_fourier_integrable_aux1 (hcont: Continuous ψ) (hsupp: Integrable 
   · let f1 : ℝ → ENNReal := fun a1 ↦ ↑‖cexp (-(↑a1 * (↑σ' - 1)))‖₊
     let f2 : ℝ → ENNReal := fun a2 ↦ ↑‖ψ a2‖₊
     suffices ∫⁻ (a : ℝ × ℝ), f1 a.1 * f2 a.2 ∂ν < ⊤ by simpa [Function.uncurry, HasFiniteIntegral]
-    refine (lintegral_prod_mul ?_ ?_).trans_lt ?_ <;> unfold_let f1 f2; fun_prop; fun_prop
+    refine (lintegral_prod_mul ?_ ?_).trans_lt ?_ <;> try fun_prop
     exact ENNReal.mul_lt_top (second_fourier_integrable_aux1a hσ).2 hsupp.2
 
 lemma second_fourier_integrable_aux2 (hσ : 1 < σ') :
@@ -896,7 +897,7 @@ theorem limiting_fourier_lim1 (hcheby : cheby f) (ψ : W21) (hx : 0 < x) :
     refine mul_le_mul ?_ (hC _) (norm_nonneg _) (div_nonneg (norm_nonneg _) (Nat.cast_nonneg _))
     by_cases h : n = 0 <;> simp [h, nterm]
     have : 1 ≤ (n : ℝ) := by simpa using Nat.pos_iff_ne_zero.mpr h
-    refine div_le_div (by simp only [apply_nonneg]) le_rfl (by simpa [Nat.pos_iff_ne_zero]) ?_
+    refine div_le_div₀ (by simp only [apply_nonneg]) le_rfl (by simpa [Nat.pos_iff_ne_zero]) ?_
     simpa using Real.rpow_le_rpow_of_exponent_le this hσ'.le
 
 theorem limiting_fourier_lim2_aux (x : ℝ) (C : ℝ) :
@@ -1061,7 +1062,7 @@ lemma limiting_cor (ψ : CS 2 ℂ) (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (
 %%-/
 
 lemma smooth_urysohn (a b c d : ℝ) (h1 : a < b) (h3 : c < d) : ∃ Ψ : ℝ → ℝ,
-    (ContDiff ℝ ⊤ Ψ) ∧ (HasCompactSupport Ψ) ∧
+    (ContDiff ℝ ∞ Ψ) ∧ (HasCompactSupport Ψ) ∧
       Set.indicator (Set.Icc b c) 1 ≤ Ψ ∧ Ψ ≤ Set.indicator (Set.Ioo a d) 1 := by
 
   obtain ⟨ψ, l1, l2, l3, l4, -⟩ := smooth_urysohn_support_Ioo h1 h3
@@ -1075,13 +1076,13 @@ A standard analysis lemma, which can be proven by convolving $1_K$ with a smooth
 
 noncomputable def exists_trunc : trunc := by
   choose ψ h1 h2 h3 h4 using smooth_urysohn (-2) (-1) (1) (2) (by linarith) (by linarith)
-  exact ⟨⟨ψ, h1.of_le le_top, h2⟩, h3, h4⟩
+  exact ⟨⟨ψ, h1.of_le (by norm_cast), h2⟩, h3, h4⟩
 
 lemma one_div_sub_one (n : ℕ) : 1 / (↑(n - 1) : ℝ) ≤ 2 / n := by
   match n with
   | 0 => simp
   | 1 => simp
-  | n + 2 => { norm_cast ; rw [div_le_div_iff] <;> simp [mul_add] <;> linarith }
+  | n + 2 => { norm_cast ; rw [div_le_div_iff₀] <;> simp [mul_add] <;> linarith }
 
 lemma quadratic_pos (a b c x : ℝ) (ha : 0 < a) (hΔ : discrim a b c < 0) : 0 < a * x ^ 2 + b * x + c := by
   have l1 : a * x ^ 2 + b * x + c = a * (x + b / (2 * a)) ^ 2 - discrim a b c / (4 * a) := by
@@ -1331,7 +1332,7 @@ lemma hh_integrable_aux (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
     apply tendsto_log_nhdsWithin_zero_right.comp
     rw [Metric.tendsto_nhdsWithin_nhdsWithin]
     intro ε hε
-    refine ⟨c * ε, by positivity, fun hx1 hx2 => ⟨?_, ?_⟩⟩
+    refine ⟨c * ε, by positivity, fun x hx1 hx2 => ⟨?_, ?_⟩⟩
     · simp at hx1 ⊢ ; positivity
     · simp [abs_eq_self.mpr hc.le] at hx2 ⊢ ; rwa [div_lt_iff₀ hc, mul_comm]
 
@@ -1394,7 +1395,7 @@ lemma bound_sum_log {C : ℝ} (hf0 : f 0 = 0) (hf : chebyWith C f) {x : ℝ} (hx
     simp only
     apply mul_le_mul le_rfl ?_ (hh_nonneg _ (by positivity)) (by positivity)
     apply hh_antitone one_div_two_pi_mem_Ioo (by simp ; positivity) (by simp ; positivity)
-    apply (div_le_div_right (by positivity)).mpr huv
+    apply (div_le_div_iff_of_pos_right (by positivity)).mpr huv
 
   have l6 {n : ℕ} : IntegrableOn (fun t ↦ x⁻¹ * hh (π⁻¹ * 2⁻¹) (t / x)) (Icc 0 n) volume := by
     apply IntegrableOn.mono_set (hh_integrable (by positivity) (by positivity) (by positivity)) Icc_subset_Ici_self
@@ -1630,12 +1631,12 @@ In particular, given $f$ in the Schwartz class, let $F : \R_+ \to \C : x \mapsto
 \end{proof}
 %%-/
 
-def toSchwartz (f : ℝ → ℂ) (h1 : ContDiff ℝ ⊤ f) (h2 : HasCompactSupport f) : 𝓢(ℝ, ℂ) where
+def toSchwartz (f : ℝ → ℂ) (h1 : ContDiff ℝ ∞ f) (h2 : HasCompactSupport f) : 𝓢(ℝ, ℂ) where
   toFun := f
   smooth' := h1
   decay' k n := by
     have l1 : Continuous (fun x => ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖) := by
-      have : ContDiff ℝ ⊤ (iteratedFDeriv ℝ n f) := h1.iteratedFDeriv_right le_top
+      have : ContDiff ℝ ∞ (iteratedFDeriv ℝ n f) := h1.iteratedFDeriv_right (mod_cast le_top)
       exact Continuous.mul (by continuity) this.continuous.norm
     have l2 : HasCompactSupport (fun x ↦ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖) := (h2.iteratedFDeriv _).norm.mul_left
     simpa using l1.bounded_above_of_compact_support l2
@@ -1717,12 +1718,12 @@ as $x \to \infty$.
 
 lemma wiener_ikehara_smooth (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')) (hcheby : cheby f)
     (hG: ContinuousOn G {s | 1 ≤ s.re}) (hG' : Set.EqOn G (fun s ↦ LSeries f s - A / (s - 1)) {s | 1 < s.re})
-    (hsmooth: ContDiff ℝ ⊤ Ψ) (hsupp: HasCompactSupport Ψ) (hplus: closure (Function.support Ψ) ⊆ Set.Ioi 0) :
+    (hsmooth: ContDiff ℝ ∞ Ψ) (hsupp: HasCompactSupport Ψ) (hplus: closure (Function.support Ψ) ⊆ Set.Ioi 0) :
     Tendsto (fun x : ℝ ↦ (∑' n, f n * Ψ (n / x)) / x - A * ∫ y in Set.Ioi 0, Ψ y) atTop (nhds 0) := by
 
   let h (x : ℝ) : ℂ := rexp (2 * π * x) * Ψ (exp (2 * π * x))
-  have h1 : ContDiff ℝ ⊤ h := by
-    have : ContDiff ℝ ⊤ (fun x : ℝ => (rexp (2 * π * x))) := (contDiff_const.mul contDiff_id).exp
+  have h1 : ContDiff ℝ ∞ h := by
+    have : ContDiff ℝ ∞ (fun x : ℝ => (rexp (2 * π * x))) := (contDiff_const.mul contDiff_id).exp
     exact (contDiff_ofReal.comp this).mul (hsmooth.comp this)
   have h2 : HasCompactSupport h := by
     have : 2 * π ≠ 0 := by simp [pi_ne_zero]
@@ -1771,7 +1772,7 @@ and the claim follows from Lemma \ref{schwarz-id}.
 
 lemma wiener_ikehara_smooth' (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')) (hcheby : cheby f)
     (hG: ContinuousOn G {s | 1 ≤ s.re}) (hG' : Set.EqOn G (fun s ↦ LSeries f s - A / (s - 1)) {s | 1 < s.re})
-    (hsmooth: ContDiff ℝ ⊤ Ψ) (hsupp: HasCompactSupport Ψ) (hplus: closure (Function.support Ψ) ⊆ Set.Ioi 0) :
+    (hsmooth: ContDiff ℝ ∞ Ψ) (hsupp: HasCompactSupport Ψ) (hplus: closure (Function.support Ψ) ⊆ Set.Ioi 0) :
     Tendsto (fun x : ℝ ↦ (∑' n, f n * Ψ (n / x)) / x) atTop (nhds (A * ∫ y in Set.Ioi 0, Ψ y)) :=
   tendsto_sub_nhds_zero_iff.mp <| wiener_ikehara_smooth hf hcheby hG hG' hsmooth hsupp hplus
 
@@ -1784,18 +1785,18 @@ theorem set_integral_ofReal {f : ℝ → ℝ} {s : Set ℝ} : ∫ x in s, (f x :
 lemma wiener_ikehara_smooth_real {f : ℕ → ℝ} {Ψ : ℝ → ℝ} (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ'))
     (hcheby : cheby f) (hG: ContinuousOn G {s | 1 ≤ s.re})
     (hG' : Set.EqOn G (fun s ↦ LSeries f s - A / (s - 1)) {s | 1 < s.re})
-    (hsmooth: ContDiff ℝ ⊤ Ψ) (hsupp: HasCompactSupport Ψ) (hplus: closure (Function.support Ψ) ⊆ Set.Ioi 0) :
+    (hsmooth: ContDiff ℝ ∞ Ψ) (hsupp: HasCompactSupport Ψ) (hplus: closure (Function.support Ψ) ⊆ Set.Ioi 0) :
     Tendsto (fun x : ℝ ↦ (∑' n, f n * Ψ (n / x)) / x) atTop (nhds (A * ∫ y in Set.Ioi 0, Ψ y)) := by
 
   let Ψ' := ofReal ∘ Ψ
-  have l1 : ContDiff ℝ ⊤ Ψ' := contDiff_ofReal.comp hsmooth
+  have l1 : ContDiff ℝ ∞ Ψ' := contDiff_ofReal.comp hsmooth
   have l2 : HasCompactSupport Ψ' := hsupp.comp_left rfl
   have l3 : closure (Function.support Ψ') ⊆ Ioi 0 := by rwa [Function.support_comp_eq] ; simp
   have key := (continuous_re.tendsto _).comp (@wiener_ikehara_smooth' A Ψ G f hf hcheby hG hG' l1 l2 l3)
   simp at key ; norm_cast at key
 
 lemma interval_approx_inf (ha : 0 < a) (hab : a < b) :
-    ∀ᶠ ε in 𝓝[>] 0, ∃ ψ : ℝ → ℝ, ContDiff ℝ ⊤ ψ ∧ HasCompactSupport ψ ∧ closure (Function.support ψ) ⊆ Set.Ioi 0 ∧
+    ∀ᶠ ε in 𝓝[>] 0, ∃ ψ : ℝ → ℝ, ContDiff ℝ ∞ ψ ∧ HasCompactSupport ψ ∧ closure (Function.support ψ) ⊆ Set.Ioi 0 ∧
       ψ ≤ indicator (Ico a b) 1 ∧ b - a - ε ≤ ∫ y in Ioi 0, ψ y := by
 
   have l1 : Iio ((b - a) / 3) ∈ 𝓝[>] 0 := nhdsWithin_le_nhds <| Iio_mem_nhds (by linarith)
@@ -1819,7 +1820,7 @@ lemma interval_approx_inf (ha : 0 < a) (hab : a < b) :
     simp
 
 lemma interval_approx_sup (ha : 0 < a) (hab : a < b) :
-    ∀ᶠ ε in 𝓝[>] 0, ∃ ψ : ℝ → ℝ, ContDiff ℝ ⊤ ψ ∧ HasCompactSupport ψ ∧ closure (Function.support ψ) ⊆ Set.Ioi 0 ∧
+    ∀ᶠ ε in 𝓝[>] 0, ∃ ψ : ℝ → ℝ, ContDiff ℝ ∞ ψ ∧ HasCompactSupport ψ ∧ closure (Function.support ψ) ⊆ Set.Ioi 0 ∧
       indicator (Ico a b) 1 ≤ ψ ∧ ∫ y in Ioi 0, ψ y ≤ b - a + ε := by
 
   have l1 : Iio (a / 2) ∈ 𝓝[>] 0 := nhdsWithin_le_nhds <| Iio_mem_nhds (by linarith)
@@ -2196,12 +2197,17 @@ $$ \sum_{n \leq x} \Lambda(n) = x + o(x).$$
 -- hypothesis)
 
 theorem WeakPNT : Tendsto (fun N ↦ cumsum Λ N / N) atTop (𝓝 1) := by
+  let F := vonMangoldt.LFunctionResidueClassAux (q := 1) 1
   have hnv := riemannZeta_ne_zero_of_one_le_re
   have l1 (n : ℕ) : 0 ≤ Λ n := vonMangoldt_nonneg
-  have l2 s (hs : 1 < s.re) : (-deriv ζ₁ / ζ₁) s = LSeries Λ s - 1 / (s - 1) := by
-    have hs₁ : s ≠ 1 := by contrapose! hs ; simp [hs]
-    simp [LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs, neg_logDeriv_ζ₁_eq hs₁ (hnv hs₁ hs.le)]
-  have l3 : ContinuousOn (-deriv ζ₁ / ζ₁) {s | 1 ≤ s.re} := continuousOn_neg_logDeriv_ζ₁.mono (by tauto)
+  have l2 s (hs : 1 < s.re) : F s = LSeries Λ s - 1 / (s - 1) := by
+    have := vonMangoldt.eqOn_LFunctionResidueClassAux (q := 1) isUnit_one hs
+    simp only [F, this, vonMangoldt.residueClass, Nat.totient_one, Nat.cast_one, inv_one, one_div, sub_left_inj]
+    apply LSeries_congr
+    intro n _
+    simp only [ofReal_inj, indicator_apply_eq_self, mem_setOf_eq]
+    exact fun hn ↦ absurd (Subsingleton.eq_one _) hn
+  have l3 : ContinuousOn F {s | 1 ≤ s.re} := vonMangoldt.continuousOn_LFunctionResidueClassAux 1
   have l4 : cheby Λ := vonMangoldt_cheby
   have l5 (σ' : ℝ) (hσ' : 1 < σ') : Summable (nterm Λ σ') := by
     simpa only [← nterm_eq_norm_term] using (@ArithmeticFunction.LSeriesSummable_vonMangoldt σ' hσ').norm
@@ -2328,7 +2334,7 @@ theorem WeakPNT_character'
           ((starRingEnd ℂ) (χ a) * ((deriv (LSeries (fun n:ℕ ↦ χ n)) s)) / (LSeries (fun n:ℕ ↦ χ n) s))) /
         (Nat.totient q : ℂ) := by
   have : NeZero q := ⟨by omega⟩
-  convert WeakPNT_character ((ZMod.isUnit_iff_coprime a q).mpr ha) hs using 1
+  convert vonMangoldt.LSeries_residueClass_eq ((ZMod.isUnit_iff_coprime a q).mpr ha) hs using 1
   · congr with n
     have : n % q = a ↔ (n : ZMod q) = a := by
       rw [ZMod.natCast_eq_natCast_iff', Nat.mod_eq_of_lt ha']
diff --git a/PrimeNumberTheoremAnd/ZetaBounds.lean b/PrimeNumberTheoremAnd/ZetaBounds.lean
index d6bb7269..af098ea4 100644
--- a/PrimeNumberTheoremAnd/ZetaBounds.lean
+++ b/PrimeNumberTheoremAnd/ZetaBounds.lean
@@ -3,7 +3,6 @@ import Mathlib.MeasureTheory.Integral.IntervalIntegral
 import Mathlib.Analysis.Calculus.Deriv.Basic
 import Mathlib.NumberTheory.LSeries.RiemannZeta
 import Mathlib.Algebra.Group.Basic
-import EulerProducts.PNT
 import PrimeNumberTheoremAnd.ResidueCalcOnRectangles
 import PrimeNumberTheoremAnd.MellinCalculus
 import Mathlib.MeasureTheory.Function.Floor
@@ -79,7 +78,7 @@ lemma ContDiffOn.continuousOn_deriv {φ : ℝ → ℂ} {a b : ℝ}
     (φDiff : ContDiffOn ℝ 1 φ (uIoo a b)) :
     ContinuousOn (deriv φ) (uIoo a b) := by
   apply ContDiffOn.continuousOn (𝕜 := ℝ) (n := 0)
-  exact (fun h ↦ ((contDiffOn_succ_iff_deriv_of_isOpen isOpen_Ioo).1 h).2) φDiff
+  exact (fun h ↦ ((contDiffOn_succ_iff_deriv_of_isOpen isOpen_Ioo).1 h).2.2) φDiff
 
 lemma LinearDerivative_ofReal (x : ℝ) (a b : ℂ) : HasDerivAt (fun (t : ℝ) ↦ a * t + b) a x := by
   refine HasDerivAt.add_const ?_ b
@@ -324,7 +323,7 @@ lemma sum_eq_int_deriv {φ : ℝ → ℂ} {a b : ℝ} (a_lt_b : a < b)
     have subs := uIcc_subsets ⟨a₁_lt_k₁.le, k₁_lt_b₁.le⟩
     have s₁ := ih₁ (fun x hx ↦ φDiff₁ x <| subs.1 hx) <| derivφCont₁.mono subs.1
     have s₂ := ih₂ (fun x hx ↦ φDiff₁ x <| subs.2 hx) <| derivφCont₁.mono subs.2
-    convert Mathlib.Tactic.LinearCombination.add_pf s₁ s₂ using 1
+    convert Mathlib.Tactic.LinearCombination'.add_pf s₁ s₂ using 1
     · rw [← Finset.sum_Ioc_add_sum_Ioc]
       simp only [Finset.mem_Icc, Int.floor_intCast, Int.le_floor]
       exact ⟨Int.cast_le.mp <| le_trans (Int.floor_le a₁) a₁_lt_k₁.le, k₁_lt_b₁.le⟩
@@ -713,7 +712,7 @@ lemma ZetaBnd_aux1b (N : ℕ) (Npos : 1 ≤ N) {σ t : ℝ} (σpos : 0 < σ) :
     · exact fun ⦃_⦄ a ↦ a
   · filter_upwards [mem_atTop (N + 1 : ℝ)] with t ht
     have : (N ^ (-σ) - t ^ (-σ)) / σ ≤ N ^ (-σ) / σ :=
-      div_le_div_right σpos |>.mpr (by simp [Real.rpow_nonneg (by linarith)])
+      div_le_div_iff_of_pos_right σpos |>.mpr (by simp [Real.rpow_nonneg (by linarith)])
     apply le_trans ?_ this
     convert ZetaBnd_aux1a (a := N) (b := t) (by positivity) (by linarith) ?_ <;> simp [σpos]
 /-%%
@@ -1826,7 +1825,7 @@ lemma ZetaNear1BndExact:
     norm_cast
     have : 0 ≤ 1 / (σ - 1) := by apply one_div_nonneg.mpr; linarith
     simp only [Real.norm_eq_abs, abs_eq_self.mpr this, mul_div, mul_one]
-    exact div_le_div (by simp [Cpos.le]) (by simp) (by linarith) (by rfl)
+    exact div_le_div₀ (by simp [Cpos.le]) (by simp) (by linarith) (by rfl)
   · replace hσ : σ ∈ W := by
       simp only [mem_inter_iff, hV σ_ge, and_true] at hσ
       simp only [mem_Icc, σ_le, and_true, W]
@@ -1844,7 +1843,9 @@ and continuity on a compact interval otherwise.
 $|\zeta(x)^3 \cdot \zeta(x+iy)^4 \cdot \zeta(x+2iy)| \ge 1$. -/
 lemma norm_zeta_product_ge_one {x : ℝ} (hx : 0 < x) (y : ℝ) :
     ‖ζ (1 + x) ^ 3 * ζ (1 + x + I * y) ^ 4 * ζ (1 + x + 2 * I * y)‖ ≥ 1 := by
-  have ⟨h₀, h₁, h₂⟩ := one_lt_re_of_pos y hx
+  have h₀ : 1 < ( 1 + x : ℂ).re := by simp[hx]
+  have h₁ : 1 < (1 + x + I * y).re := by simp [hx]
+  have h₂ : 1 < (1 + x + 2 * I * y).re := by simp [hx]
   simpa only [one_pow, norm_mul, norm_pow, DirichletCharacter.LSeries_modOne_eq,
     LSeries_one_eq_riemannZeta, h₀, h₁, h₂] using
     DirichletCharacter.norm_LSeries_product_ge_one (1 : DirichletCharacter ℂ 1) hx y
@@ -1877,7 +1878,7 @@ lemma ZetaInvBound1 {σ t : ℝ} (σ_gt : 1 < σ) :
   · refine mul_nonneg (mul_nonneg ?_ ?_) ?_ <;> simp [Real.rpow_nonneg]
   · have s_ne_one : σ + t * I ≠ 1 := by
       contrapose! σ_gt; apply le_of_eq; apply And.left; simpa [Complex.ext_iff] using σ_gt
-    simpa using riemannZeta_ne_zero_of_one_le_re s_ne_one (by simp [σ_gt.le])
+    simpa using riemannZeta_ne_zero_of_one_le_re (by simp [σ_gt.le])
 /-%%
 \begin{proof}\leanok
 The identity
@@ -1947,8 +1948,7 @@ lemma ZetaInvBound2 :
     · exact abs_eq_self.mpr <| Real.rpow_nonneg (div_nonneg (by linarith) hc.le) _
     · apply lt_iff_le_and_ne.mpr ⟨(by simp), ?_⟩
       have : ζ (↑σ + 2 * ↑t * I) ≠ 0 := by
-        apply riemannZeta_ne_zero_of_one_le_re ?_ (by simp [σ_gt.le])
-        contrapose! σ_gt; apply le_of_eq; apply And.left; simpa [Complex.ext_iff] using σ_gt
+        apply riemannZeta_ne_zero_of_one_le_re (by simp [σ_gt.le])
       symm; exact fun h2 ↦ this (by simpa using h2)
   · replace h := h σ (2 * t) (by simp [ht']) ⟨?_, σ_le⟩
     · have : 0 ≤ Real.log |2 * t| := Real.log_nonneg (by linarith)
@@ -2137,7 +2137,7 @@ lemma ZetaInvBnd :
   have σ_ge : 1 - A / Real.log |t| ≤ σ := by
     apply le_trans ?_ hσ.1
     suffices A / Real.log |t| ^ 9 ≤ A / Real.log |t| by linarith
-    exact div_le_div Apos.le (by rfl) (by positivity) <| ZetaInvBnd_aux logt_gt_one
+    exact div_le_div₀ Apos.le (by rfl) (by positivity) <| ZetaInvBnd_aux logt_gt_one
   obtain ⟨_, _, neOne⟩ := UpperBnd_aux ⟨Apos, Ale⟩ t_gt σ_ge
   set σ' := 1 + A / Real.log |t| ^ 9
   have σ'_gt : 1 < σ' := by simp only [σ', lt_add_iff_pos_right]; positivity
@@ -2174,7 +2174,7 @@ lemma ZetaInvBnd :
       refine hC₂ σ σ' t t_gt ?_ σ'_le <| lt_trans hσ.2 σ'_gt
       apply le_trans ?_ hσ.1
       rw [tsub_le_iff_right, ← add_sub_right_comm, le_sub_iff_add_le, add_le_add_iff_left]
-      exact div_le_div hA'.1.le (by simp [A]) (by positivity) <| ZetaInvBnd_aux logt_gt_one
+      exact div_le_div₀ hA'.1.le (by simp [A]) (by positivity) <| ZetaInvBnd_aux logt_gt_one
   · apply sub_le_sub (by simp only [add_sub_cancel_left, σ']; exact_mod_cast le_rfl) ?_
     rw [mul_div_assoc, mul_assoc _ 2 _]
     apply mul_le_mul (by exact_mod_cast le_rfl) ?_ (by linarith [hσ.2]) (by positivity)
@@ -2239,11 +2239,11 @@ lemma LogDerivZetaBnd :
     exact lt_trans Real.exp_one_lt_d9 (by norm_num)
   have σ_ge' : 1 - A / Real.log |t| ^ 9 ≤ σ := by
     apply le_trans (tsub_le_tsub_left ?_ 1) σ_ge
-    apply div_le_div hA.1.le (min_le_left A A') ?_ (by rfl)
+    apply div_le_div₀ hA.1.le (min_le_left A A') ?_ (by rfl)
     exact pow_pos (lt_trans (by norm_num) logt_gt) 9
   have σ_ge'' : 1 - A' / Real.log |t| ≤ σ := by
     apply le_trans (tsub_le_tsub_left ?_ 1) σ_ge
-    apply div_le_div hA'.1.le (min_le_right A A') (lt_trans (by norm_num) logt_gt) ?_
+    apply div_le_div₀ hA'.1.le (min_le_right A A') (lt_trans (by norm_num) logt_gt) ?_
     exact le_self_pow₀ logt_gt.le (by norm_num)
   replace h := h σ t t_gt ⟨σ_ge', σ_lt⟩
   replace h' := h' σ t t_gt ⟨σ_ge'', by linarith⟩
diff --git a/lake-manifest.json b/lake-manifest.json
index 4ed2fcf7..977c0b63 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,76 +1,76 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/batteries",
+ [{"url": "https://github.com/leanprover/doc-gen4.git",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "af731107d531b39cd7278c73f91c573f40340612",
-   "name": "batteries",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/quote4",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
-   "name": "Qq",
+   "scope": "",
+   "rev": "0a8cd7afb471bb1fdd335118bf1e253a38a2af53",
+   "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
+   "inputRev": "v4.14.0",
+   "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
+  {"url": "https://github.com/MichaelStollBayreuth/EulerProducts.git",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "93bcfd774f89d3874903cab06abfbf69f327cbd9",
-   "name": "aesop",
+   "scope": "",
+   "rev": "28f8a06a85b742a0233bd74d5e0dd1fec42cc320",
+   "name": "EulerProducts",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "inputRev": "28f8a06a",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "1383e72b40dd62a566896a6e348ffe868801b172",
-   "name": "proofwidgets",
+   "scope": "",
+   "rev": "4bbdccd9c5f862bf90ff12f0a9e2c8be032b9a84",
+   "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.46",
-   "inherited": true,
+   "inputRev": "v4.14.0",
+   "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
+  {"url": "https://github.com/mhuisi/lean4-cli",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover",
-   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
+   "scope": "",
+   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/import-graph",
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "ac7b989cbf99169509433124ae484318e953d201",
-   "name": "importGraph",
+   "scope": "",
+   "rev": "d55279d2ff01759fa75752fcf1a93d1db8db18ff",
+   "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/dupuisf/BibtexQuery",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "86d0d0584f5cd165353e2f8a30c455cd0e168ac2",
-   "name": "LeanSearchClient",
+   "scope": "",
+   "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b",
+   "name": "BibtexQuery",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/acmepjz/md4lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "fe8e6e649ac8251f43c6f6f934f095ebebce7e7c",
+   "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.toml"},
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
@@ -81,65 +81,65 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/mathlib4.git",
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "e348a4cc5803ca9ec286292952ddf50e88106e57",
-   "name": "mathlib",
+   "scope": "leanprover-community",
+   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
+   "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "e348a4c",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/MichaelStollBayreuth/EulerProducts.git",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "757d816708153123280fd6467f655c9796bfd3be",
-   "name": "EulerProducts",
+   "scope": "leanprover-community",
+   "rev": "519e509a28864af5bed98033dd33b95cf08e9aa7",
+   "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "757d816",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/acmepjz/md4lean",
+   "inputRev": "v4.14.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
-   "name": "MD4Lean",
+   "scope": "leanprover-community",
+   "rev": "68280daef58803f68368eb2e53046dabcd270c9d",
+   "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v0.0.47",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+  {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "b41bc9cec7f433d6e1d74ff3b59edaaf58ad2915",
-   "name": "UnicodeBasic",
+   "scope": "leanprover-community",
+   "rev": "5a0ec8588855265ade536f35bcdcf0fb24fd6030",
+   "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.14.0",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/dupuisf/BibtexQuery",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "bdc2fc30b1e834b294759a5d391d83020a90058e",
-   "name": "BibtexQuery",
+   "scope": "leanprover-community",
+   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
+   "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/doc-gen4.git",
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "b6ae1cf11e83d972ffa363f9cdc8a2f89aaa24dc",
-   "name": "«doc-gen4»",
+   "scope": "leanprover-community",
+   "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "b6ae1cf",
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "inputRev": "v4.14.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
  "name": "PrimeNumberTheoremAnd",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index 83e9b00d..5db4ed81 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -18,10 +18,10 @@ lean_lib «PrimeNumberTheoremAnd»
 -- the commit to a more recent one.
 --
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git" @ "e348a4c"
+  "https://github.com/leanprover-community/mathlib4.git" @ "v4.14.0"
 
 require EulerProducts from git
-  "https://github.com/MichaelStollBayreuth/EulerProducts.git" @ "757d816"
+  "https://github.com/MichaelStollBayreuth/EulerProducts.git" @ "28f8a06a"
 
 meta if get_config? env = some "dev" then require «doc-gen4» from git
-  "https://github.com/leanprover/doc-gen4.git" @ "b6ae1cf"
+  "https://github.com/leanprover/doc-gen4.git" @ "v4.14.0"
diff --git a/lean-toolchain b/lean-toolchain
index 57a4710c..401bc146 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc2
+leanprover/lean4:v4.14.0
\ No newline at end of file