oeis_228143_conjecture_1.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 348 curated AI-written annotations and 373 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 12 manuscript-grounded curated result annotations were composed from pinned companion PDFs and named source records in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Twelve supporting declarations for the Hilbert-functions result were upgraded on 2026-10-14 from mechanically condensed doc comments to declaration-specific explanations bound to exact page-one terminology in the pinned human-written companion. The other Hilbert challenge statements were deliberately not described as companion-backed results because that manuscript proves P5 specifically. Fifteen previously unannotated declarations along the Hilbert P5 proof spine were annotated on 2026-10-14 from the pinned companion's seven-page argument, covering the two-generator decomposition, finite-difference bounds, critical-case reduction, and final log-concavity step. Each quotation is bound to its exact manuscript page and Lean declaration; no human review is claimed. Twenty-four further declarations along the Hilbert P5 box-count and finite-difference spine were annotated on 2026-10-14, covering the two-dimensional slice count, three-dimensional box formula, first- and second-difference identities, the seven-threshold curvature expression, boundary handling, pointwise transport, sum linearity, and lower-or-upper region classification. Every annotation is bound to an exact quotation on pages 2 or 3 of the pinned human-written companion; Lean-specific boundary and threshold helpers are identified as implementation lemmas rather than separate manuscript claims. No human review is claimed. Twenty-eight further declarations along the Hilbert P5 argument were annotated on 2026-10-14 from pages 2 through 6 of the pinned human-written companion. They expose the shifted residual sequence, exact lower- and upper-region formulas, symmetry by complementary divisors, the curvature-one and curvature-two splits, and the final algebraic reductions. Lean-only transport and integer-arithmetic helpers are labeled as proof infrastructure rather than new manuscript claims; each quotation is page-bound in the source ledger, and no human review is claimed. Twenty high-level declarations completing the Hilbert P5 curvature-one and curvature-two case spine were annotated on 2026-10-14 from pages 3 through 7 of the pinned human-written companion. The explanations separate cases A and B, lower and upper monomial regions, shifted residual evaluation, impossible mixed regions, and the surviving upper-upper estimate; wrapper lemmas are explicitly described as proof structure. Every quotation is page-bound, and no human review is claimed. Twenty-two graph-reconstruction declarations were upgraded or added on 2026-10-14 from the pinned four-page human-written companion, covering the incidence-deletion deck, edge and degree recovery, unique isolated vertices, vertex-type reconstruction, neighboring-type descent, adjacency recovery, and final bipartite isomorphism. The result annotation also records that `G_not_regular` is present in the Lean statement but unused by its proof term and absent from the companion theorem. Exact historical quotations from Paul J. Kelly (1957) and Bondy with Hemminger (1977) are linked separately; no human review is claimed. Eighteen declarations along the Erdős 741(i) strict-natural-density counterexample were added on 2026-10-14, covering the carry-free base-four digit split, full cross-sum coverage, sparse pure self-sums, fixed-factor fat intervals, the lower-scale density deficit, upper-scale sum growth, and the final convergence contradiction. The result annotation was corrected to distinguish the negative strict-natural-density Lean theorem from the compatible affirmative upper-density companion theorem; Ulam AI's written counterexample is explicitly identified as using a different interval length with the same mechanism. The quotations are page- and hash-bound where the PDFs expose text; Paul Erdős's scanned 1994 question was visually checked and is linked separately without a machine-audit claim. No human review is claimed. Twenty-eight additional declaration-level annotations were added on 2026-10-14 for the Erdős 12(i) proof, and its IsGood definition was upgraded from a source-comment condensation. They cover the prime and Chinese-remainder moduli, the actual Lean congruence-block witness, exclusion of cross-block and same-block triples, lower and upper counting bounds, and the positive liminf. The prior result annotation was corrected because the pinned human-written companion proves the same theorem with a different base-2-to-base-3 construction; it is no longer presented as the Lean proof. The original property-P definition from Erdős and Sárközy (1970) is separately linked and page-bound; no human review is claimed. The remaining fifty declarations in the Erdős 12(i) file were annotated on 2026-10-14, completing declaration-level coverage of all eighty definitions, lemmas, and theorems in that file. These additions expose the prime-recursion invariants, divisibility transport, Chinese-remainder witness bounds, numerical density envelopes, injective block coding, and liminf support lemmas instead of leaving the proof spine as raw Lean; no human review is claimed. Eighteen supporting declarations for Erdős 125 were added on 2026-10-14, completing all nineteen declarations in the file. The annotations follow the pinned companion through digit-block decomposition, irrational logarithmic approximation, the explicit Lean contraction factor 11/12, geometric iteration, and the lower-density conclusion. The original 1996 question of Burr, Erdős, Graham, and Li and the 2026 discussion contributions of GTSoukalas, Terence Tao, and Giuseppe Melfi are linked separately; no human review is claimed. Twenty-eight supporting declarations for Erdős 138 were upgraded or added on 2026-10-14, completing all twenty-nine declarations in the file. The annotations separate the greedy difference proof from the Lean-specific representation bridges and ultrafilter compactness proof of existence, and bind quotations from the pinned companion, the AlphaProof Nexus paper, Erdős's 1981 source, van der Waerden's recollection, and the 2026 Erdős Problems discussion. No human review is claimed. The curated Erdős 12(ii), 138, and 152 annotations were further linked on 2026-10-14 to exact quotations from Felix Behrend, Bartel van der Waerden, and Paul Erdős with Pál Turán; the historical quotation sources are labeled separately from the pinned AlphaProof proof companions. The curated Hilbert-functions result, its OrderIdeal and pureOSequence definitions, and the Erdős 846 annotation were further linked on 2026-10-14 to exact quotations from Richard P. Stanley and from Moe Putterman, Mehtaab Sawhney, and Gregory Valiant. The Stanley PDF is hash- and page-bound in the source ledger; these historical sources are labeled separately from the pinned AlphaProof proof companions. Three additional target-specific annotations for Ben Green's Problem 57, exact last-iterate anchored-GDA convergence, and Graffiti.pc Conjecture 2 were composed on 2026-10-14 from the exact pinned Lean statements, quotations from the AlphaProof Nexus paper, and quotations from Green, Ryu with Yuan and Yin, Surina et al., and Wang with Dai and Tong; no human review is claimed. Two additional target-specific quantum-optics annotations for the explicit AME(11,5) construction and the even N >= 4, D = N monochromatic-quantum-graph theorem were composed on 2026-10-14 from the exact pinned Lean statements, page-bound quotations from the AlphaProof Nexus paper, Helwig et al., and Krenn, Gu, and Zeilinger, and Mario Krenn's public priority correction. The AME annotation makes no first-discovery claim; the monochromatic annotation states that the local AlphaProof wrapper contains sorry and links the separate pinned proof-bearing Formal Conjectures artifact without silently treating it as local verification. Twelve declarations that the pinned source repeats verbatim in several files were annotated in only one of the copies, so the build rejected them as differing copies. On 2026-10-16 each curated annotation was copied unchanged to every identical copy: the eleven Hilbert-functions definitions from hilbert_functions_5 to hilbert_functions_1, _2, _3, _4, _7 and _8, and Erdos12.IsGood from erdos_12.parts.i to erdos_12.parts.ii (the better-sourced annotation was kept in each case). Each copy's quotations are bound in the source ledger like the original's; no new text was written and no human review is claimed. The remaining source-derived annotations were 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 source prose.

