Merge pull request #180 from pitmonticone/refactor-simp

Refactor a few proofs

PrimeNumberTheoremAnd/BrunTitchmarsh.lean

@@ -63,7 +63,7 @@ theorem primesBetween_subset :
     (Finset.Icc (Nat.ceil x) (Nat.floor (x+y))).filter (fun d => ∀ p:ℕ, p.Prime → p ≤ z → ¬p ∣ d) ∪
     (Finset.Icc 1 (Nat.floor z)) := by
   intro p
-  simp
+  simp only [Finset.mem_filter, Finset.mem_Icc, Nat.ceil_le, Finset.mem_union, and_imp]
   intro hx hxy hp
   by_cases hpz : p ≤ z
   · right
@@ -93,7 +93,7 @@ theorem primesBetween_le_siftedSum_add :
   rw[siftedSum_eq_card]
   gcongr
   rw[Nat.card_Icc]
-  simp
+  simp only [add_tsub_cancel_right]
   apply Nat.floor_le
   linarith
 
@@ -130,7 +130,7 @@ theorem multSum_eq (d : ℕ) (hd : d ≠ 0):
     (primeInterSieve x y z hz).multSum d = ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) := by
   unfold Sieve.multSum
   rw[primeInterSieve]
-  simp
+  simp only [Finset.sum_boole, Nat.cast_inj]
   trans ↑(Finset.Ioc (Nat.ceil x - 1) (Nat.floor (x+y)) |>.filter (d ∣ ·) |>.card)
   · rw [←Nat.Icc_succ_left]
     congr
@@ -152,7 +152,7 @@ theorem Nat.ceil_le_self_add_one (x : ℝ) (hx : 0 ≤ x) : Nat.ceil x ≤ x + 1
 
 theorem floor_approx (x : ℝ) (hx : 0 ≤ x) : ∃ C, |C| ≤ 1 ∧  ↑((Nat.floor x)) = x + C := by
   use ↑(Nat.floor x) - x
-  simp
+  simp only [add_sub_cancel, and_true]
   rw[abs_le]
   constructor
   · simp only [neg_le_sub_iff_le_add]
