`Compfiles/Usa1995P4.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

19 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1995, Problem 4

a₀, a₁, a₂, ... is an infinite sequence of integers such that aₙ - aₘ is divisible by n - m for all (unequal) n and m. For some polynomial p(x) we have p(n) > |aₙ| for all n. Show that there is a polynomial q(x) such that q(n) = aₙ for all n.

Imports (8)

Imported by 1 file

Compfiles.lean

lemma Usa1995P4.gcd_lcm_dvd_prod_gcd gcd (lcm over s) x divides the product of the individual gcds line 38 source
Source documentation
gcd (lcm over s) x divides the product of the individual gcds.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Membership.mem, LT.lt, OfNat.ofNat, Dvd.dvd, Nat.gcd, Finset.lcm, Finset.prod
Proof uses: Finset.induction_on, EmptyCollection.emptyCollection, Eq.mpr, id, Eq, congrArg, Finset.lcm_empty, Nat.gcd_one_left, Finset.prod_empty, dvd_refl, Not, Insert.insert, GCDMonoid.lcm, Finset.lcm_insert, HMul.hMul, Finset.prod_insert, Nat.dvd_gcd, Dvd.dvd.trans, Nat.gcd_dvd_left, lcm_dvd_mul and 4 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma gcd_lcm_dvd_prod_gcd (t : ℕ → ℕ) (x : ℕ) (s : Finset ℕ) :
    (∀ i ∈ s, 0 < t i) → Nat.gcd (s.lcm t) x ∣ ∏ i ∈ s, Nat.gcd (t i) x := by
…
```
lemma Usa1995P4.prod_eq_lcm_mul_gcd_prod Exact factorization: a product of naturals equals their lcm times the product of the gcds of the successive partial lcms with the next factor line 57 source
Source documentation
Exact factorization: a product of naturals equals their lcm times the product of the gcds of the successive partial lcms with the next factor.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.prod, Finset.range, HAdd.hAdd, OfNat.ofNat, HMul.hMul, Finset.lcm, Nat.gcd
Proof uses: Nat.recAux, Eq.mpr, id, congrArg, Finset.prod_range_succ, Finset.prod_range_zero, one_mul, mul_one, Insert.insert, Finset, Finset.range_add_one, GCDMonoid.lcm, Finset.lcm_insert, EmptyCollection.emptyCollection, Finset.range_zero, Finset.lcm_empty, Nat.lcm, lcm_eq_nat_lcm, Nat.lcm_one_right, Eq.refl and 20 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma prod_eq_lcm_mul_gcd_prod (t : ℕ → ℕ) (k : ℕ) :
    ∏ i ∈ Finset.range (k + 1), t i =
      (Finset.range (k + 1)).lcm t *
        ∏ j ∈ Finset.range k, Nat.gcd ((Finset.range (j + 1)).lcm t) (t (j + 1)) := by
…
```
lemma Usa1995P4.gcd_lcm_le_pow Each step gcd is at most N ^ (j + 1), since gcd (m - i) (m - (j+1)) divides (j + 1) - i ≤ N for every i < j + 1 line 90 source
Source documentation
Each step gcd is at most N ^ (j + 1), since gcd (m - i) (m - (j+1)) divides (j + 1) - i ≤ N for every i < j + 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Membership.mem, Finset, Finset.range, LE.le, Nat.gcd, Finset.lcm, HAdd.hAdd, OfNat.ofNat, HSub.hSub, HPow.hPow
Proof uses: Iff.mp, Finset.mem_range, Dvd.dvd, Finset.prod, Usa1995P4.gcd_lcm_dvd_prod_gcd, Finset.prod_pos, Nat.gcd_pos_of_pos_left, Eq, Eq.mpr, id, congrArg, Eq.symm, Nat.dvd_sub, Nat.gcd_dvd_left, Nat.gcd_dvd_right, LE.le.trans, Nat.le_of_dvd, Trans.trans, Finset.card, Finset.prod_le_pow_card and 2 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma gcd_lcm_le_pow (m N j : ℕ) (hm : N < m) (hj : j ∈ Finset.range N) :
    Nat.gcd ((Finset.range (j + 1)).lcm (fun i => m - i)) (m - (j + 1)) ≤ N ^ (j + 1) := by
…
```
lemma Usa1995P4.prod_le_lcm_mul_pow A lower bound for the lcm of the N + 1 consecutive integers m, m - 1, ..., m - N: their product is at most N ^ (N * (N + 1)) times their lcm line 117 source
Source documentation
A lower bound for the lcm of the N + 1 consecutive integers m, m - 1, ..., m - N: their product is at most N ^ (N * (N + 1)) times their lcm.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, LE.le, Finset.prod, Finset.range, HAdd.hAdd, OfNat.ofNat, HSub.hSub, HMul.hMul, Finset.lcm, HPow.hPow
Proof uses: Eq, GT.gt, Or, Nat.eq_zero_or_pos, Eq.mpr, id, congrArg, Finset.prod_range_succ, Finset.prod_range_zero, one_mul, Insert.insert, Finset, Finset.range_add_one, GCDMonoid.lcm, Finset.lcm_insert, EmptyCollection.emptyCollection, Finset.range_zero, Finset.lcm_empty, Nat.lcm, lcm_eq_nat_lcm and 31 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma prod_le_lcm_mul_pow (N m : ℕ) (hm : N < m) :
    ∏ i ∈ Finset.range (N + 1), (m - i) ≤
      ((Finset.range (N + 1)).lcm fun i => m - i) * N ^ (N * (N + 1)) := by
