`Compfiles/Imo2023P3.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

43 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2023, Problem 3

For each integer k ≥ 2, determine all infinite sequences of positive integers a₁, a₂, ... for which there exists a polynomial P of the form

P(x) = xᵏ + cₖ₋₁xᵏ⁻¹ + ... + c₁x + c₀,

where c₀, c₁, ..., cₖ₋₁ are non-negative integers, such that

P(aₙ) = aₙ₊₁aₙ₊₂⋯aₙ₊ₖ

for every integer n ≥ 1.

Imports (7)

Imported by 1 file

Compfiles.lean

determine Imo2023P3.SolutionSet line 40 source
no axioms what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Set, PNat
Proof uses: Set.ofPred, Exists, Eq, Subtype.mk, LT.lt, HAdd.hAdd, Nat.succ_pos, HMul.hMul
10 instances, coercions and auxiliary constants left out.
def Imo2023P3.apPoly The polynomial P(x) = ∏_{i=1}^{k} (x + i·d) attached to an arithmetic progression with common difference d line 47 source
Source documentation
The polynomial P(x) = ∏_{i=1}^{k} (x + i·d) attached to an arithmetic progression with common difference d.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Polynomial, Int
Proof uses: Finset.prod, Finset.range, HAdd.hAdd, Polynomial.X, RingHom, Polynomial.C, HMul.hMul, OfNat.ofNat
17 instances, coercions and auxiliary constants left out.
```
noncomputable def apPoly (k d : ℕ) : Polynomial ℤ :=
…
```
lemma Imo2023P3.apPoly_monic line 50 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Polynomial.Monic, Int, Imo2023P3.apPoly
Proof uses: Polynomial.monic_prod_of_monic, Finset.range, HAdd.hAdd, Polynomial, Polynomial.X, RingHom, Polynomial.C, HMul.hMul, OfNat.ofNat, Membership.mem, Finset, Polynomial.monic_X_add_C
18 instances, coercions and auxiliary constants left out.
lemma Imo2023P3.apPoly_natDegree line 53 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Polynomial.natDegree, Int, Imo2023P3.apPoly
Proof uses: Eq.mpr, Finset.prod, Polynomial, Finset.range, HAdd.hAdd, Polynomial.X, RingHom, Polynomial.C, HMul.hMul, OfNat.ofNat, id, congrArg, Imo2023P3.apPoly.eq_1, Finset.sum, Polynomial.natDegree_prod_of_monic, Membership.mem, Finset, Polynomial.monic_X_add_C, of_eq_true, Eq.trans and 11 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2023P3.apPoly_degree line 57 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, WithBot, Polynomial.degree, Int, Imo2023P3.apPoly
Proof uses: Eq.mpr, Polynomial.natDegree, id, congrArg, Polynomial.degree_eq_natDegree, Polynomial.Monic.ne_zero, Imo2023P3.apPoly_monic, Imo2023P3.apPoly_natDegree, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2023P3.coeff_X_add_C_nonneg line 60 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, LE.le, OfNat.ofNat, Nat, Finsupp, Polynomial.coeff, HAdd.hAdd, Polynomial, Polynomial.X, RingHom, Polynomial.C
Proof uses: Eq.mpr, id, Eq, congrArg, Polynomial.coeff_add, ite, Polynomial.coeff_X, Polynomial.coeff_C, dite, congrFun', ite_eq_left, False.elim, Eq.mp, False, Eq.trans, Not, ite_eq_right, of_eq_true, True, add_zero and 2 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2023P3.pnat_prod_coe Coercion of a ℕ+-valued product to ℤ line 66 source
Source documentation
Coercion of a ℕ+-valued product to ℤ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, PNat, Eq, Int, Finset.prod
Proof uses: Eq.mpr, id, Eq.trans, Nat, congrArg, Finset.PNat.coe_prod, Eq.symm, Eq.refl
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma pnat_prod_coe {ι : Type*} (s : Finset ι) (f : ι → ℕ+) :
    ((∏ i ∈ s, f i : ℕ+) : ℤ) = ∏ i ∈ s, ((f i : ℕ+) : ℤ) := by
…
```
Mentions: f
lemma Imo2023P3.le_of_pow_le For naturals, x ^ k ≤ y ^ k implies x ≤ y line 71 source
Source documentation
For naturals, x ^ k ≤ y ^ k implies x ≤ y.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, HPow.hPow
Proof uses: dite, Not, lt_of_not_ge, absurd, not_le_of_gt, pow_lt_pow_left₀, Nat.zero_le, Iff.mp, Ne, Nat.pos_iff_ne_zero
25 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma le_of_pow_le {x y k : ℕ} (hk : 0 < k) (h : x ^ k ≤ y ^ k) : x ≤ y := by
…
```
Mentions: h
lemma Imo2023P3.pow_ge_add_mul First two terms of the binomial expansion bound the power below line 78 source
Source documentation
First two terms of the binomial expansion bound the power below.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HAdd.hAdd, HPow.hPow, OfNat.ofNat, HMul.hMul
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, zero_add, pow_one, congrFun', pow_zero, mul_one, one_mul, Eq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr and 39 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma pow_ge_add_mul (x y n : ℕ) :
    x ^ (n + 1) + (n + 1) * x ^ n * y ≤ (x + y) ^ (n + 1) := by
…
```
lemma Imo2023P3.eval_eq Expansion of P.eval for a monic P of degree k line 94 source
Source documentation
Expansion of P.eval for a monic P of degree k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Polynomial, Int, Polynomial.Monic, Eq, WithBot, Polynomial.degree, Polynomial.eval, HAdd.hAdd, HPow.hPow, Finset.sum, Finset.range, HMul.hMul, Finsupp, Polynomial.coeff
Proof uses: Polynomial.natDegree, Polynomial.natDegree_eq_of_degree_eq_some, Eq.mpr, id, Eq.rec, Eq.refl, Eq.trans, congrArg, Polynomial.eval_eq_sum_range, Finset.sum_range_succ, Eq.symm, Polynomial.Monic.leadingCoeff, one_mul, add_comm
57 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma eval_eq {k : ℕ} (_hk : 2 ≤ k) {P : Polynomial ℤ} (hmon : P.Monic)
    (hdeg : P.degree = k) (x : ℤ) :
    P.eval x = x ^ k + ∑ j ∈ Finset.range k, P.coeff j * x ^ j := by
