Fix the build

Author: Ruben-VandeVelde

PrimeNumberTheoremAnd/BrunTitchmarsh.lean

@@ -36,7 +36,7 @@ def primeInterSieve (x y z : ℝ) (hz : 1 ≤ z) : SelbergSieve where
     simp only [ArithmeticFunction.pdiv_apply, ArithmeticFunction.natCoe_apply,
       ArithmeticFunction.zeta_apply, hp.ne_zero, ↓reduceIte, Nat.cast_one,
       ArithmeticFunction.id_apply, one_div]
-    apply inv_lt_one
+    apply inv_lt_one_of_one_lt₀
     exact_mod_cast hp.one_lt
   level := z
   one_le_level := hz
@@ -230,7 +230,7 @@ theorem primesBetween_le (hz : 1 < z) :
   have : z ≤ z * (1+Real.log z)^3 := by
     apply le_mul_of_one_le_right
     · linarith
-    · apply one_le_pow_of_one_le _ _
+    · apply one_le_pow₀
       linarith [Real.log_nonneg (by linarith)]
   linarith [siftedSum_le _ _ _ hx hy hz, primesBetween_le_siftedSum_add x y z hz.le]
 
@@ -403,7 +403,7 @@ theorem IsBigO.nat_Top_of_atTop (f g : ℕ → ℝ) (h : f =O[Filter.atTop] g) (
         simp
   · by_cases hg : g n = 0
     · simp [hg, h0]
-    rw [← mul_inv_le_iff']
+    rw [← mul_inv_le_iff₀]
     apply Finset.le_max'
     simp only [Finset.mem_insert, Finset.mem_image, Finset.mem_range]
     exact .inr ⟨n, by omega, rfl⟩

PrimeNumberTheoremAnd/Consequences.lean

@@ -49,7 +49,7 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy
       ← intervalIntegral.integral_deriv_eq_sub hϕ₁ hϕ₂, ← intervalIntegral.integral_const_mul,
       intervalIntegral.integral_of_le hxy.le, integral_Ioc_eq_integral_Ioo,
       integral_Icc_eq_integral_Ioo]
-    apply setIntegral_congr
+    apply setIntegral_congr_fun
     · exact measurableSet_Ioo
     · intro z hz
       have : ⌊z⌋₊ = ⌊y⌋₊ := by
@@ -283,36 +283,6 @@ lemma abel_summation {a : ArithmeticFunction ℝ} (x y : ℝ) (hx : 0 < x) (hxy
       intervalIntegral.integral_add_adjacent_intervals (hab.trans hbc) hcd]
   simp [A, intervalIntegral.integral_of_le hxy.le, MeasureTheory.integral_Icc_eq_integral_Ioc]
 
-lemma nth_prime_one_eq_three : nth Nat.Prime 1 = 3 := nth_count prime_three
-
-@[simp]
-lemma Nat.primeCounting'_eq_zero_iff {n : ℕ} : n.primeCounting' = 0 ↔ n ≤ 2 := by
-  refine ⟨?_, ?_⟩
-  · contrapose!
-    intro h
-    replace h : 3 ≤ n := by omega
-    have := monotone_primeCounting' h
-    have := nth_prime_one_eq_three ▸ primeCounting'_nth_eq 1
-    omega
-  · intro hn
-    have := zeroth_prime_eq_two ▸ primeCounting'_nth_eq 0
-    have := monotone_primeCounting' hn
-    omega
-
-
-@[simp]
-lemma Nat.primeCounting_eq_zero_iff {n : ℕ} : n.primeCounting = 0 ↔ n ≤ 1 := by
-  simp [Nat.primeCounting]
-
-@[simp]
-lemma Nat.primeCounting_zero : Nat.primeCounting 0 = 0 :=
-  Nat.primeCounting_eq_zero_iff.mpr zero_le_one
-
-@[simp]
-lemma Nat.primeCounting_one : Nat.primeCounting 1 = 0 :=
-  Nat.primeCounting_eq_zero_iff.mpr le_rfl
-
-
 -- @[simps]
 -- def ArithmeticFunction.primeCounting : ArithmeticFunction ℝ where
 --   toFun x := Nat.primeCounting ⌊x⌋₊
@@ -432,7 +402,7 @@ lemma th43_b (x : ℝ) (hx : 2 ≤ x) :
       symm
       apply Set.Ico_union_Icc_eq_Icc ?_ hx
       norm_num
-    rw [this, integral_union]
+    rw [this, setIntegral_union]
     · simp only [add_left_eq_self]
       apply integral_eq_zero_of_ae
       simp only [measurableSet_Ico, ae_restrict_eq]
@@ -699,7 +669,7 @@ lemma sum_von_mangoldt_sub_sum_primes_le (x : ℝ) (hx: 2 ≤ x) :
           calc
             _ ≤ x^(1:ℝ) := by
               apply rpow_le_rpow_of_exponent_le hx_one
-              apply inv_le_one
+              apply inv_le_one_of_one_le₀
               simp only [one_le_cast]
               exact one_le_two.trans hk.1
             _ = _ := by
@@ -720,7 +690,7 @@ lemma sum_von_mangoldt_sub_sum_primes_le (x : ℝ) (hx: 2 ≤ x) :
             apply floor_le_floor
             apply rpow_le_rpow_of_exponent_le hx_one
             simp at hk
-            rw [inv_le_inv _ zero_lt_two]
+            rw [inv_le_inv₀ _ zero_lt_two]
             . exact ofNat_le_cast.mpr hk.1
             simp only [cast_pos]
             exact lt_of_lt_of_le zero_lt_two hk.1
@@ -821,7 +791,7 @@ theorem WeakPNT'' : (fun x ↦ ∑ n in (Iic ⌊x⌋₊), Λ n) ~[atTop] (fun x
     intro b hb
     have hb' : 0 ≤ b := le_of_lt (lt_of_lt_of_le (inv_pos_of_pos hε) hb)
     rw [abs_of_nonneg, abs_of_nonneg hb']
-    . apply LE.le.trans _ ((inv_pos_le_iff_one_le_mul' hε).mp hb)
+    . apply LE.le.trans _ ((inv_le_iff_one_le_mul₀' hε).mp hb)
       linarith [Nat.lt_floor_add_one b]
     rw [sub_nonneg]
     exact floor_le hb'
@@ -1070,7 +1040,7 @@ theorem sum_mobius_div_self_le (N : ℕ) : |∑ n in range N, μ n / (n : ℚ)|
   rw [sum_congr rfl (g := fun d ↦ (μ d : ℚ) * ⌊(N : ℚ) / (d : ℚ)⌋)] at h_sum
   swap
   intros
-  rw [show (N : ℚ) = ((N : ℤ) : ℚ) by norm_cast, Rat.floor_int_div_nat_eq_div]
+  rw [show (N : ℚ) = ((N : ℤ) : ℚ) by norm_cast, Rat.floor_intCast_div_natCast]
   congr
 
   /- Next, we establish bounds for the error term -/

PrimeNumberTheoremAnd/Fourier.lean

@@ -61,5 +61,5 @@ theorem fourierIntegral_self_add_deriv_deriv (f : W21) (u : ℝ) :
   simp [f.hf, l1, add_mul, Real.fourierIntegral_deriv f.hf' l5 f.hf'', Real.fourierIntegral_deriv f.hf l4 f.hf']
   field_simp [pi_ne_zero] ; ring_nf ; simp
 
-@[simp] lemma deriv_ofReal : deriv ofReal' = fun _ => 1 := by
+@[simp] lemma deriv_ofReal : deriv ofReal = fun _ => 1 := by
   ext x ; exact ((hasDerivAt_id x).ofReal_comp).deriv

PrimeNumberTheoremAnd/Mathlib/Analysis/Asymptotics/Asymptotics.lean

@@ -1,6 +1,6 @@
 import Mathlib.Analysis.Asymptotics.Asymptotics
-import Mathlib.Topology.Algebra.Order.Compact
 import Mathlib.Analysis.SpecialFunctions.Log.Basic
+import Mathlib.Topology.Order.Compact
 
 open Filter Topology
 

PrimeNumberTheoremAnd/Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

@@ -1,6 +1,6 @@
 import Mathlib.MeasureTheory.Function.LocallyIntegrable
 import Mathlib.MeasureTheory.Integral.IntegrableOn
-import Mathlib.Topology.Algebra.Order.Compact
+import Mathlib.Topology.Order.Compact
 
 open MeasureTheory MeasureTheory.Measure Set Function TopologicalSpace Bornology Filter
 

PrimeNumberTheoremAnd/Mathlib/MeasureTheory/Integral/Asymptotics.lean

@@ -49,7 +49,7 @@ theorem LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg
     [MeasurableNeg α] [μ.IsNegInvariant] (hf : LocallyIntegrable f μ)
     (hsymm : norm ∘ f =ᵐ[μ] norm ∘ f ∘ Neg.neg) (ho : f =O[atTop] g)
     (hg : IntegrableAtFilter g atTop μ) : Integrable f μ := by
-  refine (isEmpty_or_nonempty α).casesOn (fun _ ↦ Integrable.of_finite μ f) (fun _ ↦ ?_)
+  refine (isEmpty_or_nonempty α).casesOn (fun _ ↦ Integrable.of_finite) (fun _ ↦ ?_)
   let a := -|Classical.arbitrary α|
   have h_int : IntegrableOn f (Ici a) μ :=
     LocallyIntegrableOn.integrableOn_of_isBigO_atTop (hf.locallyIntegrableOn _) ho hg

PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean

@@ -417,7 +417,7 @@ theorem selberg_bound_muPlus (n : ℕ) (hn : n ∈ divisors P) :
     simp only [f]
     by_cases h : n = d1.lcm d2
     rw [if_pos h, if_pos h]
-    apply mul_le_one (s.selberg_bound_weights d1) (abs_nonneg <| γ d2)
+    apply mul_le_one₀ (s.selberg_bound_weights d1) (abs_nonneg <| γ d2)
       (s.selberg_bound_weights d2)
     rw [if_neg h, if_neg h]
   · rw [← Finset.sum_product']

PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean

@@ -328,7 +328,7 @@ lemma sqrt_le_self (x : ℝ) (hx : 1 ≤ x) : Real.sqrt x ≤ x := by
   refine Iff.mpr Real.sqrt_le_iff ?_
   constructor
   · linarith
-  refine le_self_pow hx ?right.h
+  refine le_self_pow₀ hx ?right.h
   norm_num
 
 lemma Nat.squarefree_dvd_pow (a b N: ℕ) (ha : Squarefree a) (hab : a ∣ b ^ N) : a ∣ b := by
@@ -473,7 +473,7 @@ theorem boundingSum_ge_sum (s : SelbergSieve) (hnu : s.nu = (ζ : ArithmeticFunc
       ArithmeticFunction.zeta_apply, Nat.cast_ite, CharP.cast_eq_zero, Nat.cast_one,
       ArithmeticFunction.id_apply]
     rw [if_neg, one_div]
-    apply inv_lt_one; norm_cast
+    apply inv_lt_one_of_one_lt₀; norm_cast
     exact hpp.one_lt
     exact hpp.ne_zero
   apply le_of_eq