…
```
lemma Usa1995P4.interpolate_exists Lagrange interpolation (over ℚ): the first N + 1 values of an integer sequence are interpolated by a rational polynomial of degree at most N line 147 source
Source documentation
Lagrange interpolation (over ℚ): the first N + 1 values of an integer sequence are interpolated by a rational polynomial of degree at most N.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Exists, Polynomial, Rat, And, LE.le, Polynomial.natDegree, Eq, Polynomial.eval
Proof uses: Set.InjOn, Finset, Finset.range, HAdd.hAdd, OfNat.ofNat, Membership.mem, Set, Iff.mp, Rat.natCast_inj, Exists.intro, LinearMap, RingHom.id, Lagrange.interpolate, And.intro, LT.lt, WithBot, Polynomial.degree, Finset.card, Lagrange.degree_interpolate_lt, dite and 17 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma interpolate_exists (a : ℕ → ℤ) (N : ℕ) :
    ∃ q : ℚ[X], q.natDegree ≤ N ∧ ∀ i : ℕ, i ≤ N → q.eval (i : ℚ) = (a i : ℚ) := by
…
```
def Usa1995P4.denomProd The product of the denominators of the coefficients of q of degree at most N line 166 source
Source documentation
The product of the denominators of the coefficients of q of degree at most N. Scaling q by this natural number clears the denominators.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Rat, Nat
Proof uses: Finset.prod, Finset.range, HAdd.hAdd, OfNat.ofNat, Rat.den, Finsupp, Polynomial.coeff
10 instances, coercions and auxiliary constants left out.
```
def denomProd (q : ℚ[X]) (N : ℕ) : ℕ := ∏ i ∈ Finset.range (N + 1), (q.coeff i).den
```
def Usa1995P4.clearCoeff The (integer) coefficients of denomProd q N • q line 169 source
Source documentation
The (integer) coefficients of denomProd q N • q.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Rat, Nat, Int
Proof uses: Rat.num, HMul.hMul, Usa1995P4.denomProd, Finsupp, Polynomial.coeff
10 instances, coercions and auxiliary constants left out.
```
def clearCoeff (q : ℚ[X]) (N : ℕ) (i : ℕ) : ℤ :=
…
```
def Usa1995P4.clearPoly The integer polynomial obtained from q : ℚ[X] by clearing denominators: its coefficients are clearCoeff q N, so it agrees with denomProd q N • q on all evaluations line 175 source
Source documentation
The integer polynomial obtained from q : ℚ[X] by clearing denominators: its coefficients are clearCoeff q N, so it agrees with denomProd q N • q on all evaluations.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Rat, Nat, Int
Proof uses: Finset.sum, Finset.range, HAdd.hAdd, OfNat.ofNat, LinearMap, RingHom.id, Polynomial.monomial, Usa1995P4.clearCoeff
14 instances, coercions and auxiliary constants left out.
```
noncomputable def clearPoly (q : ℚ[X]) (N : ℕ) : ℤ[X] :=
…
```
lemma Usa1995P4.denomProd_pos line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Rat, Nat, LT.lt, OfNat.ofNat, Usa1995P4.denomProd
Proof uses: Finset.prod_pos, Rat.den, Finsupp, Polynomial.coeff, Finset.range, HAdd.hAdd, Membership.mem, Finset, Rat.den_pos
19 instances, coercions and auxiliary constants left out.
lemma Usa1995P4.clearCoeff_spec The defining property of clearCoeff: as rationals, clearCoeff q N i equals denomProd q N * q.coeff i (for i ≤ N) line 183 source
Source documentation
The defining property of clearCoeff: as rationals, clearCoeff q N i equals denomProd q N * q.coeff i (for i ≤ N).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Rat, Nat, Membership.mem, Finset, Finset.range, HAdd.hAdd, OfNat.ofNat, Eq, Usa1995P4.clearCoeff, HMul.hMul, Usa1995P4.denomProd, Finsupp, Polynomial.coeff
Proof uses: Finset.prod, Rat.den, Dvd.dvd, Finset.dvd_prod_of_mem, cast, Eq.symm, Eq.trans, congrArg, Int, Rat.num, Eq.mpr, id, Trans.trans, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.refl and 15 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma clearCoeff_spec (q : ℚ[X]) (N : ℕ) {i : ℕ} (hi : i ∈ Finset.range (N + 1)) :
    ((clearCoeff q N i : ℤ) : ℚ) = (denomProd q N : ℚ) * q.coeff i := by