…
```
Mentions: P
lemma Imo2023P3.eval_pos P.eval is positive at positive integers line 106 source
Source documentation
P.eval is positive at positive integers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Polynomial, Int, Polynomial.Monic, Eq, WithBot, Polynomial.degree, Finsupp, Polynomial.coeff, LT.lt, Polynomial.eval
Proof uses: Eq.mpr, HAdd.hAdd, HPow.hPow, Finset.sum, Finset.range, HMul.hMul, id, congrArg, Imo2023P3.eval_eq, add_pos_of_pos_of_nonneg, pow_pos, Finset.sum_nonneg, Membership.mem, Finset, mul_nonneg, Nat.le_of_lt, Iff.mp, Finset.mem_range, pow_nonneg, LT.lt.le
53 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma eval_pos {k : ℕ} (_hk : 2 ≤ k) {P : Polynomial ℤ} (hmon : P.Monic)
    (hdeg : P.degree = k) (hcoef : ∀ n, n ≤ k → 0 ≤ P.coeff n)
    {x : ℤ} (hx : 0 < x) :
    0 < P.eval x := by
…
```
Mentions: P
lemma Imo2023P3.eval_strictMono P.eval is strictly increasing on positive integers line 117 source
Source documentation
P.eval is strictly increasing on positive integers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Polynomial, Int, Polynomial.Monic, Eq, WithBot, Polynomial.degree, Finsupp, Polynomial.coeff, LT.lt, Polynomial.eval
Proof uses: Eq.mpr, HAdd.hAdd, HPow.hPow, Finset.sum, Finset.range, HMul.hMul, id, congrArg, Imo2023P3.eval_eq, add_lt_add_of_lt_of_le, pow_lt_pow_left₀, LT.lt.le, Finset.sum_le_sum, Membership.mem, Finset, mul_le_mul_of_nonneg_left, pow_le_pow_left₀, Nat.le_of_lt, Iff.mp, Finset.mem_range
66 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma eval_strictMono {k : ℕ} (hk : 2 ≤ k) {P : Polynomial ℤ} (hmon : P.Monic)
    (hdeg : P.degree = k) (hcoef : ∀ n, n ≤ k → 0 ≤ P.coeff n)
    {x y : ℤ} (hx : 0 < x) (hxy : x < y) :
    P.eval x < P.eval y := by
…
```
Mentions: P
lemma Imo2023P3.key_recurrence The key recurrence obtained by dividing two consecutive instances of the functional equation: a_{n+k+1}·P(a_n) = a_{n+1}·P(a_{n+1}) line 131 source
Source documentation
The key recurrence obtained by dividing two consecutive instances of the functional equation: a_{n+k+1}·P(a_n) = a_{n+1}·P(a_{n+1}).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Polynomial, Int, Eq, Polynomial.eval, Finset.prod, Finset.range, HAdd.hAdd, OfNat.ofNat, HMul.hMul
Proof uses: Eq.mpr, id, congrArg, rfl, Finset.prod_congr, Finset, Membership.mem, Nat.add_right_comm, Nat.add_assoc, Eq.refl, Finset.prod_range_succ', mul_comm, Finset.prod_range_succ
30 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma key_recurrence {k : ℕ} {P : Polynomial ℤ} {A : ℕ → ℕ}
    (hA : ∀ m : ℕ, P.eval (A m : ℤ) = ∏ i ∈ Finset.range k, (A (m + 1 + i) : ℤ))
    (m : ℕ) :
    (A (m + 1 + k) : ℤ) * P.eval (A m : ℤ) = (A (m + 1) : ℤ) * P.eval (A (m + 1) : ℤ) := by
…
```
Mentions: P
def Imo2023P3.seqA The sequence reindexed by ℕ: seqA a m = a_{m+1} line 152 source
Source documentation
The sequence reindexed by ℕ: seqA a m = a_{m+1}.