Credit: Google DeepMind published the AlphaProof Nexus proof artifacts. The pinned repository identifies the mathematical sources and collaborators, including OEIS, Erdős Problems, Gergely Bérczi, and Mario Krenn; those source records remain the authority for individual credit.

Project sources: Pinned AlphaProof Nexus results documentation, AlphaProof Nexus paper, Pinned human-written natural-language proof companions

77 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

FormalConjectures.Util.ProblemImports

def A005259' A005259: The auxiliary sequence used for the Hankel matrix, defined as $$\sum_{k=0}^n \binom{n}{k}^2 \binom{n+k}{k}^2$$ line 46 source
Source documentation
A005259: The auxiliary sequence used for the Hankel matrix, defined as $$\sum_{k=0}^n \binom{n}{k}^2 \binom{n+k}{k}^2$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.sum, Finset.range, HAdd.hAdd, OfNat.ofNat, HMul.hMul, HPow.hPow, Nat.choose
9 instances, coercions and auxiliary constants left out.
```
def A005259' (n : ℕ) : ℕ :=
…
```
def a A228143: Determinant of the $(n+1) \times (n+1)$ Hankel-type matrix with $(i,j)$-entry equal to A005259$(i+j)$ for all $i,j = 0,\dots,n$ line 54 source
Source documentation
A228143: Determinant of the $(n+1) \times (n+1)$ Hankel-type matrix with $(i,j)$-entry equal to A005259$(i+j)$ for all $i,j = 0,\dots,n$. The entry function A005259 is taken to be $\sum_{k=0}^n \binom{n}{k}^2 \binom{n+k}{k}^2$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Fin, HAdd.hAdd, OfNat.ofNat, Matrix, Int, Equiv, Matrix.of, A005259', Int.natAbs, Matrix.det
12 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/OEIS/A309132_conjecture_carmichael.lean:45 (same statement text; different proof or body), APNOutputs/OEIS/a091669_conjecture_primitive_root.lean:46 (same statement text; different proof or body), APNOutputs/OEIS/a325046_odd_terms_at_k_times_k_plus_1.lean:52 (different declaration text), APNOutputs/OEIS/oeis_103311_conjecture_0.lean:47 (different declaration text), APNOutputs/OEIS/oeis_108_conjecture_2.lean:45 (different declaration text), APNOutputs/OEIS/oeis_113254_conjecture_0.lean:48 (different declaration text), APNOutputs/OEIS/oeis_175386_conjecture_0.lean:46 (different declaration text), APNOutputs/OEIS/oeis_194806_conjecture_0.lean:50 (same statement text; different proof or body), APNOutputs/OEIS/oeis_227582_conjecture_0.lean:60 (same statement text; different proof or body), APNOutputs/OEIS/oeis_243106_conjecture_0.lean:47 (different declaration text), APNOutputs/OEIS/oeis_248802_conjecture_0.lean:43 (different declaration text), APNOutputs/OEIS/oeis_248802_conjecture_4.lean:43 (different declaration text), APNOutputs/OEIS/oeis_267581_conjecture_0.lean:71 (same statement text; different proof or body), APNOutputs/OEIS/oeis_271591_conjecture_0.lean:57 (different declaration text), APNOutputs/OEIS/oeis_2897_conjecture_0.lean:46 (different declaration text), APNOutputs/OEIS/oeis_306424_conjecture_0.lean:52 (same statement text; different proof or body), APNOutputs/OEIS/oeis_307865_conjecture_0.lean:46 (different declaration text), APNOutputs/OEIS/oeis_323557_conjecture_0.lean:48 (different declaration text), APNOutputs/OEIS/oeis_341254_conjecture_0.lean:52 (same statement text; different proof or body), APNOutputs/OEIS/oeis_372761_conjecture_2.lean:83 (same statement text; different proof or body), APNOutputs/OEIS/oeis_62567_conjecture_0.lean:49 (same statement text; different proof or body), APNOutputs/OEIS/oeis_A028859_conjecture_1.lean:43 (different declaration text), APNOutputs/OEIS/oeis_a211417_conjecture_specific.lean:44 (different declaration text), APNOutputs/OEIS/oeis_a237271_conjecture_2.lean:49 (different declaration text), APNOutputs/OEIS/oeis_a300997_finite_difference_is_one_or_two.lean:46 (same statement text; different proof or body), APNOutputs/OEIS/oeis_a363102_conjecture_1.lean:56 (different declaration text), APNOutputs/OEIS/oeis_a368692_conjecture_integrality.lean:47 (different declaration text). Qualify references as a@path.
```
noncomputable def a (n : ℕ) : ℕ :=
…
```
def OGF_A_scaled The power series $A(x/3) = \sum_{n=0}^\infty \frac{a(n)}{3^n} x^n$ over ℚ line 65 source
Source documentation
The power series $A(x/3) = \sum_{n=0}^\infty \frac{a(n)}{3^n} x^n$ over ℚ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Rat
Proof uses: PowerSeries.mk, Nat, HDiv.hDiv, a, HPow.hPow, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
noncomputable def OGF_A_scaled : PowerSeries ℚ :=
…
```
lemma alt_sum_choose line 104 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, Finset.sum, Finset.range, HAdd.hAdd, OfNat.ofNat, HMul.hMul, HPow.hPow, Neg.neg, Nat.choose
Proof uses: Eq.mpr, Prod, Finset.HasAntidiagonal.antidiagonal, Prod.fst, Prod.snd, id, Eq.trans, congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Nat.add_choose_eq, Nat.cast_sum, Nat.cast_mul, Finset.mul_sum, mul_assoc, Function.Embedding, Function.Embedding.mk, Prod.mk and 114 more
151 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma choose_mul_choose_eq line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMul.hMul, Nat.choose, HAdd.hAdd, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrArg, HSub.hSub, congr, two_mul, Nat.choose_mul, LE.le, Nat.add_sub_cancel, Nat.mul_comm, eq_self
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma lucas_3 line 128 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int.ModEq, OfNat.ofNat, Int, Nat.choose, HMul.hMul, HDiv.hDiv, HMod.hMod
Proof uses: Eq.symm, cast, Eq, Eq.trans, congrArg, Nat.strongRec, Nat.casesAuxOn, LT.lt, Eq.refl, HAdd.hAdd, of_eq_true, True, congr, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_natDiv, Mathlib.Meta.NormNum.isNat_ofNat, add_assoc, Mathlib.Meta.NormNum.isNat_add, Nat.add_div_right, Mathlib.Meta.NormNum.isNat_lt_true and 30 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
lemma choose_2k_mod_3 line 150 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Or, Int.ModEq, OfNat.ofNat, Int, Nat.choose, HMul.hMul, HPow.hPow, Neg.neg
Proof uses: Nat.strongRecOn, LT.lt, Eq, Ne, eq_or_ne, Or.inr, Eq.refl, HMod.hMod, Eq.symm, Decidable.byContradiction, Not, of_eq_true, Eq.trans, True, congrArg, Nat.mul_mod, eq_true_of_decide, Bool, Bool.true, HDiv.hDiv and 44 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
lemma choose_n_plus_k_mod_3 line 171 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Or, Int.ModEq, OfNat.ofNat, Int, Nat.choose, HMul.hMul, HAdd.hAdd
Proof uses: Nat.strongRecOn, LT.lt, Eq, Ne, eq_or_ne, Or.inr, of_eq_true, Eq.trans, True, congrArg, congr, add_zero, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_mul, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Nat.choose_zero_right, Nat.cast_one, eq_true, True.intro and 35 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 54 steps
Open to load the checked before-and-after goal states.
lemma choose_square_mod_3_step1_helper line 203 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Nat, Or, Int.ModEq, OfNat.ofNat, HPow.hPow, Neg.neg, HMul.hMul
Proof uses: Eq.mpr, Eq, HMod.hMod, id, congrArg, sq, Or.inl, of_eq_true, Eq.trans, True, congr, Int.mul_emod, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.isInt_emod, Int.ofNat, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool and 11 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma choose_square_mod_3_step1 line 210 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int.ModEq, OfNat.ofNat, Int, HPow.hPow, HMul.hMul, Nat.choose, HAdd.hAdd, Neg.neg
Proof uses: Or, choose_2k_mod_3, choose_n_plus_k_mod_3, choose_square_mod_3_step1_helper, Or.elim, Not, em, of_eq_true, Eq, HMod.hMod, Eq.trans, True, congr, congrArg, sq, Int.mul_emod, Or.resolve_right, MulZeroClass.mul_zero, eq_true_of_decide, Eq.refl and 2 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma choose_square_mod_3 line 217 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int.ModEq, OfNat.ofNat, Int, HPow.hPow, HMul.hMul, Nat.choose, HAdd.hAdd, Neg.neg
Proof uses: Eq, cast, Eq.symm, Eq.trans, congr, congrArg, choose_mul_choose_eq, Eq.mpr, id, choose_square_mod_3_step1, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.pow_congr, Mathlib.Tactic.Ring.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 23 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma A005259_mod_3 line 229 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int.ModEq, OfNat.ofNat, Int, A005259', HPow.hPow, Neg.neg
Proof uses: Eq, Finset.sum, Finset.range, HAdd.hAdd, HMul.hMul, Nat.choose, alt_sum_choose, choose_square_mod_3, id, of_eq_true, Eq.trans, True, congr, congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Nat.cast_sum, Nat.cast_pow and 4 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def P_mat line 235 source
standard axioms: propext what this means
Statement uses: Nat, Matrix, Fin, HAdd.hAdd, OfNat.ofNat, Int
Proof uses: ite, Eq, Neg.neg, HPow.hPow
14 instances, coercions and auxiliary constants left out.
lemma det_P_mat line 238 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, Matrix.det, Fin, HAdd.hAdd, OfNat.ofNat, P_mat
Proof uses: id, Eq.mpr, ite, Neg.neg, HPow.hPow, Matrix.submatrix, Nat.succ, Fin.succ, Finset.sum, Finset.univ, HMul.hMul, Fin.succAbove, congrArg, True, Eq.trans, Matrix.det.congr_simp, funext, ite_congr, Eq.refl, Not and 43 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma P_mat_mul_M_val line 245 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, GE.ge, Eq, Int, HMul.hMul, Matrix, P_mat, Equiv, Matrix.of, A005259', HSub.hSub, HPow.hPow, Neg.neg
Proof uses: Eq.mpr, Finset.sum, Finset.univ, ite, id, congr, congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Eq.trans, ite_congr, Not, ite_mul, one_mul, neg_mul, MulZeroClass.zero_mul, sub_eq_add_neg, Finset.filter and 32 more
101 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma P_mat_mul_M_div_3 line 252 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, GE.ge, Dvd.dvd, Int, HMul.hMul, Matrix, P_mat, Equiv, Matrix.of, A005259'
Proof uses: Eq, HSub.hSub, HPow.hPow, Neg.neg, P_mat_mul_M_val, Eq.mpr, id, congrArg, Int.ModEq, A005259_mod_3, Int.ModEq.dvd, Int.ModEq.symm, Int.ModEq.trans, pow_add, Int.ModEq.refl, Int.ModEq.mul_left
42 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def D_mat line 260 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, HAdd.hAdd, OfNat.ofNat, Int
Proof uses: Matrix.diagonal, ite, Eq
18 instances, coercions and auxiliary constants left out.
lemma det_D_mat line 263 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, Matrix.det, Fin, HAdd.hAdd, OfNat.ofNat, D_mat, HPow.hPow
Proof uses: id, of_eq_true, Matrix.diagonal, ite, Eq.trans, True, congrArg, Finset.prod, Finset.univ, Matrix.det.congr_simp, Matrix, funext, ite_congr, Eq.refl, Not, Matrix.det_diagonal, Multiset.prod, Multiset.map, Finset.val, List.cons and 19 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def M_prime line 267 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, HAdd.hAdd, OfNat.ofNat, Int
Proof uses: ite, Eq, A005259', HDiv.hDiv, HMul.hMul, P_mat, Equiv, Matrix.of
20 instances, coercions and auxiliary constants left out.
lemma P_mul_M_eq_D_mul_M_prime line 271 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Matrix, Fin, HAdd.hAdd, OfNat.ofNat, Int, HMul.hMul, P_mat, Equiv, Matrix.of, A005259', D_mat, M_prime
Proof uses: Matrix.ext, dite, Eq.mpr, Finset.sum, Finset.univ, ite, Neg.neg, Matrix.diagonal, id, congr, congrArg, Eq.trans, Eq.mp, Finset.sum_congr, Eq.refl, Finset, Membership.mem, HPow.hPow, ite_congr, Not and 25 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma a_div_3_pow line 286 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Dvd.dvd, HPow.hPow, OfNat.ofNat, a
Proof uses: Eq, Matrix, Fin, HAdd.hAdd, Int, HMul.hMul, P_mat, Equiv, Matrix.of, A005259', D_mat, M_prime, P_mul_M_eq_D_mul_M_prime, Matrix.det, Eq.mpr, id, congrArg, Eq.refl, Exists.intro, Eq.mp and 10 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma choose_square_mod_4 line 299 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Int.ModEq, Int, HPow.hPow, HMul.hMul, Nat.choose, HAdd.hAdd
Proof uses: Dvd.dvd.modEq_zero_int, pow_dvd_pow_of_dvd, cast, Dvd.dvd, Eq.symm, Eq.trans, congrArg, dite, Eq, Exists.intro, Not, Eq.rec, Finset.sum, Prod, Finset.HasAntidiagonal.antidiagonal, Prod.fst, Prod.snd, Eq.mpr, Finset.range, id and 48 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma A005259_mod_4 line 308 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int.ModEq, OfNat.ofNat, Int, A005259'
Proof uses: GE.ge, HPow.hPow, HMul.hMul, Nat.choose, HAdd.hAdd, choose_square_mod_4, Eq.mpr, Eq, HMod.hMod, Finset.sum, Finset.range, id, congrArg, Eq.trans, Nat.cast_sum, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Nat.cast_mul and 30 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def P_mat4 line 313 source
no axioms what this means
Statement uses: Nat, Matrix, Fin, HAdd.hAdd, OfNat.ofNat, Int
Proof uses: ite, Eq, Neg.neg
11 instances, coercions and auxiliary constants left out.
lemma det_P_mat4 line 316 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, Matrix.det, Fin, HAdd.hAdd, OfNat.ofNat, P_mat4
Proof uses: id, Eq.mpr, ite, Neg.neg, Finset.sum, Finset.univ, Nat.succ, HMul.hMul, HPow.hPow, Matrix.submatrix, Fin.succAbove, Fin.succ, congrArg, Eq.trans, Matrix.det.congr_simp, funext, ite_congr, Eq.refl, Not, Matrix.det_succ_column_zero and 64 more
114 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma P_mat4_mul_M_val line 326 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, GE.ge, Eq, Int, HMul.hMul, Matrix, P_mat4, Equiv, Matrix.of, A005259', HSub.hSub
Proof uses: Eq.mpr, Finset.sum, Finset.univ, ite, Neg.neg, id, congr, congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Eq.trans, ite_congr, Not, ite_mul, one_mul, neg_mul, MulZeroClass.zero_mul, sub_eq_add_neg and 20 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma P_mat4_mul_M_div_4 line 332 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, GE.ge, Dvd.dvd, Int, HMul.hMul, Matrix, P_mat4, Equiv, Matrix.of, A005259'
Proof uses: Eq, HSub.hSub, P_mat4_mul_M_val, Eq.mpr, id, congrArg, Int.ModEq, A005259_mod_4, Int.ModEq.dvd, Int.ModEq.symm, Int.ModEq.trans
34 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def D_mat4 line 340 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, HAdd.hAdd, OfNat.ofNat, Int
Proof uses: Matrix.diagonal, ite, Eq
18 instances, coercions and auxiliary constants left out.
lemma det_D_mat4 line 343 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, Matrix.det, Fin, HAdd.hAdd, OfNat.ofNat, D_mat4, HPow.hPow
Proof uses: id, of_eq_true, Matrix.diagonal, ite, Eq.trans, True, congrArg, Finset.prod, Finset.univ, Matrix.det.congr_simp, Matrix, funext, ite_congr, Eq.refl, Not, Matrix.det_diagonal, Multiset.prod, Multiset.map, Finset.val, List.cons and 19 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def M_prime4 line 347 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, HAdd.hAdd, OfNat.ofNat, Int
Proof uses: ite, Eq, A005259', HDiv.hDiv, HMul.hMul, P_mat4, Equiv, Matrix.of
20 instances, coercions and auxiliary constants left out.
lemma P_mul_M_eq_D_mul_M_prime4 line 351 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Matrix, Fin, HAdd.hAdd, OfNat.ofNat, Int, HMul.hMul, P_mat4, Equiv, Matrix.of, A005259', D_mat4, M_prime4
Proof uses: Matrix.ext, dite, Eq.mpr, Finset.sum, Finset.univ, ite, Neg.neg, Matrix.diagonal, HDiv.hDiv, id, congr, congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Eq.trans, ite_congr, Not, ite_mul and 31 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma a_div_4_pow line 366 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Dvd.dvd, HPow.hPow, OfNat.ofNat, a
Proof uses: Eq, Matrix, Fin, HAdd.hAdd, Int, HMul.hMul, P_mat4, Equiv, Matrix.of, A005259', D_mat4, M_prime4, P_mul_M_eq_D_mul_M_prime4, Matrix.det, Eq.mpr, id, congrArg, Eq.refl, Exists.intro, Eq.mp and 10 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
def A005259_comp line 378 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.sum, Finset.range, HAdd.hAdd, OfNat.ofNat, HMul.hMul, HPow.hPow, Nat.choose
9 instances, coercions and auxiliary constants left out.
def a_comp line 382 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Fin, HAdd.hAdd, OfNat.ofNat, Matrix, Int, Equiv, Matrix.of, A005259_comp, Int.natAbs, Matrix.det
12 instances, coercions and auxiliary constants left out.
lemma a_comp_val_1 line 388 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, a_comp, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma a_val_1 line 390 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, a, OfNat.ofNat
Proof uses: a_comp, id, Fin, HAdd.hAdd, Matrix, Int, Equiv, Matrix.of, A005259', Int.natAbs, Matrix.det, A005259_comp, Finset.sum, Finset.range, HMul.hMul, HPow.hPow, Nat.choose, Eq.refl, Eq.mpr, congrArg and 1 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma a_mod_16 line 397 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Dvd.dvd, a
Proof uses: HPow.hPow, a_div_4_pow, Nat.casesAuxOn, Eq, Decidable.byContradiction, Not, Eq.symm, HAdd.hAdd, Eq.mpr, id, congrArg, a_val_1, Exists.intro, HMul.hMul, rfl, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.pow_congr, Mathlib.Tactic.Ring.cast_pos and 25 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma a_div_16_mul_3_pow line 412 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Dvd.dvd, HMul.hMul, HPow.hPow, a
Proof uses: a_mod_16, a_div_3_pow, IsCoprime, Int, Tactic.NormNum.isInt_isCoprime, Int.ofNat, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Iff.mpr, Eq, Int.gcd, Int.isCoprime_iff_gcd_eq_one, Tactic.NormNum.int_gcd_helper, Int.natAbs_natCast, Tactic.NormNum.nat_gcd_helper_2', IsCoprime.pow_right, Exists, HAdd.hAdd, Int.ofNat_dvd and 34 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
def B_seq line 437 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int
Proof uses: HDiv.hDiv, a, HPow.hPow, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/OEIS/oeis_227582_conjecture_0.lean:147 (different declaration text), APNOutputs/OEIS/oeis_248802_conjecture_0.lean:84 (different declaration text). Qualify references as B_seq@path.
lemma B_seq_zero line 440 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Int, B_seq, OfNat.ofNat, Nat
Proof uses: Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma B_seq_mod_16 line 443 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Dvd.dvd, Int, B_seq
Proof uses: HMul.hMul, HPow.hPow, a, a_div_16_mul_3_pow, Iff.mpr, Int.ofNat_dvd, id, Eq, HDiv.hDiv, Ne, ne_of_gt, pow_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble, Trans.trans, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd and 23 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
def B_series line 455 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Int
Proof uses: PowerSeries.mk, B_seq
lemma map_B_series line 458 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, PowerSeries, Rat, RingHom, Int, PowerSeries.map, Int.castRingHom, B_series, OGF_A_scaled
Proof uses: PowerSeries.ext, Nat, Eq.mpr, LinearMap, RingHom.id, PowerSeries.coeff, HDiv.hDiv, a, HPow.hPow, OfNat.ofNat, id, congr, RingHom.mk, MonoidHom.mk, OneHom.mk, Int.cast_mul, PowerSeries.mk, B_seq, congrArg, PowerSeries.coeff_mk and 18 more
99 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
def Y_seq line 470 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int
Proof uses: ite, Eq, OfNat.ofNat, HDiv.hDiv, B_seq
5 instances, coercions and auxiliary constants left out.
def Y_series line 473 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Int
Proof uses: PowerSeries.mk, Y_seq
lemma B_series_eq_1_plus_16_Y line 476 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, PowerSeries, Int, B_series, HAdd.hAdd, OfNat.ofNat, Unit, HMul.hMul, Nat, Y_series
Proof uses: PowerSeries.ext, Nat.casesAuxOn, LinearMap, RingHom.id, PowerSeries.coeff, Eq.mpr, RingHom, PowerSeries.constantCoeff, id, congr, congrArg, PowerSeries.coeff_zero_eq_constantCoeff, Eq.trans, congrFun, map_add, map_mul, Eq.refl, Eq.symm, B_seq, PowerSeries.mk and 17 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma Y_series_zero line 501 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Int, LinearMap, RingHom.id, PowerSeries, PowerSeries.coeff, OfNat.ofNat, Nat, Y_series
Proof uses: id, Eq.mpr, PowerSeries.mk, Y_seq, congrArg, PowerSeries.coeff_mk, of_eq_true, ite, HDiv.hDiv, B_seq, Eq.trans, True, ite_cond_eq_true, eq_self
25 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def ValuationGe line 512 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PowerSeries, Int
Proof uses: LT.lt, Eq, LinearMap, RingHom.id, PowerSeries.coeff, OfNat.ofNat
11 instances, coercions and auxiliary constants left out.
lemma ValuationGe_zero line 515 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Int, ValuationGe, OfNat.ofNat, Nat
Proof uses: LT.lt, Decidable.byContradiction, Eq, LinearMap, RingHom.id, PowerSeries.coeff, Not
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ValuationGe_mul line 519 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PowerSeries, Int, ValuationGe, HAdd.hAdd, HMul.hMul, Unit
Proof uses: LT.lt, Eq.mpr, Eq, LinearMap, RingHom.id, PowerSeries.coeff, OfNat.ofNat, Finset.sum, Prod, Finset.HasAntidiagonal.antidiagonal, Prod.fst, Prod.snd, id, congrArg, PowerSeries.coeff_mul, Finset.sum_eq_zero, Membership.mem, Finset, Prod.mk, Or and 8 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma ValuationGe_add line 533 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PowerSeries, Int, ValuationGe, HAdd.hAdd
Proof uses: LT.lt, Eq.mpr, Eq, LinearMap, RingHom.id, PowerSeries.coeff, OfNat.ofNat, id, congrArg, map_add, add_zero, Eq.refl
38 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ValuationGe_pow_ge_one line 538 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, PowerSeries, Int, ValuationGe, HPow.hPow
Proof uses: Eq, HAdd.hAdd, Exists, Nat.exists_eq_succ_of_ne_zero, Eq.mpr, id, congrArg, HMul.hMul, pow_succ, ValuationGe_zero, Unit, ValuationGe_mul, Eq.mp, zero_add
31 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma diff_pow_eq line 546 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PowerSeries, Int, Exists, And, Eq, HSub.hSub, HPow.hPow, HAdd.hAdd, OfNat.ofNat, HMul.hMul, Unit, ValuationGe
Proof uses: Nat.recAux, Exists.intro, And.intro, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.pow_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.cast_pos, Mathlib.Tactic.Ring.add_pf_zero_add, Mathlib.Tactic.Ring.pow_add, Mathlib.Tactic.Ring.single_pow, Mathlib.Tactic.Ring.mul_pow and 45 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
lemma ValuationGe_diff_pow line 572 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PowerSeries, Int, ValuationGe, HAdd.hAdd, OfNat.ofNat, HSub.hSub, HPow.hPow
Proof uses: And, Eq, HMul.hMul, Unit, Exists, diff_pow_eq, Eq.mpr, id, congrArg, ValuationGe_mul, Decidable.byContradiction, Not, Eq.mp
34 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma ValuationGe_const_mul line 582 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PowerSeries, Int, ValuationGe, HMul.hMul, Unit
Proof uses: OfNat.ofNat, ValuationGe_zero, HAdd.hAdd, ValuationGe_mul, Eq.mp, congrArg, zero_add
15 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma coeff_const_mul_pow_eq line 588 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PowerSeries, Int, ValuationGe, HAdd.hAdd, OfNat.ofNat, HSub.hSub, Eq, LinearMap, RingHom.id, PowerSeries.coeff, HMul.hMul, Unit, HPow.hPow
Proof uses: ValuationGe_diff_pow, ValuationGe_const_mul, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.pow_congr, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.add_pf_add_gt, Mathlib.Tactic.Ring.add_pf_add_zero, Mathlib.Tactic.Ring.pow_add, Mathlib.Tactic.Ring.single_pow, Mathlib.Tactic.Ring.mul_pow and 32 more
85 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
def P_poly line 600 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Int
Proof uses: HAdd.hAdd, HMul.hMul, Unit, OfNat.ofNat, HPow.hPow, Nat
27 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/OEIS/oeis_51293_conjecture_0.lean:302 (different declaration text). Qualify references as P_poly@path.
lemma coeff_P_poly_eq line 603 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PowerSeries, Int, ValuationGe, HAdd.hAdd, OfNat.ofNat, HSub.hSub, Eq, LinearMap, RingHom.id, PowerSeries.coeff, P_poly
Proof uses: id, Eq.mpr, HMul.hMul, Unit, HPow.hPow, congr, congrArg, Eq.trans, map_add, coeff_const_mul_pow_eq, Eq.refl
63 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma one_plus_two_X_pow_8 line 616 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Int, Eq, HPow.hPow, Nat, HAdd.hAdd, OfNat.ofNat, Unit, HMul.hMul, P_poly
Proof uses: id, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.pow_congr, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Tactic.Ring.mul_congr, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_mul, Mathlib.Tactic.Ring.mul_add, Mathlib.Tactic.Ring.mul_pf_right, Mathlib.Tactic.Ring.mul_one, Mathlib.Tactic.Ring.mul_zero, Mathlib.Tactic.Ring.add_pf_add_zero, Mathlib.Tactic.Ring.zero_mul and 21 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def X_seq line 621 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int
Proof uses: WellFounded.Nat.fix, InvImage, LT.lt, X_seq.match_1, Unit, OfNat.ofNat, Nat.succ, PowerSeries, PowerSeries.mk, dite, HAdd.hAdd, Not, HSub.hSub, LinearMap, RingHom.id, PowerSeries.coeff, P_poly
18 instances, coercions and auxiliary constants left out.
def X_series line 628 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Int
Proof uses: PowerSeries.mk, X_seq, Nat, LinearMap, RingHom.id, PowerSeries.coeff
9 instances, coercions and auxiliary constants left out.
lemma X_series_coeff_zero line 631 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Int, Eq, LinearMap, RingHom.id, PowerSeries.coeff, OfNat.ofNat, Nat, X_series
Proof uses: id, Eq.mpr, PowerSeries.mk, X_seq, congrArg, PowerSeries.coeff_mk, of_eq_true, eq_self
22 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def trunc_ps line 636 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PowerSeries, Int
Proof uses: PowerSeries.mk, ite, LT.lt, LinearMap, RingHom.id, PowerSeries.coeff, OfNat.ofNat
12 instances, coercions and auxiliary constants left out.
lemma trunc_ps_coeff_lt line 639 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PowerSeries, Int, LT.lt, Eq, LinearMap, RingHom.id, PowerSeries.coeff, trunc_ps
Proof uses: id, Eq.mpr, PowerSeries.mk, ite, OfNat.ofNat, congrArg, PowerSeries.coeff_mk, if_pos, Eq.refl
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma trunc_ps_coeff_ge line 644 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PowerSeries, Int, Not, LT.lt, Eq, LinearMap, RingHom.id, PowerSeries.coeff, trunc_ps, OfNat.ofNat
Proof uses: id, Eq.mpr, PowerSeries.mk, ite, congrArg, PowerSeries.coeff_mk, if_neg, Eq.refl
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma X_series_val_one line 649 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Int, ValuationGe, OfNat.ofNat, Nat, X_series
Proof uses: LT.lt, Eq, Decidable.byContradiction, Not, Eq.mpr, LinearMap, RingHom.id, PowerSeries.coeff, id, congrArg, X_series_coeff_zero, Eq.refl
15 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma trunc_ps_val_one line 654 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PowerSeries, Int, ValuationGe, OfNat.ofNat, trunc_ps
Proof uses: LT.lt, Eq, Decidable.byContradiction, Not, Eq.mpr, LinearMap, RingHom.id, PowerSeries.coeff, id, congrArg, dite, trunc_ps_coeff_lt, trunc_ps_coeff_ge, Eq.refl
17 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma val_diff_trunc line 663 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PowerSeries, Int, ValuationGe, HSub.hSub, trunc_ps
Proof uses: LT.lt, Eq, LinearMap, RingHom.id, PowerSeries.coeff, map_sub, RingHom, Eq.mpr, OfNat.ofNat, id, congrArg, trunc_ps_coeff_lt, sub_self, Eq.refl
39 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma X_series_coeff_succ line 668 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Int, Nat, Eq, LinearMap, RingHom.id, PowerSeries.coeff, HAdd.hAdd, OfNat.ofNat, X_series, HSub.hSub, P_poly, trunc_ps
Proof uses: id, of_eq_true, PowerSeries.mk, X_seq, HMul.hMul, Unit, HPow.hPow, ite, LT.lt, Eq.trans, True, LE.le, congr, congrArg, PowerSeries.coeff_mk, Nat.succ, X_seq.eq_2, funext, ite_congr, Eq.refl and 5 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma X_plus_P_poly_eq_Y_coeff line 673 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Int, Nat, Eq, LinearMap, RingHom.id, PowerSeries.coeff, HAdd.hAdd, OfNat.ofNat, X_series, P_poly
Proof uses: HSub.hSub, trunc_ps, X_series_coeff_succ, map_add, Eq.mpr, id, congrArg, ValuationGe, val_diff_trunc, X_series_val_one, trunc_ps_val_one, coeff_P_poly_eq, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.add_congr, Int.rawCast, Int.negOfNat and 20 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma coeff_zero_P_poly line 685 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Int, Eq, LinearMap, RingHom.id, PowerSeries.coeff, OfNat.ofNat, Nat, P_poly
Proof uses: of_eq_true, HAdd.hAdd, HMul.hMul, Unit, HPow.hPow, Eq.trans, True, congrArg, RingHom, PowerSeries.constantCoeff, congrFun, PowerSeries.coeff_zero_eq_constantCoeff, map_add, congr, map_mul, map_pow, id, Eq.mp, zero_pow, Not and 5 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma X_plus_P_poly_eq_Y_zero line 689 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Int, Eq, LinearMap, RingHom.id, PowerSeries.coeff, OfNat.ofNat, Nat, HAdd.hAdd, X_series, P_poly
Proof uses: Eq.mpr, id, congrArg, map_add, X_series_coeff_zero, coeff_zero_P_poly, zero_add, Eq.refl
49 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma X_plus_P_poly_eq_Y line 695 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Int, Eq, LinearMap, RingHom.id, PowerSeries.coeff, OfNat.ofNat, Nat, HAdd.hAdd, X_series, P_poly
Proof uses: PowerSeries.ext, Nat.casesAuxOn, X_plus_P_poly_eq_Y_zero, Eq.symm, X_plus_P_poly_eq_Y_coeff, Eq.refl
42 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma X_series_pow_8 line 703 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Int, Eq, LinearMap, RingHom.id, PowerSeries.coeff, OfNat.ofNat, Nat, HPow.hPow, HAdd.hAdd, Unit, HMul.hMul, X_series
Proof uses: P_poly, one_plus_two_X_pow_8, X_plus_P_poly_eq_Y, Eq.mp, congrArg
68 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma exists_seq_P line 710 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Int, Eq, LinearMap, RingHom.id, PowerSeries.coeff, OfNat.ofNat, Nat, Exists, And, HPow.hPow, HAdd.hAdd, Unit, HMul.hMul
Proof uses: Exists.intro, X_series, And.intro, X_series_coeff_zero, X_series_pow_8
68 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma exists_eighth_root_B line 718 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, PowerSeries, Int, Eq, HPow.hPow, Nat, OfNat.ofNat, B_series
Proof uses: LinearMap, RingHom.id, PowerSeries.coeff, Y_series, Y_series_zero, And, HAdd.hAdd, Unit, HMul.hMul, exists_seq_P, Exists.intro, Eq.mpr, id, congrArg, Eq.symm, B_series_eq_1_plus_16_Y
43 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem target_theorem_0 line 730 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, PowerSeries, Int, Eq, Rat, RingHom, PowerSeries.map, Int.castRingHom, HPow.hPow, Nat, OfNat.ofNat, OGF_A_scaled
Proof uses: B_series, exists_eighth_root_B, Exists.intro, Eq.mpr, id, congrArg, map_B_series
29 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/OEIS/A224515_conjecture_existence.lean:269 (different declaration text), APNOutputs/OEIS/A309132_conjecture_carmichael.lean:375 (different declaration text), APNOutputs/OEIS/A382590_conjecture_kth_prime_factor_is_eventually_periodic.lean:303 (different declaration text), APNOutputs/OEIS/a091669_conjecture_primitive_root.lean:275 (different declaration text), APNOutputs/OEIS/a325046_odd_terms_at_k_times_k_plus_1.lean:187 (different declaration text), APNOutputs/OEIS/oeis_103311_conjecture_0.lean:240 (different declaration text), APNOutputs/OEIS/oeis_108_conjecture_2.lean:281 (different declaration text), APNOutputs/OEIS/oeis_113254_conjecture_0.lean:153 (different declaration text), APNOutputs/OEIS/oeis_175386_conjecture_0.lean:326 (different declaration text), APNOutputs/OEIS/oeis_194806_conjecture_0.lean:495 (different declaration text), APNOutputs/OEIS/oeis_227582_conjecture_0.lean:306 (different declaration text), APNOutputs/OEIS/oeis_243106_conjecture_0.lean:164 (different declaration text), APNOutputs/OEIS/oeis_248802_conjecture_0.lean:223 (different declaration text), APNOutputs/OEIS/oeis_248802_conjecture_4.lean:841 (different declaration text), APNOutputs/OEIS/oeis_256012_conjecture_0.lean:116 (different declaration text), APNOutputs/OEIS/oeis_267581_conjecture_0.lean:212 (different declaration text), APNOutputs/OEIS/oeis_271591_conjecture_0.lean:518 (different declaration text), APNOutputs/OEIS/oeis_278070_conjecture_0.lean:91 (different declaration text), APNOutputs/OEIS/oeis_282779_conjecture_0.lean:141 (different declaration text), APNOutputs/OEIS/oeis_289411_conjecture_0.lean:189 (different declaration text), APNOutputs/OEIS/oeis_2897_conjecture_0.lean:427 (different declaration text), APNOutputs/OEIS/oeis_306424_conjecture_0.lean:300 (different declaration text), APNOutputs/OEIS/oeis_307865_conjecture_0.lean:212 (different declaration text), APNOutputs/OEIS/oeis_323557_conjecture_0.lean:214 (different declaration text), APNOutputs/OEIS/oeis_340737_conjecture_0.lean:456 (different declaration text), APNOutputs/OEIS/oeis_341254_conjecture_0.lean:136 (different declaration text), APNOutputs/OEIS/oeis_363347_conjecture_2.lean:848 (different declaration text), APNOutputs/OEIS/oeis_372761_conjecture_2.lean:756 (different declaration text), APNOutputs/OEIS/oeis_51293_conjecture_0.lean:517 (different declaration text), APNOutputs/OEIS/oeis_62567_conjecture_0.lean:329 (different declaration text), APNOutputs/OEIS/oeis_A028859_conjecture_1.lean:432 (different declaration text), APNOutputs/OEIS/oeis_A258667_conjecture_0.lean:446 (different declaration text), APNOutputs/OEIS/oeis_a211417_conjecture_specific.lean:264 (different declaration text), APNOutputs/OEIS/oeis_a237271_conjecture_2.lean:124 (different declaration text), APNOutputs/OEIS/oeis_a300997_finite_difference_is_one_or_two.lean:1111 (different declaration text), APNOutputs/OEIS/oeis_a363102_conjecture_1.lean:302 (different declaration text), APNOutputs/OEIS/oeis_a368692_conjecture_integrality.lean:182 (different declaration text). Qualify references as target_theorem_0@path.

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