…
```
Mentions: Usa1995P4.clearCoeff, Usa1995P4.denomProd
lemma Usa1995P4.clearPoly_eval line 200 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Rat, Nat, Int, Eq, Polynomial.eval, Usa1995P4.clearPoly, Finset.sum, Finset.range, HAdd.hAdd, OfNat.ofNat, HMul.hMul, Usa1995P4.clearCoeff, HPow.hPow
Proof uses: Eq.mpr, LinearMap, RingHom.id, Polynomial.monomial, id, congrArg, Usa1995P4.clearPoly.eq_1, Polynomial.eval_finsetSum, Finset.sum_congr, rfl, Finset, Membership.mem, Polynomial.eval_monomial, Eq.refl
36 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa1995P4.clearPoly_eval_cast Evaluating the cleared polynomial gives denomProd q N times the evaluation of q (as rational numbers) line 207 source
Source documentation
Evaluating the cleared polynomial gives denomProd q N times the evaluation of q (as rational numbers).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Rat, Nat, LE.le, Polynomial.natDegree, Eq, Polynomial.eval, Int, Usa1995P4.clearPoly, HMul.hMul, Usa1995P4.denomProd
Proof uses: Eq.mpr, Finset.sum, Finset.range, HAdd.hAdd, OfNat.ofNat, Usa1995P4.clearCoeff, HPow.hPow, id, congrArg, Usa1995P4.clearPoly_eval, Int.cast_sum, Finsupp, Polynomial.coeff, Finset.sum_congr, rfl, Finset, Membership.mem, Int.cast_mul, Int.cast_pow, Int.cast_natCast and 10 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma clearPoly_eval_cast (q : ℚ[X]) {N : ℕ} (hqN : q.natDegree ≤ N) (m : ℕ) :
    (((clearPoly q N).eval (m : ℤ) : ℤ) : ℚ) = (denomProd q N : ℚ) * q.eval (m : ℚ) := by
…
```
Mentions: Usa1995P4.clearPoly, Usa1995P4.denomProd
lemma Usa1995P4.clearPoly_node At the interpolation nodes i ≤ N, the cleared polynomial takes the value denomProd q N * a i line 217 source
Source documentation
At the interpolation nodes i ≤ N, the cleared polynomial takes the value denomProd q N * a i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Polynomial, Rat, LE.le, Polynomial.natDegree, Eq, Polynomial.eval, Usa1995P4.clearPoly, HMul.hMul, Usa1995P4.denomProd
Proof uses: Usa1995P4.clearPoly_eval_cast, Eq.mpr, id, congrArg, Eq.trans, Int.cast_mul, congrFun', Int.cast_natCast, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HPow.hPow, Nat.rawCast, OfNat.ofNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add and 10 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma clearPoly_node (a : ℕ → ℤ) {q : ℚ[X]} {N : ℕ} (hqN : q.natDegree ≤ N)
    (hqval : ∀ i : ℕ, i ≤ N → q.eval (i : ℚ) = (a i : ℚ)) {i : ℕ} (hi : i ≤ N) :
    (clearPoly q N).eval (i : ℤ) = (denomProd q N : ℤ) * a i := by