no axioms what this means
Statement uses: PNat, Nat
Proof uses: Subtype.mk, LT.lt, OfNat.ofNat, HAdd.hAdd, Nat.succ_pos
5 instances, coercions and auxiliary constants left out.
```
def seqA (a : ℕ+ → ℕ+) (m : ℕ) : ℕ := (a ⟨m + 1, Nat.succ_pos m⟩).val
```
lemma Imo2023P3.seqA_pos line 154 source
no axioms what this means
Statement uses: PNat, Nat, LT.lt, OfNat.ofNat, Imo2023P3.seqA
Proof uses: PNat.pos, Subtype.mk, HAdd.hAdd, Nat.succ_pos
6 instances, coercions and auxiliary constants left out.
lemma Imo2023P3.hA_of The functional equation restated for the ℕ-indexed sequence line 157 source
Source documentation
The functional equation restated for the ℕ-indexed sequence.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Polynomial, Int, PNat, Eq, Polynomial.eval, Finset.prod, Finset.range, Subtype.mk, LT.lt, OfNat.ofNat, HAdd.hAdd, Nat.succ_pos, Imo2023P3.seqA
Proof uses: Eq.trans, Eq.mp, congrArg, Imo2023P3.pnat_prod_coe, Finset.prod_congr, rfl, Finset, Membership.mem
22 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma hA_of {k : ℕ} {P : Polynomial ℤ} {a : ℕ+ → ℕ+}
    (hP : ∀ n : ℕ+, P.eval ((a n) : ℤ) =
      ∏ i ∈ Finset.range k, a ⟨n + i + 1, Nat.succ_pos _⟩) (m : ℕ) :
    P.eval (seqA a m : ℤ) = ∏ i ∈ Finset.range k, (seqA a (m + 1 + i) : ℤ) := by
…
```
Mentions: P, Imo2023P3.seqA
def Imo2023P3.Csum Csum P k = Σ_{j<k} P.coeff j, the total mass of the lower coefficients line 166 source
Source documentation
Csum P k = Σ_{j<k} P.coeff j, the total mass of the lower coefficients.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int, Nat
Proof uses: Finset.sum, Finset.range, Finsupp, Polynomial.coeff
7 instances, coercions and auxiliary constants left out.
```
def Csum (P : Polynomial ℤ) (k : ℕ) : ℤ := ∑ j ∈ Finset.range k, P.coeff j
```
Mentions: P
lemma Imo2023P3.Csum_nonneg line 168 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Polynomial, Int, LE.le, OfNat.ofNat, Finsupp, Polynomial.coeff, Imo2023P3.Csum
Proof uses: Finset.sum_nonneg, Finset.range, Membership.mem, Finset, Nat.le_of_lt, Iff.mp, LT.lt, Finset.mem_range
22 instances, coercions and auxiliary constants left out.
lemma Imo2023P3.eval_lower Lower bound: x ^ k ≤ P.eval x for x ≥ 1 line 173 source
Source documentation
Lower bound: x ^ k ≤ P.eval x for x ≥ 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Polynomial, Int, Polynomial.Monic, Eq, WithBot, Polynomial.degree, Finsupp, Polynomial.coeff, HPow.hPow, Polynomial.eval
Proof uses: Eq.mpr, HAdd.hAdd, Finset.sum, Finset.range, HMul.hMul, id, congrArg, Imo2023P3.eval_eq, le_add_of_nonneg_right, Finset.sum_nonneg, Membership.mem, Finset, mul_nonneg, Nat.le_of_lt, Iff.mp, LT.lt, Finset.mem_range, pow_nonneg
51 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma eval_lower {k : ℕ} (hk : 2 ≤ k) {P : Polynomial ℤ} (hmon : P.Monic)
    (hdeg : P.degree = k) (hcoef : ∀ n, n ≤ k → 0 ≤ P.coeff n)
    {x : ℤ} (hx : 1 ≤ x) : x ^ k ≤ P.eval x := by
…
```
Mentions: P
lemma Imo2023P3.eval_upper Upper bound: P.eval x ≤ x ^ k + C·x ^ (k-1) for x ≥ 1 line 183 source
Source documentation
Upper bound: P.eval x ≤ x ^ k + C·x ^ (k-1) for x ≥ 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Polynomial, Int, Polynomial.Monic, Eq, WithBot, Polynomial.degree, Finsupp, Polynomial.coeff, Polynomial.eval, HAdd.hAdd, HPow.hPow, HMul.hMul, Imo2023P3.Csum, HSub.hSub
Proof uses: Eq.mpr, Finset.sum, Finset.range, id, congrArg, Imo2023P3.eval_eq, add_le_add_right, Finset.sum_mul, Finset.sum_le_sum, Membership.mem, Finset, Nat.le_pred_of_lt, Nat.sub, Iff.mp, LT.lt, Finset.mem_range, mul_le_mul_of_nonneg_left, pow_le_pow_right₀, Nat.le_of_lt
64 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma eval_upper {k : ℕ} (hk : 2 ≤ k) {P : Polynomial ℤ} (hmon : P.Monic)
    (hdeg : P.degree = k) (hcoef : ∀ n, n ≤ k → 0 ≤ P.coeff n)
    {x : ℤ} (hx : 1 ≤ x) : P.eval x ≤ x ^ k + Csum P k * x ^ (k - 1) := by
