From d4a477e6f35ac625627332f5f2a19467f32d145a Mon Sep 17 00:00:00 2001 From: Vilin97 automation Date: Tue, 22 Sep 2026 10:14:17 -0700 Subject: [PATCH] perf(Erdos367): narrow imports and replace proof search --- LeanPool/Erdos367.lean | 6 ------ LeanPool/Erdos367/Core139.lean | 2 +- LeanPool/Erdos367/PellLimsup.lean | 5 +++-- LeanPool/Erdos367/RFullLowerBound.lean | 9 ++++++--- 4 files changed, 10 insertions(+), 12 deletions(-) diff --git a/LeanPool/Erdos367.lean b/LeanPool/Erdos367.lean index cae87ffeba..55d2471f07 100644 --- a/LeanPool/Erdos367.lean +++ b/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 diff --git a/LeanPool/Erdos367/Core139.lean b/LeanPool/Erdos367/Core139.lean index 12c7a0a3b2..8826818b66 100644 --- a/LeanPool/Erdos367/Core139.lean +++ b/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, diff --git a/LeanPool/Erdos367/PellLimsup.lean b/LeanPool/Erdos367/PellLimsup.lean index 35d4b96eda..6ce512960a 100644 --- a/LeanPool/Erdos367/PellLimsup.lean +++ b/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`. diff --git a/LeanPool/Erdos367/RFullLowerBound.lean b/LeanPool/Erdos367/RFullLowerBound.lean index 6562e0bf79..08ac9542bf 100644 --- a/LeanPool/Erdos367/RFullLowerBound.lean +++ b/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). -/