…
```
Mentions: Usa1995P4.clearPoly, Usa1995P4.denomProd
lemma Usa1995P4.clearPoly_dvd The difference clearPoly q N ⬝ m - denomProd q N * a m is divisible by m - i for every i ≤ N line 229 source
Source documentation
The difference clearPoly q N ⬝ m - denomProd q N * a m is divisible by m - i for every i ≤ N.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Dvd.dvd, HSub.hSub, Polynomial, Rat, LE.le, Polynomial.natDegree, Eq, Polynomial.eval, Membership.mem, Finset, Finset.range, HAdd.hAdd, OfNat.ofNat, Usa1995P4.clearPoly, HMul.hMul, Usa1995P4.denomProd
Proof uses: Polynomial.sub_dvd_eval_sub, Usa1995P4.clearPoly_node, Iff.mp, LT.lt, Nat.succ, Nat.lt_succ_iff, Finset.mem_range, dvd_sub, dvd_mul_of_dvd_right, Eq.mpr, id, congrArg, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr and 34 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma clearPoly_dvd (a : ℕ → ℤ) (hdiv : ∀ n m : ℕ, ((n : ℤ) - (m : ℤ)) ∣ a n - a m)
    {q : ℚ[X]} {N : ℕ} (hqN : q.natDegree ≤ N)
    (hqval : ∀ i : ℕ, i ≤ N → q.eval (i : ℚ) = (a i : ℚ)) (m : ℕ) {i : ℕ}
    (hi : i ∈ Finset.range (N + 1)) :
    ((m : ℤ) - (i : ℤ)) ∣ (clearPoly q N).eval (m : ℤ) - (denomProd q N : ℤ) * a m := by
…
```
Mentions: Usa1995P4.clearPoly, Usa1995P4.denomProd
lemma Usa1995P4.sum_pow_abs_le A sum of the form ∑ c i * m ^ i with m ≥ 1 grows at most like m ^ N line 252 source
Source documentation
A sum of the form ∑ c i * m ^ i with m ≥ 1 grows at most like m ^ N.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LE.le, OfNat.ofNat, abs, Finset.sum, Finset.range, HAdd.hAdd, HMul.hMul, HPow.hPow, Int.natAbs
Proof uses: le_of_lt, Iff.mpr, LT.lt, Nat.cast_pos', lt_of_lt_of_le, inferInstance, PartialOrder, Zero, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble, Trans.trans, Eq, Finset.abs_sum_le_sum_abs, Finset.sum_congr, rfl, Finset, Membership.mem and 22 more
109 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma sum_pow_abs_le (c : ℕ → ℤ) (N : ℕ) (m : ℕ) (hm : 1 ≤ m) :
    |∑ i ∈ Finset.range (N + 1), c i * (m : ℤ) ^ i| ≤
      ((∑ i ∈ Finset.range (N + 1), (c i).natAbs : ℕ) : ℤ) * (m : ℤ) ^ N := by
…
```
lemma Usa1995P4.abs_eval_le The evaluation of an integer polynomial at m ≥ 1 is bounded by a constant times m ^ natDegree line 272 source
Source documentation
The evaluation of an integer polynomial at m ≥ 1 is bounded by a constant times m ^ natDegree.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int, Nat, LE.le, OfNat.ofNat, abs, Polynomial.eval, HMul.hMul, Finset.sum, Finset.range, HAdd.hAdd, Polynomial.natDegree, Int.natAbs, Finsupp, Polynomial.coeff, HPow.hPow
Proof uses: Eq.mpr, id, Eq, congrArg, Polynomial.eval_eq_sum_range, Usa1995P4.sum_pow_abs_le
46 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma abs_eval_le (p : ℤ[X]) (m : ℕ) (hm : 1 ≤ m) :
    |p.eval (m : ℤ)| ≤
      ((∑ i ∈ Finset.range (p.natDegree + 1), (p.coeff i).natAbs : ℕ) : ℤ) *
        (m : ℤ) ^ p.natDegree := by
…
```
lemma Usa1995P4.clearPoly_eq_of_large Key step: for large m, the cleared polynomial agrees with denomProd q N * a m line 283 source
Source documentation
Key step: for large m, the cleared polynomial agrees with denomProd q N * a m. The difference is divisible by the lcm of m, m - 1, ..., m - N, which (being larger than the product of the growth bounds) forces the difference to vanish.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Dvd.dvd, HSub.hSub, Polynomial, Rat, LE.le, Polynomial.natDegree, Eq, Polynomial.eval, OfNat.ofNat, abs, Usa1995P4.clearPoly, HMul.hMul, HPow.hPow, LT.lt, HAdd.hAdd, Usa1995P4.denomProd
Proof uses: rfl, Decidable.byContradiction, Not, Ne, Eq.mpr, id, congrArg, Iff.mpr, sub_ne_zero, Membership.mem, Finset, Finset.range, Int.natAbs, Usa1995P4.clearPoly_dvd, Nat.cast_sub, Iff.mp, Finset.mem_range, Int.ofNat_dvd_left, Eq.mp, Eq.symm and 107 more
171 instances, coercions and auxiliary constants left out.