…
```
Mentions: P, Imo2023P3.Csum
lemma Imo2023P3.chain_le_nat Chaining one-step inequalities over an interval line 197 source
Source documentation
Chaining one-step inequalities over an interval.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, LT.lt, HAdd.hAdd, OfNat.ofNat
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrArg, add_zero, LE.le.trans
18 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma chain_le_nat {B : ℕ → ℕ} {a b : ℕ} (h : ∀ j, a ≤ j → j < b → B j ≤ B (j + 1)) :
    ∀ {t}, a + t ≤ b → B a ≤ B (a + t) := by
…
```
Mentions: h
lemma Imo2023P3.seq_monotone The sequence is non-decreasing line 209 source
Source documentation
The sequence is non-decreasing. Proof: among all descent indices n (with A (n+1) < A n), take one with A (n+1) minimal; the key recurrence forces A (n+k+1) < A (n+1), and chaining up to n+k+1 contradicts minimality.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Polynomial, Int, Polynomial.Monic, Eq, WithBot, Polynomial.degree, Finsupp, Polynomial.coeff, Polynomial.eval, Finset.prod, Finset.range, HAdd.hAdd, LT.lt, Monotone
Proof uses: monotone_nat_of_le_succ, Classical.byContradiction, Not, Set, Set.ofPred, Exists, And, rfl, Set.Nonempty, Eq.mp, Eq.trans, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, Exists.intro, Membership.mem, And.intro, InfSet.sInf, False, Nat.sInf_mem and 32 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 67 steps
Open to load the checked before-and-after goal states.
```
lemma seq_monotone {k : ℕ} (hk : 2 ≤ k) {P : Polynomial ℤ} (hmon : P.Monic)
    (hdeg : P.degree = k) (hcoef : ∀ n, n ≤ k → 0 ≤ P.coeff n)
    {A : ℕ → ℕ} (hA : ∀ m, P.eval (A m : ℤ) = ∏ i ∈ Finset.range k, (A (m + 1 + i) : ℤ))
    (hpos : ∀ m, 0 < A m) : Monotone A := by
…
```
Mentions: P
lemma Imo2023P3.diff_le Bounded consecutive differences: A (m+1) ≤ A m + C where C = (Csum P k).toNat line 278 source
Source documentation
Bounded consecutive differences: A (m+1) ≤ A m + C where C = (Csum P k).toNat.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Polynomial, Int, Polynomial.Monic, Eq, WithBot, Polynomial.degree, Finsupp, Polynomial.coeff, Polynomial.eval, Finset.prod, Finset.range, HAdd.hAdd, LT.lt, Monotone, Int.toNat, Imo2023P3.Csum
Proof uses: Eq.mpr, id, congrArg, rfl, Int.toNat_of_nonneg, Imo2023P3.Csum_nonneg, HPow.hPow, Finset.card, Finset.prod_const, Finset.card_range, Eq.refl, Finset.prod_le_prod₀, Membership.mem, Finset, Nat.zero_le, HMul.hMul, HSub.hSub, Imo2023P3.pow_ge_add_mul, Trans.trans, Nat.add_le_add_left and 84 more
142 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
```
lemma diff_le {k : ℕ} (hk : 2 ≤ k) {P : Polynomial ℤ} (hmon : P.Monic)
    (hdeg : P.degree = k) (hcoef : ∀ n, n ≤ k → 0 ≤ P.coeff n)
    {A : ℕ → ℕ} (hA : ∀ m, P.eval (A m : ℤ) = ∏ i ∈ Finset.range k, (A (m + 1 + i) : ℤ))
    (hpos : ∀ m, 0 < A m) (hmono : Monotone A) (m : ℕ) :
    A (m + 1) ≤ A m + (Csum P k).toNat := by
…
```
Mentions: P, Imo2023P3.Csum
lemma Imo2023P3.shift_bounds The shifts A (m+i) - A m lie in [0, i·C] line 317 source
Source documentation
The shifts A (m+i) - A m lie in [0, i·C].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Polynomial, Int, Polynomial.Monic, Eq, WithBot, Polynomial.degree, Finsupp, Polynomial.coeff, Polynomial.eval, Finset.prod, Finset.range, HAdd.hAdd, LT.lt, Monotone, And, HSub.hSub, HMul.hMul and 1 more
Proof uses: Int.toNat, rfl, Int.toNat_of_nonneg, Imo2023P3.Csum_nonneg, Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, add_zero, MulZeroClass.zero_mul, Trans.trans, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, Eq.mpr, id, Eq.symm and 61 more
114 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma shift_bounds {k : ℕ} (hk : 2 ≤ k) {P : Polynomial ℤ} (hmon : P.Monic)
    (hdeg : P.degree = k) (hcoef : ∀ n, n ≤ k → 0 ≤ P.coeff n)
    {A : ℕ → ℕ} (hA : ∀ m, P.eval (A m : ℤ) = ∏ i ∈ Finset.range k, (A (m + 1 + i) : ℤ))
    (hpos : ∀ m, 0 < A m) (hmono : Monotone A) (m i : ℕ) :
    0 ≤ (A (m + i) : ℤ) - A m ∧ (A (m + i) : ℤ) - A m ≤ i * Csum P k := by
