perf(Erdos367): narrow imports and replace proof search

LeanPool/Erdos367.lean

@@ -11,12 +11,6 @@ public import LeanPool.Erdos367.RFullLowerBound
 public import LeanPool.Erdos367.PellLimsup
 public import LeanPool.Erdos367.Core139
 public import LeanPool.Erdos367.Core4027
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.Analysis.SpecialFunctions.Gamma.Basic
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.Matroid.Init
-import Mathlib.Data.Nat.Factorial.DoubleFactorial
-import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
 
 /-!
 # Erdős Problem #367

LeanPool/Erdos367/Core139.lean

@@ -223,7 +223,7 @@ theorem T3 (s t₀ : ℕ) (hs : s.Prime) (hs3 : s ≠ 3) (ht₀ : 1 ≤ t₀ ∧
       512 * (nval s t₀ * rFullPart 3 (nval s t₀ + 1)) ^ 9 ≥ nval s t₀ ^ 9 * tval s t₀ ^ 36 := by
     have := Nat.pow_le_pow_left h2BB_ge_nt4 9
     ring_nf at *
-    aesop
+    omega
   simp_all +decide only [gt_iff_lt]
   exact lt_of_lt_of_le
     (by nlinarith [pow_pos hn_pos 9, pow_pos hn_pos 4,

LeanPool/Erdos367/PellLimsup.lean

@@ -511,7 +511,7 @@ lemma prime_sq_dvd_pellN_plus2 (p : ℕ) (hp : p.Prime) (hp5 : p % 8 = 5) :
     rw [pellN_eq, show pellX j ^ 2 = 8 * pellY j ^ 2 + 1 by
       linarith [pell_identity j]]
     ring
-  aesop
+  simpa [hj.1, hL.1] using h_div
 
 /-! ## Key lemma and main theorem
 
@@ -655,7 +655,8 @@ From an infinite set, extract a finset of any desired cardinality.
 -/
 lemma exists_finset_of_infinite {α : Type*} {S : Set α} (hS : S.Infinite) (n : ℕ) :
     ∃ T : Finset α, n ≤ T.card ∧ ∀ x ∈ T, x ∈ S := by
-  rcases hS.exists_subset_card_eq n with ⟨ T, hT ⟩; aesop
+  rcases hS.exists_subset_card_eq n with ⟨ T, hT ⟩
+  exact ⟨T, le_of_eq hT.2.symm, hT.1⟩
 
 /-
 For a finset of distinct primes, if each `p^2 ∣ m`, then `∏ p^2 ∣ m`.

LeanPool/Erdos367/RFullLowerBound.lean

@@ -89,7 +89,7 @@ lemma rFullPart_pow (r m : ℕ) (hm : m ≠ 0) (hr : r ≠ 0) :
     rFullPart r (m ^ r) = m ^ r := by
   apply Nat.factorization_inj
   · exact Nat.ne_of_gt ( rFullPart_pos _ _ ( pow_ne_zero _ hm ) );
-  · aesop;
+  · exact pow_ne_zero _ hm
   · ext p
     by_cases hp : p.Prime
     · rw [rFullPart_factorization _ _ (pow_ne_zero _ hm)]
@@ -118,12 +118,15 @@ lemma pow_dvd_rFullPart (r m d : ℕ) (hm : m ≠ 0) (hdvd : d ^ r ∣ m) :
   rw [ ← Nat.factorization_le_iff_dvd ];
   · intro p
     have := Nat.factorization_le_iff_dvd
-      (show d ^ r ≠ 0 from by aesop)
+      (show d ^ r ≠ 0 from by
+        intro hzero
+        apply hm
+        exact Nat.eq_zero_of_zero_dvd (hzero ▸ hdvd))
       (show m ≠ 0 from hm) |>.2 hdvd
     simp_all +decide [Finsupp.le_def]
     by_cases h : r ≤ m.factorization p <;> simp_all +decide [ rFullPart_factorization ];
     nlinarith [ this p ];
-  · aesop;
+  · exact fun hzero => hm (Nat.eq_zero_of_zero_dvd (hzero ▸ hdvd))
   · exact Nat.ne_of_gt ( rFullPart_pos r m hm )
 
 /-- If d^r ∣ m and m ≠ 0, then d^r ≤ B_r(m). -/