Tactic trace: 70 steps
Open to load the checked before-and-after goal states.
```
lemma clearPoly_eq_of_large (a : ℕ → ℤ)
    (hdiv : ∀ n m : ℕ, ((n : ℤ) - (m : ℤ)) ∣ a n - a m)
    {q : ℚ[X]} {N : ℕ} (hqN : q.natDegree ≤ N)
    (hqval : ∀ i : ℕ, i ≤ N → q.eval (i : ℚ) = (a i : ℚ))
    {C C₁ : ℕ}
    (hC : ∀ m : ℕ, 1 ≤ m → |(clearPoly q N).eval (m : ℤ)| ≤ (C : ℤ) * (m : ℤ) ^ N)
    (hC₁ : ∀ m : ℕ, 1 ≤ m → |a m| ≤ (C₁ : ℤ) * (m : ℤ) ^ N)
    (m : ℕ) (hm : 2 * N < m)
    (hmB : 2 ^ (N + 1) * N ^ (N * (N + 1)) * (C + denomProd q N * C₁) < m) :
    (clearPoly q N).eval (m : ℤ) = (denomProd q N : ℤ) * a m := by
…
```
Mentions: Usa1995P4.clearPoly, Usa1995P4.denomProd
lemma Usa1995P4.clearPoly_eq_all Documented declaration: clearPoly_eq_all line 384 source
Source documentation
Tail argument: the cleared polynomial agrees with denomProd q N * a n for every n (for large arguments use clearPoly_eq_of_large; divisibility by M - n for a large M then forces equality at n).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Dvd.dvd, HSub.hSub, Polynomial, Rat, LE.le, Polynomial.natDegree, Eq, Polynomial.eval, OfNat.ofNat, abs, Usa1995P4.clearPoly, HMul.hMul, HPow.hPow, Usa1995P4.denomProd
Proof uses: rfl, Int.natAbs, Exists, And, LT.lt, HAdd.hAdd, Exists.intro, Usa1995P4.clearPoly_eq_of_large, Polynomial.sub_dvd_eval_sub, dvd_sub, dvd_mul_of_dvd_right, Neg.neg, Eq.mpr, id, congrArg, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring and 43 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma clearPoly_eq_all (a : ℕ → ℤ)
    (hdiv : ∀ n m : ℕ, ((n : ℤ) - (m : ℤ)) ∣ a n - a m)
    {q : ℚ[X]} {N : ℕ} (hqN : q.natDegree ≤ N)
    (hqval : ∀ i : ℕ, i ≤ N → q.eval (i : ℚ) = (a i : ℚ))
    {C C₁ : ℕ}
    (hC : ∀ m : ℕ, 1 ≤ m → |(clearPoly q N).eval (m : ℤ)| ≤ (C : ℤ) * (m : ℤ) ^ N)
    (hC₁ : ∀ m : ℕ, 1 ≤ m → |a m| ≤ (C₁ : ℤ) * (m : ℤ) ^ N)
    (n : ℕ) :
    (clearPoly q N).eval (n : ℤ) = (denomProd q N : ℤ) * a n := by
…
```
Mentions: Usa1995P4.clearPoly, Usa1995P4.denomProd
problem Usa1995P4.usa1995_p4 line 426 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Dvd.dvd, HSub.hSub, Exists, Polynomial, GT.gt, Polynomial.eval, abs, Rat, Eq
Proof uses: And, LE.le, Polynomial.natDegree, Usa1995P4.interpolate_exists, OfNat.ofNat, Usa1995P4.clearPoly, HMul.hMul, HPow.hPow, Exists.intro, Finset.sum, Finset.range, HAdd.hAdd, Int.natAbs, Usa1995P4.clearCoeff, Eq.mpr, id, congrArg, Usa1995P4.clearPoly_eval, Usa1995P4.sum_pow_abs_le, Finsupp and 38 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.