…
```
Mentions: P, Imo2023P3.Csum
lemma Imo2023P3.monic_prod_linear A product of linear factors is monic line 342 source
Source documentation
A product of linear factors is monic.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Finset, Polynomial.Monic, Finset.prod, Polynomial, HAdd.hAdd, Polynomial.X, RingHom, Polynomial.C
Proof uses: Polynomial.monic_prod_of_monic, Membership.mem, Polynomial.monic_X_add_C
21 instances, coercions and auxiliary constants left out.
```
lemma monic_prod_linear {σ : ℕ → ℤ} (s : Finset ℕ) :
    (∏ i ∈ s, (X + C (σ i))).Monic :=
…
```
lemma Imo2023P3.natDegree_prod_linear line 346 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Finset, Eq, Polynomial.natDegree, Finset.prod, Polynomial, HAdd.hAdd, Polynomial.X, RingHom, Polynomial.C, Finset.card
Proof uses: Eq.mpr, Finset.sum, id, congrArg, Polynomial.natDegree_prod_of_monic, Membership.mem, Polynomial.monic_X_add_C, of_eq_true, Eq.trans, True, congrFun', HSMul.hSMul, OfNat.ofNat, Finset.sum_congr, Eq.refl, Polynomial.natDegree_X_add_C, Finset.sum_const, mul_one, eq_self
34 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2023P3.degree_prod_linear line 351 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Finset, Eq, WithBot, Polynomial.degree, Finset.prod, Polynomial, HAdd.hAdd, Polynomial.X, RingHom, Polynomial.C, Finset.card
Proof uses: Eq.mpr, Polynomial.natDegree, id, congrArg, Polynomial.degree_eq_natDegree, Polynomial.Monic.ne_zero, Imo2023P3.monic_prod_linear, Imo2023P3.natDegree_prod_linear, Eq.refl
27 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2023P3.coeff_prod_linear_bound Coefficients of a product of linear factors X + C σᵢ are bounded by (1 + S) ^ (number of factors) when every |σᵢ| ≤ S line 357 source
Source documentation
Coefficients of a product of linear factors X + C σᵢ are bounded by (1 + S) ^ (number of factors) when every |σᵢ| ≤ S.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, LE.le, OfNat.ofNat, Nat, Finset, Membership.mem, abs, Finsupp, Polynomial.coeff, Finset.prod, Polynomial, HAdd.hAdd, Polynomial.X, RingHom, Polynomial.C, HPow.hPow, Finset.card
Proof uses: Finset.induction, EmptyCollection.emptyCollection, Eq.mpr, id, Eq, congrArg, Finset.prod_empty, Finset.card_empty, pow_zero, ite, Polynomial.coeff_one, dite, congrFun', ite_eq_left, of_eq_true, Eq.trans, True, abs_one, Not, ite_eq_right and 104 more
149 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma coeff_prod_linear_bound {S : ℤ} (hS : 0 ≤ S) (σ : ℕ → ℤ) :
    ∀ (s : Finset ℕ), (∀ i ∈ s, |σ i| ≤ S) →
      ∀ j : ℕ, |(∏ i ∈ s, (X + C (σ i))).coeff j| ≤ (1 + S) ^ s.card := by
…
```
Mentions: S
def Imo2023P3.Fpoly Fpoly P A k m := ∏_{i=1}^{k} (X + C (A (m+i) - A m)) - P; it vanishes at A m line 391 source
Source documentation
Fpoly P A k m := ∏_{i=1}^{k} (X + C (A (m+i) - A m)) - P; it vanishes at A m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int, Nat
Proof uses: HSub.hSub, Finset.prod, Finset.range, HAdd.hAdd, Polynomial.X, RingHom, Polynomial.C, OfNat.ofNat
19 instances, coercions and auxiliary constants left out.
```
noncomputable def Fpoly (P : Polynomial ℤ) (A : ℕ → ℕ) (k m : ℕ) : Polynomial ℤ :=
…
```
Mentions: P
lemma Imo2023P3.Fpoly_eval line 394 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Polynomial, Int, Eq, Polynomial.eval, Finset.prod, Finset.range, HAdd.hAdd, OfNat.ofNat, Imo2023P3.Fpoly
Proof uses: Eq.mpr, HSub.hSub, Polynomial.X, RingHom, Polynomial.C, id, congrArg, Imo2023P3.Fpoly.eq_1, Polynomial.eval_sub, Polynomial.eval_prod, Finset.prod_congr, rfl, Finset, Membership.mem, Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow and 29 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2023P3.Fpoly_degree_lt line 406 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Polynomial, Int, Polynomial.Monic, Eq, WithBot, Polynomial.degree, LT.lt, Imo2023P3.Fpoly
Proof uses: Finset.prod, Finset.range, HAdd.hAdd, Polynomial.X, RingHom, Polynomial.C, HSub.hSub, Eq.mpr, Finset.card, id, congrArg, Imo2023P3.degree_prod_linear, Finset.card_range, Eq.refl, Ne, Polynomial.Monic.ne_zero, Imo2023P3.monic_prod_linear, Polynomial.leadingCoeff, Polynomial.Monic.leadingCoeff, Polynomial.degree_sub_lt_left and 1 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2023P3.Fpoly_coeff_bound line 421 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Polynomial, Int, Polynomial.Monic, Eq, WithBot, Polynomial.degree, Finsupp, Polynomial.coeff, Polynomial.eval, Finset.prod, Finset.range, HAdd.hAdd, LT.lt, Monotone, abs, Imo2023P3.Fpoly, HPow.hPow and 2 more
Proof uses: Imo2023P3.Csum_nonneg, dite, Polynomial.X, RingHom, Polynomial.C, HSub.hSub, Finset.card, Imo2023P3.coeff_prod_linear_bound, mul_nonneg, le_of_lt, Iff.mpr, 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 and 36 more
139 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma Imo2023P3.root_bound An integer root x ≥ 1 of a nonzero integer polynomial is bounded by natDegree × (coefficient bound) line 462 source
Source documentation
An integer root x ≥ 1 of a nonzero integer polynomial is bounded by natDegree × (coefficient bound).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int, Ne, OfNat.ofNat, Nat, LE.le, abs, Finsupp, Polynomial.coeff, Eq, Polynomial.eval, HMul.hMul, Polynomial.natDegree
Proof uses: le_trans, abs_nonneg, dite, Finset.sum, Finset.range, HAdd.hAdd, HPow.hPow, Polynomial.eval_eq_sum_range, Iff.mpr, Polynomial.leadingCoeff, Polynomial.leadingCoeff_ne_zero, Eq.mp, congrArg, absurd, Eq.symm, Eq.trans, pow_zero, mul_one, Finset.sum_range_one, Not and 97 more
134 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
```
lemma root_bound {F : Polynomial ℤ} {B : ℤ} (hF : F ≠ 0) (hB : ∀ j, |F.coeff j| ≤ B)
    {x : ℤ} (hx : 1 ≤ x) (hFx : F.eval x = 0) : x ≤ F.natDegree * B := by
…
```
lemma Imo2023P3.eval_sum_eq Once A m exceeds the root bound, F_m vanishes, and comparing the X ^ (k-1)-coefficients yields the key relation Σ_{i<k} A (m+1+i) = k·A m + c_{k-1} line 527 source
Source documentation
Once A m exceeds the root bound, F_m vanishes, and comparing the X ^ (k-1)-coefficients yields the key relation Σ_{i<k} A (m+1+i) = k·A m + c_{k-1}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Polynomial, Int, Polynomial.Monic, Eq, WithBot, Polynomial.degree, Finsupp, Polynomial.coeff, Polynomial.eval, Finset.prod, Finset.range, HAdd.hAdd, LT.lt, Monotone, GE.ge, HMul.hMul, HPow.hPow and 3 more
Proof uses: Imo2023P3.Fpoly, Decidable.byContradiction, Not, Polynomial.natDegree, Imo2023P3.root_bound, Imo2023P3.Fpoly_coeff_bound, cast, Eq.symm, Eq.trans, congrFun', congrArg, Nat.cast_one, Imo2023P3.Fpoly_eval, Eq.mpr, id, propext, Polynomial.natDegree_lt_iff_degree_lt, Imo2023P3.Fpoly_degree_lt, Imo2023P3.Csum_nonneg, le_of_lt and 112 more
165 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
lemma eval_sum_eq {k : ℕ} (hk : 2 ≤ k) {P : Polynomial ℤ} (hmon : P.Monic)
    (hdeg : P.degree = k) (hcoef : ∀ n, n ≤ k → 0 ≤ P.coeff n)
    {A : ℕ → ℕ} (hA : ∀ m, P.eval (A m : ℤ) = ∏ i ∈ Finset.range k, (A (m + 1 + i) : ℤ))
    (hpos : ∀ m, 0 < A m) (hmono : Monotone A)
    {N₀ : ℕ} (hN₀ : ∀ m, m ≥ N₀ → (k * ((1 + k * Csum P k) ^ k + Csum P k) : ℤ) < A m)
    (m : ℕ) (hm : m ≥ N₀) :
    ∑ i ∈ Finset.range k, (A (m + 1 + i) : ℤ) = k * (A m : ℤ) + P.coeff (k - 1) := by
