oeis_363347_conjecture_2.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

69 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

FormalConjectures.Util.ProblemImports

def continued_fraction_denominator Helper function for A363347, which computes the denominator $R_k(n)$ of the continued fraction expression line 48 source
Source documentation
Helper function for A363347, which computes the denominator $R_k(n)$ of the continued fraction expression. For $2 \le k \le n-1$, $R_k(n)$ is defined recursively: $$R_k(n) = k - \frac{k+1}{R_{k+1}(n)}$$ The base case is $R_{n-1}(n) = (n-1) - \frac{n}{-4}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Rat
Proof uses: WellFounded.Nat.fix, HSub.hSub, InvImage, LT.lt, dite, LE.le, OfNat.ofNat, Not, And, Eq, HAdd.hAdd, HDiv.hDiv
18 instances, coercions and auxiliary constants left out.
```
def continued_fraction_denominator (n k : ℕ) : ℚ :=
…
```
def A363347 A363347: Denominator of the continued fraction line 71 source
Source documentation
A363347: Denominator of the continued fraction $$\frac{1}{2 - \frac{3}{3 - \frac{4}{4 - \frac{5}{\dots - \frac{n-1}{(n-1) - \frac{n}{-4}}}}}} $$ The value of the continued fraction is $C_n = 1/R_2(n)$. If $R_2(n) = N/D$ in reduced form, $C_n = D/N$. The sequence $a(n)$ is the denominator of the final fraction, which is $\vert N \vert$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: ite, LE.le, OfNat.ofNat, Rat, continued_fraction_denominator, Int.natAbs, Rat.num
3 instances, coercions and auxiliary constants left out.
```
noncomputable def A363347 (n : ℕ) : ℕ :=
…
```
def Z_seq line 112 source
no axioms what this means
Statement uses: Nat, Int
Proof uses: Z_seq.match_1, Unit, OfNat.ofNat, Nat.succ, HMul.hMul, HAdd.hAdd, HSub.hSub
12 instances, coercions and auxiliary constants left out.
def U_val line 120 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Rat
Proof uses: ite, LT.lt, OfNat.ofNat, HDiv.hDiv, HMul.hMul, HSub.hSub, Nat.factorial
13 instances, coercions and auxiliary constants left out.
lemma U_val_rec line 123 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Eq, Rat, U_val, HSub.hSub, HMul.hMul, HAdd.hAdd
Proof uses: id, Eq.mpr, ite, LT.lt, HDiv.hDiv, Nat.factorial, congr, congrArg, Eq.trans, ite_congr, Eq.refl, Not, mul_comm, if_neg, of_eq_true, LE.le, True, eq_true, LE.le.trans', Mathlib.Meta.NormNum.isNat_le_true and 81 more
151 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def A_seq line 129 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Rat
Proof uses: WellFounded.Nat.fix, HSub.hSub, InvImage, LT.lt, dite, GE.ge, OfNat.ofNat, Not, Eq, HMul.hMul, HAdd.hAdd
18 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/OEIS/oeis_227582_conjecture_0.lean:146 (different declaration text). Qualify references as A_seq@path.
lemma A_seq_rec line 135 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HAdd.hAdd, OfNat.ofNat, Eq, Rat, A_seq, HSub.hSub, HMul.hMul
Proof uses: Eq.mpr, ite, GE.ge, id, congrArg, A_seq.eq_1, Neg.neg, sub_eq_add_neg, if_neg, Eq.refl
37 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Z_seq_rec line 140 source
standard axioms: propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Eq, Int, Z_seq, HAdd.hAdd, HMul.hMul, HSub.hSub
Proof uses: Eq.mpr, id, congrArg, Eq.symm, Nat.sub_add_cancel, Nat.succ, Z_seq.eq_6, 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 W_rec line 145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HAdd.hAdd, Eq, Rat, HSub.hSub, HMul.hMul, A_seq, U_val
Proof uses: id, Eq.rec, dite, GE.ge, Not, NatCast.natCast, InvImage, LT.lt, WellFounded.Nat.fix, ite, HDiv.hDiv, Nat.factorial, W_rec.match_1, symm, Eq.mpr, Eq.mpr_not, Eq.refl, congr, congrArg, Eq.trans and 90 more
124 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma W_val line 153 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HSub.hSub, Eq, Rat, HMul.hMul, HDiv.hDiv, Nat.factorial, A_seq, U_val, HAdd.hAdd
Proof uses: Nat.succ, Exists, Nat.exists_eq_succ_of_ne_zero, Nat.le, HEq, Eq.rec, LE.le.trans, False, False.elim, Nat.le.refl, noConfusion_of_Nat, Nat.ctorIdx, Nat.le.step, Eq.refl, HEq.refl, Eq.mpr, inferInstance, CommGroupWithZero, id, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq and 178 more
201 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
lemma X_rec line 170 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HAdd.hAdd, Eq, Rat, HDiv.hDiv, HMul.hMul, A_seq, Nat.factorial, HSub.hSub
Proof uses: A_seq_rec, Nat.le.rec, Nat.cast_mul, Nat.succ, Nat.le, of_eq_true, Eq.trans, True, congrArg, Nat.cast_succ, eq_self, Eq.rec, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, NNRat.rawCast, Mathlib.Tactic.Ring.div_congr, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.atom_pf and 57 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def Y_val line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Rat
Proof uses: HDiv.hDiv, HMul.hMul, A_seq, Nat.factorial, HSub.hSub, OfNat.ofNat
10 instances, coercions and auxiliary constants left out.
def R_val line 179 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Rat
Proof uses: HSub.hSub, HMul.hMul, OfNat.ofNat, A_seq, Z_seq
10 instances, coercions and auxiliary constants left out.
lemma Y_rec line 181 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HAdd.hAdd, Eq, Rat, Y_val, HMul.hMul, HSub.hSub
Proof uses: X_rec
14 instances, coercions and auxiliary constants left out.
lemma R_rec line 184 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Rat, R_val, HAdd.hAdd, HMul.hMul, HSub.hSub
Proof uses: Eq.mpr, id, congrArg, Eq.symm, mul_comm, A_seq, Z_seq, R_val.eq_1, Eq.trans, congr, Nat.cast_add, add_sub_cancel_right, Int, R_rec.match_2, Z_seq.match_1, Unit, Nat.succ, Nat.rec, PProd, PProd.mk and 51 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Y_eq_R_3 line 192 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Rat, Y_val, OfNat.ofNat, R_val
Proof uses: HDiv.hDiv, HMul.hMul, A_seq, Nat.factorial, of_eq_true, HAdd.hAdd, Eq.trans, True, congr, congrArg, zero_add, mul_one, IsUnit.mul_div_cancel_right, IsUnit, Ne, Not, False, not_false_eq_true, eq_self, HSub.hSub and 70 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Y_eq_R_pair line 200 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HAdd.hAdd, OfNat.ofNat, And, Eq, Rat, Y_val, R_val
Proof uses: Nat.recAux, HDiv.hDiv, HMul.hMul, A_seq, Nat.factorial, of_eq_true, Eq.trans, True, congr, congrArg, zero_add, mul_one, IsUnit.mul_div_cancel_right, IsUnit, Ne, Not, False, not_false_eq_true, eq_self, HSub.hSub and 78 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
lemma Y_eq_R line 227 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HAdd.hAdd, OfNat.ofNat, Eq, Rat, Y_val, R_val
Proof uses: Nat.casesAuxOn, Y_eq_R_3, Eq.symm, And.right, Y_eq_R_pair, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma A_seq_Z_seq line 235 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Rat, HDiv.hDiv, HMul.hMul, A_seq, Nat.factorial, HSub.hSub, Z_seq
Proof uses: Exists, HAdd.hAdd, Nat.exists_eq_add_of_le', Y_val, R_val, Y_eq_R, Eq.mpr, id, congr, Nat.succ, congrArg, Eq.trans, Nat.succ_sub_one, Nat.cast_mul, Nat.cast_add, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, DivInvMonoid and 10 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma A_seq_n line 244 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Rat, HDiv.hDiv, HMul.hMul, A_seq, Nat.factorial, HSub.hSub, Z_seq
Proof uses: le_refl, A_seq_Z_seq
17 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def A_int line 251 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Int
Proof uses: WellFounded.Nat.fix, HSub.hSub, InvImage, LT.lt, dite, GE.ge, OfNat.ofNat, Not, Eq, HMul.hMul, HAdd.hAdd
18 instances, coercions and auxiliary constants left out.
lemma A_int_eq_d line 257 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HSub.hSub, Eq, Rat, A_seq, A_int
Proof uses: Nat.recAux, OfNat.ofNat, GE.ge, Decidable.byContradiction, Not, Eq.mpr, ite, HMul.hMul, HAdd.hAdd, id, congrArg, A_seq.eq_def, Int, A_int.eq_def, Decidable, congr, if_pos, False.elim, Eq.refl, if_neg and 7 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma A_int_eq line 281 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Rat, A_seq, A_int
Proof uses: A_int_eq_d, HSub.hSub, le_refl
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma A2_eq line 284 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Eq, Rat, A_seq, HSub.hSub, HAdd.hAdd, HPow.hPow, HMul.hMul
Proof uses: LE.le, Nat.le.refl, Decidable.byContradiction, Not, HDiv.hDiv, Nat.factorial, U_val, W_val, of_eq_true, ite, LT.lt, Eq.trans, True, congrArg, False, ite_congr, eq_false, Mathlib.Meta.NormNum.isNat_lt_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 124 more
135 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
lemma A_seq_3_2_bound line 305 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Rat, HMul.hMul, Nat.factorial, HSub.hSub, A_seq, Z_seq
Proof uses: HDiv.hDiv, A_seq_n, id, Eq.mpr, WellFounded.Nat.fix, InvImage, LT.lt, dite, GE.ge, Not, HAdd.hAdd, congrArg, WellFounded.Nat.fix_eq, dif_pos, Nat.le.refl, Eq.refl, Eq.rec, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast and 30 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
def X_int line 312 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Int
Proof uses: HMul.hMul, Nat.factorial, HSub.hSub, OfNat.ofNat, A_int
7 instances, coercions and auxiliary constants left out.
lemma A_int_rec line 314 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, HAdd.hAdd, OfNat.ofNat, Eq, Int, A_int, HSub.hSub, HMul.hMul
Proof uses: Not, GE.ge, Eq.mpr, ite, id, Eq.rec, Eq.refl, Eq.trans, congrArg, A_int.eq_1, of_eq_true, True, ite_cond_eq_false, False, eq_false, eq_self
30 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma X_int_rec line 321 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HAdd.hAdd, Eq, Int, X_int, HMul.hMul, HSub.hSub
Proof uses: A_int, A_int_rec, Nat.factorial, Nat.le.rec, Eq.refl, Nat.le, Nat.succ, id, Eq.rec, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.add_pf_add_gt, Mathlib.Tactic.Ring.add_pf_add_zero and 32 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
def Y_int line 329 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Int
Proof uses: HSub.hSub, HMul.hMul, OfNat.ofNat, X_int, HAdd.hAdd
10 instances, coercions and auxiliary constants left out.
lemma Y_int_rec line 331 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HAdd.hAdd, Eq, Int, Y_int, HMul.hMul
Proof uses: id, X_int, HSub.hSub, X_int_rec, IsEmpty, Real, Nonempty, Or, isEmpty_or_nonempty, Or.inl, False.elim, Eq.mp, False, Eq.trans, eq_false, not_false, Or.inr, Eq.mpr, Nat.factorial, A_int and 51 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Y_int_eq_fact_aux line 340 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HAdd.hAdd, OfNat.ofNat, HSub.hSub, Eq, Int, Y_int, HMul.hMul, Nat.factorial
Proof uses: Nat.recAux, rfl, Eq.mpr, id, congrArg, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.add_mul, Mathlib.Tactic.Ring.mul_add, Mathlib.Tactic.Ring.mul_pf_right, Mathlib.Tactic.Ring.one_mul, Mathlib.Tactic.Ring.mul_zero, Mathlib.Tactic.Ring.add_pf_add_zero and 13 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
lemma Y_int_eq_fact line 372 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HSub.hSub, Eq, Int, Y_int, HMul.hMul, Nat.factorial
Proof uses: Exists, HAdd.hAdd, Exists.intro, Decidable.byContradiction, Not, Y_int_eq_fact_aux, Eq.symm
22 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma A_int_n line 378 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, A_int, OfNat.ofNat
Proof uses: GE.ge, Decidable.byContradiction, Not, Eq.mpr, ite, HSub.hSub, HMul.hMul, HAdd.hAdd, id, congrArg, A_int.eq_def, of_eq_true, Eq.trans, True, ite_cond_eq_true, LE.le, eq_self
20 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma X_int_n line 383 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Eq, Int, X_int, HMul.hMul, Nat.factorial, HSub.hSub
Proof uses: id, Eq.mpr, A_int, congrArg, A_int_n, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Y_int_two_eq_A_int line 387 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, Y_int, OfNat.ofNat, A_int
Proof uses: id, HSub.hSub, HMul.hMul, X_int, HAdd.hAdd, rfl, Nat.factorial, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.mul_congr, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.sub_pf, Int.rawCast and 28 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma A_int_two_eq line 394 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Eq, Rat, A_int, HSub.hSub, HAdd.hAdd, HPow.hPow, HMul.hMul
Proof uses: Eq.mpr, A_seq, id, congrArg, Eq.symm, A_int_eq, A2_eq
32 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma A_int_two_pos line 398 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, GT.gt, Int, A_int
Proof uses: Eq, Rat, HSub.hSub, HAdd.hAdd, HPow.hPow, HMul.hMul, A_int_two_eq, cast, LT.lt, Eq.trans, congrArg, Eq.symm, Nat.cast_zero, Int.cast_zero, Eq.rec, Iff.mpr, sub_pos, LE.le, congr, Function.comp and 3 more
85 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Y_int_pos line 402 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, LE.le, HSub.hSub, GT.gt, Int, Y_int
Proof uses: Eq, HMul.hMul, Nat.factorial, Y_int_eq_fact, A_int, Y_int_two_eq_A_int, A_int_two_pos, cast, LT.lt, Eq.symm, Eq.trans, congrArg, Nat.cast_zero, Nat.factorial_pos, Eq.mpr, id, Eq.mp, mul_pos, Iff.mpr, Nat.cast_pos'
47 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma X_int_pos_d line 411 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, LE.le, HSub.hSub, GT.gt, Int, X_int
Proof uses: Nat.recAux, Eq, HMul.hMul, Nat.factorial, X_int_n, cast, LT.lt, Eq.symm, Eq.trans, congrArg, Nat.cast_zero, Nat.factorial_pos, Decidable.byContradiction, Not, Eq.mpr, id, mul_pos, Iff.mpr, Nat.cast_pos', Mathlib.Meta.Positivity.pos_of_isNat and 73 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
lemma A_int_pos line 445 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, LE.le, GT.gt, Int, A_int
Proof uses: HSub.hSub, Decidable.byContradiction, Not, X_int, X_int_pos_d, Eq, HMul.hMul, Nat.factorial, rfl, cast, LT.lt, Eq.symm, Eq.trans, congrArg, Nat.cast_zero, Nat.factorial_pos, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd and 52 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma A_seq_neq_zero line 455 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, LE.le, Ne, Rat, A_seq
Proof uses: GT.gt, Int, A_int, A_int_pos, ne_of_gt, Eq, A_int_eq, Eq.mpr, id, congrArg, cast, Eq.trans, Not, Eq.symm, Nat.cast_zero, Int.cast_zero
36 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma frac_sub_eq line 462 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Rat, Ne, OfNat.ofNat, Eq, HSub.hSub, HDiv.hDiv, HMul.hMul, HAdd.hAdd
Proof uses: Eq.mpr, id, congrArg, mul_div_cancel_right₀, Eq.refl, Eq.symm, sub_div
34 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma cf_denom_eq_A_seq_d line 467 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HSub.hSub, GT.gt, OfNat.ofNat, LE.le, Rat, continued_fraction_denominator, HDiv.hDiv, A_seq, HAdd.hAdd
Proof uses: Nat.recAux, Decidable.byContradiction, Not, Eq.mpr, ite, And, id, congrArg, continued_fraction_denominator.eq_def, Decidable, if_neg, if_pos, LT.lt, HMul.hMul, A_seq_rec, div_div_eq_mul_div, Eq.refl, GE.ge, Ne, A_seq_neq_zero and 58 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 66 steps
Open to load the checked before-and-after goal states.
lemma cf_denom_eq_A_seq line 512 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, LE.le, HSub.hSub, Eq, Rat, continued_fraction_denominator, HDiv.hDiv, A_seq, HAdd.hAdd
Proof uses: cf_denom_eq_A_seq_d, rfl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma exists_sq_eq_five line 515 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Or, Nat.ModEq, OfNat.ofNat, Exists, And, LE.le, HDiv.hDiv, Int.ModEq, Int, HPow.hPow
Proof uses: Eq.mpr, Eq.refl, by_contra, Not, absurd, Fact, False, Fact.mk, Nat.prime_five, dite, IsSquare, ZMod, Exists.elim, Eq, HMul.hMul, Eq.mp, congrArg, propext, ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one, HMod.hMod and 42 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma A_int_two_eq_Z line 524 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Eq, Int, A_int, HSub.hSub, HAdd.hAdd, HPow.hPow, HMul.hMul
Proof uses: Rat, A_int_two_eq, cast, Eq.trans, Int.subNatNat, congrArg, congr, Eq.symm
61 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Rat_num_natAbs_eq line 528 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Ne, OfNat.ofNat, Eq, Nat, Int.natAbs, Rat.num, HDiv.hDiv, Rat, Int.gcd
Proof uses: Eq.mpr, HMul.hMul, Int.sign, Nat.gcd, ite, id, congrArg, Eq.trans, Inv.inv, Rat.den, div_eq_mul_inv, Rat.mul_num, congr, Rat.num_inv, Nat.cast_one, mul_one, Rat.den_inv, ite_congr, Eq.refl, Not and 24 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma A363347_eq_reduced line 533 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Eq, A363347, HDiv.hDiv, Int.natAbs, A_int, Int.gcd
Proof uses: id, Not, LE.le, Eq.mpr, ite, Rat, continued_fraction_denominator, Rat.num, congrArg, ite_cond_eq_false, eq_false, Decidable.byContradiction, HSub.hSub, A_seq, HAdd.hAdd, cf_denom_eq_A_seq, GT.gt, A_int_eq, Ne, Int and 8 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma A_int_3_2_bound line 550 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Eq, Int, HMul.hMul, Nat.factorial, HSub.hSub, A_int, Z_seq
Proof uses: Rat, A_seq, A_seq_3_2_bound, A_int_eq, cast, Eq.trans, Int.subNatNat, congr, congrArg, Nat.cast_mul, Eq.symm, Int.cast_mul, Int.cast_ofNat, Int.cast_natCast, Eq.mp
63 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def S_val line 558 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int
Proof uses: WellFounded.Nat.fix, InvImage, LT.lt, dite, LE.le, OfNat.ofNat, Not, HAdd.hAdd, HSub.hSub, Nat.factorial
12 instances, coercions and auxiliary constants left out.
lemma S_val_rec line 563 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Int, S_val, HAdd.hAdd, Nat.factorial, HSub.hSub
Proof uses: Eq.mpr, ite, id, Eq.rec, Eq.refl, Eq.trans, S_val.eq_def, Decidable, Not, congrArg, if_neg, Decidable.byContradiction, if_pos
26 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma X_3_form_k_base line 571 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Int, HMul.hMul, HSub.hSub, A_int, HAdd.hAdd, S_val, X_int
Proof uses: Eq.mpr, ite, Nat.factorial, id, congrArg, S_val.eq_def, Decidable, Not, if_neg, Decidable.byContradiction, if_pos, rfl, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 29 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma X_3_form_k_step line 580 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HAdd.hAdd, Eq, Int, HMul.hMul, HSub.hSub, A_int, S_val, X_int
Proof uses: Decidable.byContradiction, Not, Y_int, rfl, Nat.factorial, Y_int_eq_fact, Y_int_two_eq_A_int, S_val_rec, Eq.mpr, id, congrArg, Nat.factorial_succ, Eq.trans, Nat.cast_mul, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat and 61 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 48 steps
Open to load the checked before-and-after goal states.
lemma X_3_form_k line 625 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Int, HMul.hMul, HSub.hSub, A_int, HAdd.hAdd, S_val, X_int
Proof uses: Exists, Exists.intro, Decidable.byContradiction, Not, Nat.recAux, X_3_form_k_base, X_3_form_k_step, Eq.symm
32 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma A_3_eq_n line 640 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Eq, Int, HMul.hMul, HSub.hSub, A_int, HAdd.hAdd, S_val, Nat.factorial
Proof uses: LE.le, Decidable.byContradiction, Not, X_int, X_3_form_k, X_int_n, Eq.mp, congrArg
27 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma A_3_eq_from_n line 649 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, HMul.hMul, OfNat.ofNat, HSub.hSub, A_int, HAdd.hAdd, S_val, Nat.factorial, Ne
Proof uses: Trans.trans, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.sub_pf, Mathlib.Tactic.Ring.neg_add, Mathlib.Tactic.Ring.neg_one_mul, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.isInt_mul, Int.ofNat, Mathlib.Meta.NormNum.IsInt.of_raw and 28 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma fact_n_minus_one line 661 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Eq, Int, Nat.factorial, HSub.hSub, HMul.hMul
Proof uses: HAdd.hAdd, Decidable.byContradiction, Not, Eq.mpr, id, congrArg, Nat.factorial_succ, Eq.trans, Nat.cast_mul, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.cast_pos and 31 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma A_3_eq line 678 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Eq, Int, HMul.hMul, A_int, HAdd.hAdd, S_val, HSub.hSub, Nat.factorial
Proof uses: A_3_eq_from_n, A_3_eq_n, fact_n_minus_one
20 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma S_val_even line 686 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Exists, Int, Eq, S_val, HMul.hMul
Proof uses: HAdd.hAdd, Exists.intro, HSub.hSub, Decidable.byContradiction, Not, Nat.recAux, Nat.factorial, S_val_rec, LE.le, Eq.mpr, ite, id, congrArg, S_val.eq_def, Decidable, if_neg, if_pos, Eq.refl, Mathlib.Tactic.Ring.of_eq, Nat.rawCast and 22 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
lemma k_dvd_term line 721 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, LT.lt, HMul.hMul, Eq, HSub.hSub, HAdd.hAdd, HPow.hPow, Dvd.dvd, Int, Nat.factorial
Proof uses: Dvd.dvd.mul_left, Dvd.dvd.natCast, Nat.dvd_factorial, Nat.casesAuxOn, Decidable.byContradiction, Not, Eq.symm, Eq.refl, Nat.le_sub_of_add_le, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat and 70 more
130 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma A_3_exact_from_eq line 725 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Eq, S_val, HMul.hMul, OfNat.ofNat, A_int, HAdd.hAdd, HSub.hSub, Nat.factorial
Proof uses: Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Int.rawCast, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.neg_congr and 47 more
90 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma A_3_exact line 731 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Exists, Int, Eq, A_int, HAdd.hAdd, HMul.hMul, HSub.hSub, Nat.factorial
Proof uses: S_val, S_val_even, Exists.intro, A_3_exact_from_eq, A_3_eq, Decidable.byContradiction, Not
27 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma k_dvd_A3_from_formula line 742 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Eq, Int.natAbs, A_int, HMul.hMul, Exists, Int, HAdd.hAdd, HSub.hSub, Nat.factorial, Dvd.dvd
Proof uses: Eq.mpr, id, congrArg, dvd_mul_right, cast, Eq.refl, Iff.mp, Int.dvd_natAbs, Eq.symm, dvd_add, dvd_mul_of_dvd_right
36 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma A_int_two_abs_eq line 752 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Eq, Int.natAbs, HSub.hSub, Int, HAdd.hAdd, HPow.hPow, HMul.hMul
Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.neg_congr, Mathlib.Tactic.Ring.neg_add, Mathlib.Tactic.Ring.neg_one_mul and 58 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma k_dvd_A3 line 763 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, GE.ge, OfNat.ofNat, LT.lt, HMul.hMul, Eq, Int.natAbs, A_int, Dvd.dvd, Int
Proof uses: Or, Decidable.byContradiction, Not, Eq.mpr, id, congrArg, Eq.trans, ite, HSub.hSub, HAdd.hAdd, A_int.eq_1, ite_cond_eq_true, LE.le, True, of_eq_true, by_contra, Function.comp, Nat.succ, False, of_decide_eq_true and 43 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma p_not_dvd_A3 line 783 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, GE.ge, OfNat.ofNat, LT.lt, Eq, Int.natAbs, A_int, HMul.hMul, Not, Dvd.dvd, Int
Proof uses: Nat.factorial, HSub.hSub, Z_seq, A_int_3_2_bound, Eq.mpr, id, congrArg, dvd_mul_left, cast, Eq.symm, Iff.mp, Int.dvd_natAbs, Int.dvd_sub, dvd_mul_of_dvd_right, Eq.mp, Prime, Eq.refl, Nat.prime_iff_prime_int, Or, Prime.dvd_or_dvd and 8 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
lemma A363347_eval line 811 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, GE.ge, OfNat.ofNat, LT.lt, Eq, Int.natAbs, A_int, HMul.hMul, GT.gt, Dvd.dvd, Int, Not, A363347
Proof uses: HDiv.hDiv, Int.gcd, A363347_eq_reduced, Eq.mpr, id, congrArg, Nat.gcd, Nat.Coprime.gcd_mul_right_cancel, Iff.mpr, Nat.Coprime, Nat.Prime.coprime_iff_not_dvd, Eq.mp, Nat.gcd_eq_left, Eq.refl, cast, Nat.mul_div_cancel_left
20 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma A363347_achieves_prime line 824 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Or, Nat.ModEq, OfNat.ofNat, Exists, Eq, A363347
Proof uses: GE.ge, A363347_achieves_prime.match_1, absurd, of_decide_eq_false, Eq.refl, Bool, Decidable.decide, HAdd.hAdd, Decidable.byContradiction, Not, And, LE.le, HDiv.hDiv, Int.ModEq, Int, HPow.hPow, exists_sq_eq_five, A363347_achieves_prime.match_2, LT.lt, Int.natAbs and 89 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
theorem target_theorem_0 line 848 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, And, Nat.Prime, Or, Nat.ModEq, OfNat.ofNat, Exists, Eq, A363347
Proof uses: A363347_achieves_prime, And.left, And.right
2 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_228143_conjecture_1.lean:730 (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_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: 2 steps
Open to load the checked before-and-after goal states.