@@ -162,7 +162,7 @@ theorem floor_approx (x : ℝ) (hx : 0 ≤ x) : ∃ C, |C| ≤ 1 ∧  ↑((Nat.f
 
 theorem ceil_approx (x : ℝ) (hx : 0 ≤ x) : ∃ C, |C| ≤ 1 ∧  ↑((Nat.ceil x)) = x + C := by
   use ↑(Nat.ceil x) - x
-  simp
+  simp only [add_sub_cancel, and_true]
   rw[abs_le]
   constructor
   · simp only [neg_le_sub_iff_le_add]
@@ -290,7 +290,7 @@ theorem tmp (N : ℕ) : ((Finset.range N).filter Nat.Prime).card ≤ 4 * (N / Re
   · norm_cast
     apply Finset.card_le_card
     intro n
-    simp
+    simp only [Finset.mem_filter, Finset.mem_range, and_imp]
     refine fun hnN hp ↦ ⟨by omega, hp⟩
   rw [← primesBetween_one]
   by_cases hN : N = 0
@@ -451,7 +451,7 @@ theorem IsBigO.nat_Top_of_atTop (f g : ℕ → ℝ) (h : f =O[Filter.atTop] g) (
     · simp [hg, h0]
     rw [← mul_inv_le_iff']
     apply Finset.le_max'
-    simp
+    simp only [Finset.mem_insert, Finset.mem_image, Finset.mem_range]
     exact .inr ⟨n, by omega, rfl⟩
     · simp [hg]
 
@@ -535,15 +535,17 @@ theorem card_isPrimePow_isBigO :
 
 theorem card_range_filter_isPrimePow_le : ∃ C, ∀ N, ((Finset.range N).filter IsPrimePow).card ≤ C * (N / Real.log N) := by
   convert_to (fun N ↦ ((Finset.range N).filter IsPrimePow).card : ℕ → ℝ) =O[⊤] (fun N ↦ (N / Real.log N))
-  · simp
+  · simp only [isBigO_top, RCLike.norm_natCast, norm_div, Real.norm_eq_abs]
     peel with C N
     by_cases hN : N = 0
     · simp [hN]
     rw [abs_of_nonneg]
     apply Real.log_nonneg
     norm_cast; omega
   apply IsBigO.nat_Top_of_atTop _ _ card_isPrimePow_isBigO
-  simp
+  simp only [div_eq_zero_iff, Nat.cast_eq_zero, Real.log_eq_zero, Nat.cast_eq_one, or_self_left,
+    Finset.card_eq_zero, forall_eq_or_imp, Finset.range_zero, Finset.filter_empty, Finset.range_one,
+    true_and]
   refine ⟨rfl, ?_⟩
   intro a ha
   exfalso

PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean

@@ -115,7 +115,7 @@ theorem nu_pos_of_dvd_prodPrimes {d : ℕ} (hd : d ∣ P) : 0 < ν d := by
     0 < ∏ p in d.primeFactors, ν p := by
       apply prod_pos
       intro p hpd
-      have hp_prime : p.Prime := by exact prime_of_mem_primeFactors hpd
+      have hp_prime : p.Prime := prime_of_mem_primeFactors hpd
       have hp_dvd : p ∣ P := (dvd_of_mem_primeFactors hpd).trans hd
       exact s.nu_pos_of_prime p hp_prime hp_dvd
     _ = ν d := s.nu_mult.prod_factors_of_mult ν (Squarefree.squarefree_of_dvd hd s.prodPrimes_squarefree)

PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean

@@ -477,7 +477,9 @@ theorem boundingSum_ge_sum (s : SelbergSieve) (hnu : s.nu = (ζ : ArithmeticFunc
     simp
   · intro p hpp _
     rw[hnu]
-    simp
+    simp only [ArithmeticFunction.pdiv_apply, ArithmeticFunction.natCoe_apply,
+      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
     exact hpp.one_lt

PrimeNumberTheoremAnd/MellinCalculus.lean

@@ -123,7 +123,7 @@ lemma IntervalIntegral.integral_eq_integral_of_support_subset_Icc {a b : ℝ} {
     ← integral_indicator measurableSet_Icc, indicator_eq_self.2 h]
   · by_cases hab2 : b = a
     · rw [hab2] at h ⊢
-      simp [intervalIntegral.integral_same]
+      simp only [intervalIntegral.integral_same]
       simp only [Icc_self] at h
       have : ∫ (x : ℝ), f x ∂μ = ∫ (x : ℝ) in {a}, f x ∂μ := by
         rw [ ← integral_indicator (by simp), indicator_eq_self.2 h]
@@ -1274,7 +1274,7 @@ lemma Smooth1Properties_above_aux2 {x y ε : ℝ} (hε : ε ∈ Ioo 0 1) (hy : y
   · have : y ^ (1 / ε) ≤ y := by
       nth_rewrite 2 [← rpow_one y]
       exact rpow_le_rpow_of_exponent_ge ypos y1 (by linarith [one_lt_one_div εpos ε1])
-    have pos : 0 < y ^ (1 / ε) := by apply rpow_pos_of_pos <| ypos
+    have pos : 0 < y ^ (1 / ε) := rpow_pos_of_pos ypos _
     rw [ge_iff_le, div_le_iff, div_mul_eq_mul_div, le_div_iff', mul_comm] <;> try linarith
   · rw [ge_iff_le, le_div_iff <| ypos]; exact (mul_le_iff_le_one_right zero_lt_two).mpr y1
 /-%%

PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean

@@ -467,8 +467,8 @@ lemma ResidueTheoremAtOrigin' {z w c : ℂ} (h1 : z.re < 0) (h2 : z.im < 0) (h3
 
 theorem ResidueTheoremInRectangle (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im)
     (pInRectInterior : Rectangle z w ∈ 𝓝 p) : RectangleIntegral' (λ s => c / (s - p)) z w = c := by
-  simp [rectangle_mem_nhds_iff, mem_reProdIm, uIoo_of_le zRe_le_wRe, uIoo_of_le zIm_le_wIm]
-    at pInRectInterior
+  simp only [rectangle_mem_nhds_iff, uIoo_of_le zRe_le_wRe, uIoo_of_le zIm_le_wIm, mem_reProdIm,
+    mem_Ioo] at pInRectInterior
   rw [RectangleIntegral.translate', RectangleIntegral']
   have : 1 / (2 * ↑π * I) * (2 * I * ↑π * c) = c := by field_simp [two_pi_I_ne_zero] ; ring
   rwa [ResidueTheoremAtOrigin'] ; all_goals { simp [*] }

PrimeNumberTheoremAnd/Wiener.lean

@@ -75,7 +75,7 @@ lemma smooth_urysohn_support_Ioo (h1 : a < b) (h3: c < d) :
           rw [Set.indicator_apply]
           split_ifs with h
           · have : Ψ x ∈ Set.range Ψ := by simp only [Set.mem_range, exists_apply_eq_apply]
-            have : Ψ x ∈ Set.Icc 0 1 := by exact hΨrange this
+            have : Ψ x ∈ Set.Icc 0 1 := hΨrange this
             simpa using this.2
           · simp only [Set.mem_Ioo, Pi.one_apply] at *
             simp only [not_and_or, not_lt] at h
@@ -1140,7 +1140,7 @@ lemma gg_of_hh {x : ℝ} (hx : x ≠ 0) (i : ℝ) : gg x i = x⁻¹ * hh (1 / (2
   field_simp [gg, hh]
 
 lemma gg_l1 {x : ℝ} (hx : 0 < x) (n : ℕ) : |gg x n| ≤ 1 / n := by
-  simp [gg_of_hh hx.ne.symm, abs_mul]
+  simp only [gg_of_hh hx.ne.symm, one_div, mul_inv_rev, abs_mul]
   apply mul_le_mul le_rfl (hh_le _ _ (by positivity)) (by positivity) (by positivity) |>.trans (le_of_eq ?_)
   simp [abs_inv, abs_eq_self.mpr hx.le] ; field_simp
 
@@ -1227,7 +1227,7 @@ theorem sum_le_integral {x₀ : ℝ} {f : ℝ → ℝ} {n : ℕ} (hf : AntitoneO
 
   have l4 : IntervalIntegrable f volume x₀ (x₀ + 1) := by
     apply IntegrableOn.intervalIntegrable
-    simp
+    simp only [ge_iff_le, le_add_iff_nonneg_right, zero_le_one, uIcc_of_le]
     apply hfi.mono_set
     apply Icc_subset_Icc ; linarith ; simp
   have l5 x (hx : x ∈ Ioc x₀ (x₀ + 1)) : (fun x ↦ f (x₀ + 1)) x ≤ f x := by
@@ -1254,11 +1254,11 @@ theorem sum_le_integral {x₀ : ℝ} {f : ℝ → ℝ} {n : ℕ} (hf : AntitoneO
   simp [add_comm _ x₀] at this ; rw [this]
   rw [intervalIntegral.integral_add_adjacent_intervals]
   · apply IntegrableOn.intervalIntegrable
-    simp
+    simp only [ge_iff_le, le_add_iff_nonneg_right, zero_le_one, uIcc_of_le]
     apply hfi.mono_set
     apply Icc_subset_Icc ; linarith ; simp
   · apply IntegrableOn.intervalIntegrable
-    simp
+    simp only [ge_iff_le, add_le_add_iff_left, le_add_iff_nonneg_left, Nat.cast_nonneg, uIcc_of_le]
     apply hfi.mono_set
     apply Icc_subset_Icc ; linarith ; simp
 
@@ -1334,7 +1334,7 @@ lemma hh_integrable_aux (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
   · convert_to IntegrableOn g' _
     exact integrableOn_Ioi_deriv_of_nonneg k3 key k4 k1
   · have := integral_Ioi_of_hasDerivAt_of_nonneg k3 key k4 k1
-    simp [g₀, g'] at this ⊢
+    simp only [mul_inv_rev, inv_div, mul_neg, ↓reduceIte, sub_neg_eq_add, g', g₀] at this ⊢
     convert this using 1 ; field_simp ; ring
 
 lemma hh_integrable (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
@@ -1832,7 +1832,7 @@ lemma WI_summable {f : ℕ → ℝ} {g : ℝ → ℝ} (hg : HasCompactSupport g)
     Summable (fun n => f n * g (n / x)) := by
   obtain ⟨M, hM⟩ := hg.bddAbove.mono subset_closure
   apply summable_of_finite_support
-  simp ; apply Finite.inter_of_right ; rw [finite_iff_bddAbove]
+  simp only [Function.support_mul] ; apply Finite.inter_of_right ; rw [finite_iff_bddAbove]
   exact ⟨Nat.ceil (M * x), fun i hi => by simpa using Nat.ceil_mono ((div_le_iff hx).mp (hM hi))⟩
 
 lemma WI_sum_le {f : ℕ → ℝ} {g₁ g₂ : ℝ → ℝ} (hf : 0 ≤ f) (hg : g₁ ≤ g₂) (hx : 0 < x)
@@ -1856,7 +1856,8 @@ lemma WI_sum_Iab_le {f : ℕ → ℝ} (hpos : 0 ≤ f) {C : ℝ} (hcheby : cheby
   rw [tsum_eq_sum l1, div_le_iff hx, mul_assoc, mul_assoc]
   apply Finset.sum_le_sum l2 |>.trans
   have := hcheby ⌈b * x⌉₊ ; simp at this ; apply this.trans
-  have : 0 ≤ C := by have := hcheby 1 ; simp [cumsum] at this ; exact (abs_nonneg _).trans this
+  have : 0 ≤ C := by have := hcheby 1 ; simp only [cumsum, Finset.range_one, Complex.norm_eq_abs,
+    abs_ofReal, Finset.sum_singleton, Nat.cast_one, mul_one] at this ; exact (abs_nonneg _).trans this
   refine mul_le_mul_of_nonneg_left ?_ this
   apply (Nat.ceil_lt_add_one (by positivity)).le.trans
   linarith
@@ -1891,7 +1892,7 @@ lemma WI_tendsto_aux (a b : ℝ) {A : ℝ} (hA : 0 < A) :
   intro x hx1 hx2
   constructor
   · simpa [lt_div_iff' hA]
-  · simp [Real.dist_eq] at hx2 ⊢
+  · simp only [Real.dist_eq, dist_zero_right, Real.norm_eq_abs] at hx2 ⊢
     have : |x / A - (b - a)| = |x - A * (b - a)| / A := by
       rw [← abs_eq_self.mpr hA.le, ← abs_div, abs_eq_self.mpr hA.le] ; congr ; field_simp
     rwa [this, div_lt_iff' hA]
@@ -1927,7 +1928,7 @@ theorem residue_nonneg {f : ℕ → ℝ} (hpos : 0 ≤ f)
       (h1.continuous.integrable_of_hasCompactSupport h2).integrableOn
     have r3 : Ico 1 2 ⊆ Function.support ψ := by intro x hx ; have := h4 x ; simp [hx] at this ⊢ ; linarith
     have r4 : Ico 1 2 ⊆ Function.support ψ ∩ Ioi 0 := by
-      simp [r3] ; apply Ico_subset_Icc_self.trans ; rw [Icc_subset_Ioi_iff] <;> linarith
+      simp only [subset_inter_iff, r3, true_and] ; apply Ico_subset_Icc_self.trans ; rw [Icc_subset_Ioi_iff] <;> linarith
     have r5 : 1 ≤ volume ((Function.support fun y ↦ ψ y) ∩ Ioi 0) := by convert volume.mono r4 ; norm_num
     simpa [setIntegral_pos_iff_support_of_nonneg_ae r1 r2] using zero_lt_one.trans_le r5
   have := div_nonneg l3 l4.le ; field_simp at this ; exact this
@@ -2097,7 +2098,8 @@ lemma tendsto_S_S_zero {f : ℕ → ℝ} (hpos : 0 ≤ f) (hcheby : cheby f) :
   have l2 : |cumsum f ⌈ε * ↑N⌉₊ / ↑N| ≤ C * ⌈ε * N⌉₊ / N := by
     have r1 := hC ⌈ε * N⌉₊
     have r2 : 0 ≤ cumsum f ⌈ε * N⌉₊ := by apply cumsum_nonneg hpos
-    simp [abs_div, abs_eq_self.mpr r2, abs_eq_self.mpr (hpos _)] at r1 ⊢
+    simp only [Complex.norm_eq_abs, abs_ofReal, abs_eq_self.mpr (hpos _), abs_div,
+      abs_eq_self.mpr r2, Nat.abs_cast, ge_iff_le] at r1 ⊢
     apply div_le_div_of_nonneg_right r1 (by positivity)
   simpa [← S_sub_S h2.2] using l2.trans_lt h1