…
```
Mentions: P, Imo2023P3.Csum
def Imo2023P3.Dif The consecutive difference Dif A j = A (j+1) - A j as an integer line 573 source
Source documentation
The consecutive difference Dif A j = A (j+1) - A j as an integer.

no axioms what this means
Statement uses: Nat, Int
Proof uses: HSub.hSub, HAdd.hAdd, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
def Dif (A : ℕ → ℕ) (j : ℕ) : ℤ := (A (j + 1) : ℤ) - A j
```
lemma Imo2023P3.diff_eventually_const Documented declaration: diff_eventually_const line 578 source
Source documentation
Once A m exceeds the root bound, the difference Dif A j is eventually constant: the sum relation Σ_{l<k} Dif A (j+1+l) = k · Dif A j forces the maximal difference to propagate.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Polynomial, Int, Polynomial.Monic, Eq, WithBot, Polynomial.degree, Finsupp, Polynomial.coeff, Polynomial.eval, Finset.prod, Finset.range, HAdd.hAdd, LT.lt, Monotone, GE.ge, HMul.hMul, HPow.hPow and 3 more
Proof uses: Finset.sum, HSub.hSub, Imo2023P3.eval_sum_eq, cast, Eq.symm, Eq.mpr, id, congrArg, Imo2023P3.Dif.eq_1, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, Nat.rawCast and 92 more
143 instances, coercions and auxiliary constants left out.

