Reduce IwaniecLinearSieve arithmetic elaboration cost

LeanPool/IwaniecLinearSieve/Jacobsthal/Reduction.lean

@@ -44,7 +44,7 @@ theorem exists_covering_length_le (hL : LinearSieveEstimate)
   refine ⟨K / (c * c'), max z₀ 2, fun z hz S hS hcard x m hm ↦ ?_⟩
   have hz0 : z₀ ≤ z := (le_max_left _ _).trans hz
   have hz2 : 2 ≤ z := (le_max_right _ _).trans hz
-  have hlog : 0 < log z := log_pos (by linarith)
+  have hlog : 0 < log z := log_pos (by linarith only [hz2])
   have hRz := R_pos z
   set M := rosserMain true (C₀ * z ^ 2) z
   obtain ⟨hmain, hcount⟩ := hL z hz0
@@ -56,7 +56,7 @@ theorem exists_covering_length_le (hL : LinearSieveEstimate)
     exact h q hq hqk
   rw [hzero, card_empty, Nat.cast_zero] at hsieve
   -- `M ≥ R(z) c / log z`
-  have hM : R z * (c / log z) ≤ M := by nlinarith
+  have hM : R z * (c / log z) ≤ M := by nlinarith only [hmain]
   have hM0 : 0 ≤ M := (mul_nonneg hRz.le (div_pos hc hlog).le).trans hM
   have hprod := R_le_prod_of_card_eq hS hcard
   have h1 : (m : ℝ) * M ≤ #(rosserSet true (C₀ * z ^ 2) z) := by
@@ -65,7 +65,7 @@ theorem exists_covering_length_le (hL : LinearSieveEstimate)
       refine mul_le_mul_of_nonneg_left ?_ m.cast_nonneg
       calc M = R z * (M / R z) := by field_simp
         _ ≤ _ := mul_le_mul_of_nonneg_right hprod (div_nonneg hM0 hRz.le)
-    linarith
+    linarith only [hsieve, this]
   have hRlog : c' ≤ R z * log z := by
     have := hR z hz2
     rwa [div_le_iff₀ hlog] at this
@@ -82,9 +82,9 @@ theorem exists_covering_length_le (hL : LinearSieveEstimate)
       exact (mul_le_mul_of_nonneg_left hM hm0).trans (h1.trans hcount)
     have e3 : K * z ^ 2 / log z ^ 2 * log z ^ 2 = K * z ^ 2 := by
       field_simp
-    linarith
+    linarith only [e1, e2, e3]
   rw [div_mul_eq_mul_div, le_div_iff₀ (mul_pos hc hc')]
-  linarith
+  linarith only [h2]
 
 
 /-- The primes below `p_N + 1`, where `p_N = Nat.nth Nat.Prime (N - 1)` is the `N`-th prime, are

LeanPool/IwaniecLinearSieve/Jacobsthal/ShiftedSieve.lean

@@ -323,7 +323,7 @@ theorem abs_card_filter_dvd_sub_le (x : ℤ) (X : ℕ) {d : ℕ} (hd : 0 < d) :
     push_cast
     ring
   have hX : (0 : ℚ) ≤ X / d := by positivity
-  have hle : ⌈u⌉ ≤ ⌈v⌉ := Int.ceil_mono (by rw [hvu]; linarith)
+  have hle : ⌈u⌉ ≤ ⌈v⌉ := Int.ceil_mono (by rw [hvu]; linarith only [hX])
   rw [max_eq_left (sub_nonneg.2 hle)] at h
   have hq : |((⌈v⌉ - ⌈u⌉ : ℤ) : ℚ) - X / d| ≤ 1 := by
     have h1 := Int.le_ceil v
@@ -437,7 +437,7 @@ theorem shiftedSieve_of_bijOn (y : ℝ) {S : Finset ℕ} {e : ℕ → ℕ}
       ∑ A ∈ T.powerset, w A * #((range X).filter fun k : ℕ ↦ (n A : ℤ) ∣ x + k) := by
     rw [← sum_sub_distrib]
     exact sum_le_sum hc
-  linarith
+  linarith only [hb, hd, he', hsum]
 
 
 /-- Any `π(z)` primes can be matched with the primes below `z` so that each prime below `z` is

LeanPool/IwaniecLinearSieve/LinearSieve/Calculus.lean

@@ -50,45 +50,45 @@ theorem mainMaj_antitone : ∀ lower, Antitone (mainMaj lower)
   | true => fSieve_antitone
   | false => fun u v h => by
     simp only [mainMaj_false]
-    exact add_le_add (FSieve_antitone h) (max_le_max (by linarith) le_rfl)
+    exact add_le_add (FSieve_antitone h) (max_le_max (by linarith only [h]) le_rfl)
 
 theorem mainMaj_le_MSieve : ∀ (lower : Bool) (s : ℝ), mainMaj lower s ≤ MSieve s
   | true, s => by
     have := FSieve_nonneg s; have := le_max_right (3 - s) 0
     simp only [mainMaj_true, MSieve]; linarith
   | false, s => by
     have := fSieve_nonneg s
-    simp only [mainMaj_false, MSieve]; linarith
+    simp only [mainMaj_false, MSieve]; linarith only [this]
 
 /-- `g₂(s) = ∫_s^∞ (3 - (t-1))⁺/(t-1) dt` for `s ≥ 2`. -/
 theorem g_two_eq_integral {s : ℝ} (hs : 2 ≤ s) :
     IntegrableOn (fun t => max (3 - (t - 1)) 0 / (t - 1)) (Ioi s) ∧
       g 2 s = ∫ t in Ioi s, max (3 - (t - 1)) 0 / (t - 1) := by
   have hz : ∀ t : ℝ, 4 ≤ t → max (3 - (t - 1)) 0 / (t - 1) = 0 := fun t ht => by
-    rw [max_eq_right (by linarith), zero_div]
+    rw [max_eq_right (by linarith only [ht]), zero_div]
   rcases le_or_gt s 4 with hs4 | hs4
   · have heq : EqOn (fun t : ℝ => max (3 - (t - 1)) 0 / (t - 1)) (fun t => 3 / (t - 1) - 1)
         (Icc s 4) := fun t ht => by
-      have : 0 < t - 1 := by linarith [ht.1]
+      have : 0 < t - 1 := by linarith only [ht.1, hs, ht]
       simp only
-      rw [max_eq_left (by linarith [ht.2])]
+      rw [max_eq_left (by linarith only [ht.2, ht])]
       field_simp
     have hcont : ContinuousOn (fun t : ℝ => 3 / (t - 1) - 1) (Icc s 4) :=
       (continuousOn_const.div (continuousOn_id.sub continuousOn_const) fun t ht => by
-        simp only [Pi.sub_apply, id]; linarith [ht.1]).sub continuousOn_const
+        simp only [Pi.sub_apply, id]; linarith only [ht.1, hs, ht]).sub continuousOn_const
     obtain ⟨hI, hE⟩ := integral_Ioi_eq_of_eq_zero hs4
       (((hcont.congr heq).integrableOn_Icc).mono_set Ioc_subset_Icc_self) hz
     refine ⟨hI, ?_⟩
     rw [hE, intervalIntegral.integral_congr (heq.mono (uIcc_of_le hs4).subset)]
     have hderiv : ∀ t ∈ uIcc s 4, HasDerivAt (fun t => 3 * log (t - 1) - t) (3 / (t - 1) - 1) t :=
       fun t ht => by
         rw [uIcc_of_le hs4] at ht
-        have h1 : t - 1 ≠ 0 := by linarith [ht.1]
+        have h1 : t - 1 ≠ 0 := by linarith only [ht.1, hs, ht]
         have := ((((hasDerivAt_id' t).sub_const 1).log h1).const_mul 3).sub (hasDerivAt_id' t)
         convert this using 1; field_simp
     rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hderiv
       (hcont.mono (uIcc_of_le hs4).subset |>.intervalIntegrable), g_two_eq ⟨hs, hs4⟩,
-      log_div (by norm_num) (by linarith)]
+      log_div (by norm_num) (by linarith only [hs])]
     norm_num; ring
   · obtain ⟨hI, hE⟩ := integral_Ioi_eq_of_eq_zero le_rfl (by simp) fun t ht => hz t (by linarith)
     exact ⟨hI, by rw [hE, intervalIntegral.integral_same, g_two_of_four_le hs4.le]⟩
@@ -117,7 +117,7 @@ theorem mainMaj_false_eq_integral (s : ℝ) :
 
 /-- `mainMaj` in terms of `fr`: `M true = f` and, on `s ≥ 3`, `M false = F`. -/
 theorem mainMaj_false_of_three_le {s : ℝ} (hs : 3 ≤ s) : mainMaj false s = FSieve s := by
-  rw [mainMaj_false, max_eq_right (by linarith), add_zero]
+  rw [mainMaj_false, max_eq_right (by linarith only [hs]), add_zero]
 
 /-! ### `errMaj` -/
 
@@ -172,7 +172,7 @@ theorem errMaj_mem : ∀ (lower : Bool) (s : ℝ),
   | false, s => majF_mem s
 
 theorem errMaj_le_two (lower : Bool) (s : ℝ) : errMaj lower s ≤ 2 := by
-  linarith [(errMaj_mem lower s).2, bigM_le_three s]
+  linarith only [(errMaj_mem lower s).2, bigM_le_three s]
 
 theorem errMaj_false_of_le_three {s : ℝ} (hs : s ≤ 3) : errMaj false s = 1 :=
   majF_of_le_three hs
@@ -190,9 +190,9 @@ theorem tendsto_errMaj_atTop : ∀ lower, Tendsto (errMaj lower) atTop (𝓝 0)
 
 theorem errMaj_shift_pos (lower : Bool) {t : ℝ} (ht : 1 < t) :
     0 < errMaj lower (t - 1) * t / (t - 1) ^ 2 := by
-  have h1 : 0 < t - 1 := by linarith
+  have h1 : 0 < t - 1 := by linarith only [ht]
   have := errMaj_pos lower (t - 1)
-  have : 0 < t := by linarith
+  have : 0 < t := by linarith only [ht]
   positivity
 
 /-- (3.13), (3.14): for `s ≥ 2` (`lower = true`) or `s ≥ 3` (`lower = false`),
@@ -207,7 +207,7 @@ theorem errMaj_eq_integral (lower : Bool) {s : ℝ} (hs : errLower lower ≤ s)
       (errMaj (!lower) (t - 1) * t / (t - 1) ^ 2) t := fun t ht =>
     (hasDerivAt_errMaj lower (hs.trans_lt ht)).neg.congr_deriv (by ring)
   have hpos : ∀ t ∈ Ioi s, 0 ≤ errMaj (!lower) (t - 1) * t / (t - 1) ^ 2 := fun t ht =>
-    (errMaj_shift_pos _ (by linarith [ht.out])).le
+    (errMaj_shift_pos _ (by linarith only [ht.out, hs, h2, ht])).le
   have hlim : Tendsto (fun t => -errMaj lower t) atTop (𝓝 0) := by
     simpa using (tendsto_errMaj_atTop lower).neg
   refine ⟨integrableOn_Ioi_deriv_of_nonneg hcont hderiv hpos hlim, ?_⟩