Tactic trace: 68 steps
Open to load the checked before-and-after goal states.
```
lemma diff_eventually_const {k : ℕ} (hk : 2 ≤ k) {P : Polynomial ℤ} (hmon : P.Monic)
    (hdeg : P.degree = k) (hcoef : ∀ n, n ≤ k → 0 ≤ P.coeff n)
    {A : ℕ → ℕ} (hA : ∀ m, P.eval (A m : ℤ) = ∏ i ∈ Finset.range k, (A (m + 1 + i) : ℤ))
    (hpos : ∀ m, 0 < A m) (hmono : Monotone A)
    {N₀ : ℕ} (hN₀ : ∀ m, m ≥ N₀ → (k * ((1 + k * Csum P k) ^ k + Csum P k) : ℤ) < A m) :
    ∃ m c, (∀ j ≥ m, Dif A j = c) := by
…
```
Mentions: P, Imo2023P3.Csum, Imo2023P3.Dif
lemma Imo2023P3.apPoly_coeff_nonneg_aux line 648 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, LE.le, Int, OfNat.ofNat, Finsupp, Polynomial.coeff, Finset.prod, Polynomial, HAdd.hAdd, Polynomial.X, RingHom, Polynomial.C, HMul.hMul
Proof uses: Finset.induction, Eq.mpr, EmptyCollection.emptyCollection, id, Eq, congrArg, Finset.prod_empty, ite, Polynomial.coeff_one, dite, ite_eq_left, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Not, ite_eq_right, Membership.mem, Insert.insert and 12 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2023P3.apPoly_coeff_nonneg line 658 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Int, OfNat.ofNat, Finsupp, Polynomial.coeff, Imo2023P3.apPoly
Proof uses: Imo2023P3.apPoly_coeff_nonneg_aux, Finset.range
7 instances, coercions and auxiliary constants left out.
lemma Imo2023P3.apPoly_eval line 661 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Eq, Polynomial.eval, Imo2023P3.apPoly, Finset.prod, Finset.range, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: Eq.mpr, Polynomial, Polynomial.X, RingHom, Polynomial.C, id, congrArg, Imo2023P3.apPoly.eq_1, Polynomial.eval_prod, Finset.prod_congr, rfl, Finset, Membership.mem, Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C, Eq.refl
34 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2023P3.backward_bounded The bounded case: a bounded monotone sequence of naturals stabilizes, and the functional equation forces it to be constant line 668 source
Source documentation
The bounded case: a bounded monotone sequence of naturals stabilizes, and the functional equation forces it to be constant.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Polynomial, Int, Polynomial.Monic, Eq, WithBot, Polynomial.degree, Finsupp, Polynomial.coeff, Polynomial.eval, Finset.prod, Finset.range, HAdd.hAdd, LT.lt, Monotone, Exists, HMul.hMul
Proof uses: GE.ge, converges_of_monotone_of_bounded, Eq.mp, congrArg, le_refl, HPow.hPow, Eq.mpr, id, Finset.prod_congr, rfl, Finset, Membership.mem, Eq.refl, Finset.card, Finset.prod_const, Finset.card_range, Finset.sum, Imo2023P3.eval_eq, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro and 103 more
154 instances, coercions and auxiliary constants left out.

Tactic trace: 104 steps
Open to load the checked before-and-after goal states.
```
lemma backward_bounded {k : ℕ} (hk : 2 ≤ k) {P : Polynomial ℤ} (hmon : P.Monic)
    (hdeg : P.degree = k) (hcoef : ∀ n, n ≤ k → 0 ≤ P.coeff n)
    {A : ℕ → ℕ} (hA : ∀ m, P.eval (A m : ℤ) = ∏ i ∈ Finset.range k, (A (m + 1 + i) : ℤ))
    (hpos : ∀ m, 0 < A m) (hmono : Monotone A)
    {B : ℕ} (hB : ∀ m, A m ≤ B) :
    ∃ a₀ d : ℕ, ∀ m, A m = a₀ + d * m := by
…
```
Mentions: P
lemma Imo2023P3.backward_unbounded The unbounded case: once the sequence exceeds the root bound, it is an arithmetic progression line 755 source
Source documentation
The unbounded case: once the sequence exceeds the root bound, it is an arithmetic progression.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Polynomial, Int, Polynomial.Monic, Eq, WithBot, Polynomial.degree, Finsupp, Polynomial.coeff, Polynomial.eval, Finset.prod, Finset.range, HAdd.hAdd, LT.lt, Monotone, GE.ge, HMul.hMul, HPow.hPow and 2 more
Proof uses: Imo2023P3.Dif, Imo2023P3.diff_eventually_const, Max.max, rfl, le_refl, cast, Eq.symm, Eq.mpr, HSub.hSub, id, congrArg, Imo2023P3.Dif.eq_1, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance and 137 more
187 instances, coercions and auxiliary constants left out.

Tactic trace: 195 steps
Open to load the checked before-and-after goal states.
```
lemma backward_unbounded {k : ℕ} (hk : 2 ≤ k) {P : Polynomial ℤ} (hmon : P.Monic)
    (hdeg : P.degree = k) (hcoef : ∀ n, n ≤ k → 0 ≤ P.coeff n)
    {A : ℕ → ℕ} (hA : ∀ m, P.eval (A m : ℤ) = ∏ i ∈ Finset.range k, (A (m + 1 + i) : ℤ))
    (hpos : ∀ m, 0 < A m) (hmono : Monotone A)
    {N₀ : ℕ} (hN₀ : ∀ m, m ≥ N₀ → (k * ((1 + k * Csum P k) ^ k + Csum P k) : ℤ) < A m) :
    ∃ a₀ d : ℕ, ∀ m, A m = a₀ + d * m := by
…
```
Mentions: P, Imo2023P3.Csum
lemma Imo2023P3.backward_main The backward direction: any sequence satisfying the functional equation is an arithmetic progression line 934 source
Source documentation
The backward direction: any sequence satisfying the functional equation is an arithmetic progression.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Polynomial, Int, Polynomial.Monic, Eq, WithBot, Polynomial.degree, Finsupp, Polynomial.coeff, Polynomial.eval, Finset.prod, Finset.range, HAdd.hAdd, LT.lt, Exists, HMul.hMul
Proof uses: Monotone, Imo2023P3.seq_monotone, dite, Classical.propDecidable, Imo2023P3.backward_bounded, Not, Imo2023P3.Csum, Imo2023P3.Csum_nonneg, Int.toNat, HPow.hPow, Eq.mp, Eq.trans, binderNameHint, forall_congr, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, GE.ge, Iff.mp, Int.toNat_lt' and 61 more
100 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma backward_main {k : ℕ} (hk : 2 ≤ k) {P : Polynomial ℤ} (hmon : P.Monic)
    (hdeg : P.degree = k) (hcoef : ∀ n, n ≤ k → 0 ≤ P.coeff n)
    {A : ℕ → ℕ} (hA : ∀ m, P.eval (A m : ℤ) = ∏ i ∈ Finset.range k, (A (m + 1 + i) : ℤ))
    (hpos : ∀ m, 0 < A m) :
    ∃ a₀ d : ℕ, ∀ m, A m = a₀ + d * m := by
…
```
Mentions: P
problem Imo2023P3.imo2023_p3 line 957 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, PNat, Iff, Membership.mem, Set, Imo2023P3.SolutionSet, Exists, Polynomial, Int, And, Polynomial.Monic, Eq, WithBot, Polynomial.degree, Finsupp, Polynomial.coeff, Polynomial.eval, Finset.prod and 5 more
Proof uses: Iff.intro, HMul.hMul, Exists.intro, Imo2023P3.apPoly, And.intro, Imo2023P3.apPoly_monic, Imo2023P3.apPoly_degree, Imo2023P3.apPoly_coeff_nonneg, cast, Eq.symm, HSub.hSub, Eq.mp, congrArg, Subtype, Subtype.ext, Nat.sub_add_cancel, PNat.pos, Eq.mpr, id, Imo2023P3.apPoly_eval and 57 more
88 instances, coercions and auxiliary constants left out.

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