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

78 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

FormalConjectures.Util.ProblemImports

def a A248802: Smallest prime factor of $2^{(2^n+2)} + 3$ line 43 source
Source documentation
A248802: Smallest prime factor of $2^{(2^n+2)} + 3$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Nat.minFac, HAdd.hAdd, HPow.hPow, OfNat.ofNat
6 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/OEIS/A309132_conjecture_carmichael.lean:45 (different declaration text), APNOutputs/OEIS/a091669_conjecture_primitive_root.lean:46 (different declaration text), 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 (same statement text; different proof or body), APNOutputs/OEIS/oeis_113254_conjecture_0.lean:48 (different declaration text), APNOutputs/OEIS/oeis_175386_conjecture_0.lean:46 (same statement text; different proof or body), APNOutputs/OEIS/oeis_194806_conjecture_0.lean:50 (different declaration text), APNOutputs/OEIS/oeis_227582_conjecture_0.lean:60 (different declaration text), APNOutputs/OEIS/oeis_228143_conjecture_1.lean:54 (different declaration text), APNOutputs/OEIS/oeis_243106_conjecture_0.lean:47 (different declaration text), APNOutputs/OEIS/oeis_248802_conjecture_0.lean:43 (same statement text; different proof or body), APNOutputs/OEIS/oeis_267581_conjecture_0.lean:71 (different declaration text), APNOutputs/OEIS/oeis_271591_conjecture_0.lean:57 (same statement text; different proof or body), APNOutputs/OEIS/oeis_2897_conjecture_0.lean:46 (same statement text; different proof or body), APNOutputs/OEIS/oeis_306424_conjecture_0.lean:52 (different declaration text), APNOutputs/OEIS/oeis_307865_conjecture_0.lean:46 (same statement text; different proof or body), APNOutputs/OEIS/oeis_323557_conjecture_0.lean:48 (different declaration text), APNOutputs/OEIS/oeis_341254_conjecture_0.lean:52 (different declaration text), APNOutputs/OEIS/oeis_372761_conjecture_2.lean:83 (different declaration text), APNOutputs/OEIS/oeis_62567_conjecture_0.lean:49 (different declaration text), APNOutputs/OEIS/oeis_A028859_conjecture_1.lean:43 (same statement text; different proof or body), APNOutputs/OEIS/oeis_a211417_conjecture_specific.lean:44 (same statement text; different proof or body), APNOutputs/OEIS/oeis_a237271_conjecture_2.lean:49 (same statement text; different proof or body), APNOutputs/OEIS/oeis_a300997_finite_difference_is_one_or_two.lean:46 (different declaration text), APNOutputs/OEIS/oeis_a363102_conjecture_1.lean:56 (same statement text; different proof or body), APNOutputs/OEIS/oeis_a368692_conjecture_integrality.lean:47 (same statement text; different proof or body). Qualify references as a@path.
```
def a (n : ℕ) : ℕ := (2 ^ (2 ^ n + 2) + 3).minFac
```
def covered_by_C1 An index k is covered by Conjecture 1 if k = 10m + 2 for some m >= 0, predicting a(k)=67 line 46 source
Source documentation
An index k is covered by Conjecture 1 if k = 10m + 2 for some m >= 0, predicting a(k)=67.

no axioms what this means
Statement uses: Nat
Proof uses: Exists, Eq, HAdd.hAdd, HMul.hMul, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
def covered_by_C1 (k : ℕ) : Prop := ∃ m : ℕ, k = 10 * m + 2
```
def covered_by_C2 An index k is covered by Conjecture 2 if k = 36m + 16 for some m >= 0, and m is not 1 mod 5, predicting a(k)=271 line 49 source
Source documentation
An index k is covered by Conjecture 2 if k = 36m + 16 for some m >= 0, and m is not 1 mod 5, predicting a(k)=271.

no axioms what this means
Statement uses: Nat
Proof uses: Exists, And, Eq, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Ne, HMod.hMod
7 instances, coercions and auxiliary constants left out.
```
def covered_by_C2 (k : ℕ) : Prop := ∃ m : ℕ, k = 36 * m + 16 ∧ m % 5 ≠ 1
```
def covered_by_C3 An index k is covered by Conjecture 3 if k = 84m + 22 for some m >= 0, and m is not 0 mod 5, predicting a(k)=523 line 52 source
Source documentation
An index k is covered by Conjecture 3 if k = 84m + 22 for some m >= 0, and m is not 0 mod 5, predicting a(k)=523.

no axioms what this means
Statement uses: Nat
Proof uses: Exists, And, Eq, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Ne, HMod.hMod
7 instances, coercions and auxiliary constants left out.
```
def covered_by_C3 (k : ℕ) : Prop := ∃ m : ℕ, k = 84 * m + 22 ∧ m % 5 ≠ 0
…
```
lemma mod_1399_step1 line 89 source
standard axioms: propext what this means
Statement uses: Nat.ModEq, OfNat.ofNat, Nat, HPow.hPow
Proof uses: of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma mod_1399_step2 line 91 source
standard axioms: propext what this means
Statement uses: Nat, Nat.ModEq, OfNat.ofNat, HPow.hPow
Proof uses: Nat.ModEq.pow, mod_1399_step1, Eq.mp, congrArg, one_pow
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma mod_1399_step3 line 96 source
standard axioms: propext what this means
Statement uses: Nat, Nat.ModEq, OfNat.ofNat, HPow.hPow, HAdd.hAdd, HMul.hMul
Proof uses: Eq, Eq.mpr, id, congrArg, pow_add, pow_mul, Eq.refl, Nat.ModEq.mul_right, mod_1399_step2, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Nat.ModEq.trans
20 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma mod_1399_step4 line 105 source
standard axioms: propext what this means
Statement uses: Nat.ModEq, OfNat.ofNat, Nat, HPow.hPow
Proof uses: of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma exp_ge_204 line 107 source
standard axioms: propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HPow.hPow, HAdd.hAdd, HMul.hMul
Proof uses: Trans.trans, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Nat.pow_le_pow_right, GT.gt, Nat.le_add_left
22 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma modEq_to_eq line 111 source
standard axioms: propext what this means
Statement uses: Nat, Nat.ModEq, LE.le, LT.lt, Exists, Eq, HAdd.hAdd, HMul.hMul
Proof uses: Exists.intro, HDiv.hDiv, HMod.hMod, Nat.mod_eq_of_lt, Nat.div_add_mod, Eq.symm, Eq.mp, congrArg
16 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma mod_1399_step5 line 120 source
standard axioms: propext what this means
Statement uses: Nat, Nat.ModEq, OfNat.ofNat, HPow.hPow, HAdd.hAdd, HMul.hMul
Proof uses: Exists, Eq, modEq_to_eq, mod_1399_step3, exp_ge_204, of_decide_eq_true, LT.lt, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.mpr, congrArg, pow_add, pow_mul, Nat.ModEq.pow, mod_1399_step4, Nat.ModEq.mul_right, Eq.mp and 2 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma mod_1399_step6 line 133 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.ModEq, OfNat.ofNat, HAdd.hAdd, HPow.hPow, HMul.hMul
Proof uses: Eq, Eq.mpr, id, congrArg, pow_add, Eq.refl, Nat.ModEq.mul_right, mod_1399_step5, Nat.ModEq.add_right, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Nat.ModEq.trans
20 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma divides_1399 line 145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Dvd.dvd, OfNat.ofNat, HAdd.hAdd, HPow.hPow, HMul.hMul
Proof uses: Nat.ModEq, mod_1399_step6, Nat.dvd_of_mod_eq_zero
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def pow_mod line 149 source
no axioms what this means
Statement uses: Nat
Proof uses: Id.run, OfNat.ofNat, HMod.hMod, Bind.bind, Id, MProd, ForIn.forIn, Lean.Loop, Unit, Lean.Loop.mk, MProd.mk, MProd.fst, MProd.snd, ite, ForInStep, GT.gt, PUnit, HMul.hMul, HDiv.hDiv, Pure.pure and 8 more
17 instances, coercions and auxiliary constants left out.
def is_prime line 159 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Bool
Proof uses: Id.run, PUnit, Id, Bind.bind, MProd, Option, ForIn.forIn, Std.Range, inferInstance, Membership, Std.Range.mk, OfNat.ofNat, Nat.zero_lt_one, MProd.mk, Option.none, PUnit.unit, MProd.snd, ite, ForInStep, Eq and 12 more
15 instances, coercions and auxiliary constants left out.
def bad_for_even_k line 165 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Bool
Proof uses: Id.run, PUnit, Id, OfNat.ofNat, Bind.bind, MProd, Option, ForIn.forIn, Std.Range, inferInstance, Membership, Std.Range.mk, HAdd.hAdd, Nat.zero_lt_one, MProd.mk, Option.none, MProd.snd, HMod.hMod, HMul.hMul, HSub.hSub and 15 more
19 instances, coercions and auxiliary constants left out.
lemma zmod_pow_mod line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Eq, ZMod, HPow.hPow, HMod.hMod, HSub.hSub
Proof uses: pow_eq_pow_mod, ZMod.pow_card_sub_one_eq_one, HEq, Function.comp, Dvd.dvd, LT.lt, Nat.eq_zero_of_dvd_of_lt, Iff.mp, outParam, CharP.cast_eq_zero_iff, False, False.elim, Eq.refl, noConfusion_of_Nat, Nat.ctorIdx, HEq.refl
56 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma not_C1_implies line 182 source
standard axioms: propext what this means
Statement uses: Nat, Not, covered_by_C1, Ne, HMod.hMod, OfNat.ofNat
Proof uses: Eq, Exists.intro, HAdd.hAdd, HMul.hMul, HDiv.hDiv, Nat.div_add_mod, Eq.symm, Eq.mp, congrArg
12 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma not_C1_C2_implies line 190 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, covered_by_C1, covered_by_C2, Ne, HMod.hMod, OfNat.ofNat
Proof uses: Eq, HAdd.hAdd, HMul.hMul, HDiv.hDiv, Nat.div_add_mod, Eq.symm, Eq.mp, congrArg, dite, False, Exists.intro, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Neg.neg, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr and 61 more
88 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma not_C1_C3_implies line 207 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, covered_by_C1, covered_by_C3, Ne, HMod.hMod, OfNat.ofNat
Proof uses: Eq, HAdd.hAdd, HMul.hMul, HDiv.hDiv, Nat.div_add_mod, Eq.symm, Eq.mp, congrArg, dite, False, Exists.intro, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Neg.neg, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr and 61 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma p_mod_base line 224 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, GE.ge, Nat.ModEq, HPow.hPow, OfNat.ofNat, HAdd.hAdd
Proof uses: Eq, HMul.hMul, HSub.hSub, Eq.mpr, id, congrArg, Eq.symm, pow_add, Decidable.byContradiction, Not, Eq.refl, Nat.ModEq.mul_left
24 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma p_67_mod line 236 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Nat.ModEq, HPow.hPow, HAdd.hAdd
Proof uses: p_mod_base, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma p_271_mod line 239 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Nat.ModEq, HPow.hPow, HAdd.hAdd
Proof uses: p_mod_base, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma p_523_mod line 242 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Nat.ModEq, HPow.hPow, HAdd.hAdd
Proof uses: p_mod_base, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma period_mod_ind line 245 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, Nat.ModEq, HPow.hPow, OfNat.ofNat, HAdd.hAdd, HMul.hMul
Proof uses: Nat.recAux, Eq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.mul_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.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, Mathlib.Tactic.Ring.zero_mul and 19 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma p_mod_all_generic line 262 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, GT.gt, OfNat.ofNat, Nat.ModEq, HPow.hPow, HAdd.hAdd, HMod.hMod
Proof uses: dite, LT.lt, Eq, Nat.mod_eq_of_lt, Eq.mpr, id, congrArg, Nat.ModEq.symm, Not, Decidable.byContradiction, HMul.hMul, HDiv.hDiv, Eq.symm, Nat.mod_add_div, HSub.hSub, Nat.div_pos, mul_comm, Eq.refl, period_mod_ind
36 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma p_271_mod_all line 281 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Nat.ModEq, HPow.hPow, HAdd.hAdd, HMod.hMod
Proof uses: p_mod_all_generic, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, GT.gt, p_271_mod, Decidable.byContradiction, Not
15 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma p_523_mod_all line 284 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Nat.ModEq, HPow.hPow, HAdd.hAdd, HMod.hMod
Proof uses: p_mod_all_generic, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, GT.gt, p_523_mod, Decidable.byContradiction, Not
15 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma p_not_div_67 line 287 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Ne, HMod.hMod, Eq, Not, Dvd.dvd, HAdd.hAdd, HPow.hPow
Proof uses: Eq.mpr, HMul.hMul, HDiv.hDiv, id, congrArg, Eq.symm, Nat.mod_add_div, Eq.trans, congr, Monoid, Eq.rec, pow_add, pow_mul, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_pow, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.trans, Nat.pow and 32 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
def sq_mod line 295 source
no axioms what this means
Statement uses: Nat
Proof uses: sq_mod.match_1, Unit, OfNat.ofNat, HMod.hMod, Nat.succ, HMul.hMul
7 instances, coercions and auxiliary constants left out.
lemma sq_mod_eq line 299 source
standard axioms: propext what this means
Statement uses: Nat, Eq, sq_mod, HMod.hMod, HPow.hPow, OfNat.ofNat
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrArg, pow_zero, pow_one, eq_self, Eq.mpr, HAdd.hAdd, HMul.hMul, id, Nat.ModEq.pow, Nat.mod_modEq, Eq.symm, pow_two, pow_mul, pow_succ', mul_comm, Eq.refl
26 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma sq_mod_add line 312 source
standard axioms: propext what this means
Statement uses: Nat, Eq, sq_mod, HAdd.hAdd
Proof uses: Eq.mpr, HMod.hMod, HPow.hPow, OfNat.ofNat, id, congrArg, sq_mod_eq, Nat.ModEq.pow, Nat.mod_modEq, HMul.hMul, Eq.symm, pow_mul, pow_add, Eq.refl
15 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def bad_for_k line 318 source
no axioms what this means
Statement uses: Nat, Bool
Proof uses: BEq.beq, HMod.hMod, HAdd.hAdd, HMul.hMul, sq_mod, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.
def check_271_all line 321 source
no axioms what this means
Statement uses: Bool
Proof uses: List.all, Nat, List.range, OfNat.ofNat, ite, Eq, Bool.or, BEq.beq, HMod.hMod, Bool.true, bad_for_k, HAdd.hAdd, Bool.false
8 instances, coercions and auxiliary constants left out.
def check_523_all line 327 source
no axioms what this means
Statement uses: Bool
Proof uses: List.all, Nat, List.range, OfNat.ofNat, ite, Eq, Bool.or, BEq.beq, HMod.hMod, Bool.true, bad_for_k, HAdd.hAdd, Bool.false
8 instances, coercions and auxiliary constants left out.
lemma bad_for_k_iff line 333 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, Eq, Bool, bad_for_k, Bool.true, Dvd.dvd, HAdd.hAdd, HPow.hPow, OfNat.ofNat
Proof uses: id, Eq.mpr, BEq.beq, HMod.hMod, HMul.hMul, sq_mod, congrArg, sq_mod_eq, propext, beq_iff_eq, pow_add, Eq.refl, Nat.ModEq, Nat.ModEq.mul_right, Nat.ModEq.symm, Nat.mod_modEq, Nat.ModEq.add_right, Eq.symm, Iff.symm, Nat.dvd_iff_mod_eq_zero
21 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma bad_for_k_periodic line 348 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Nat.ModEq, HSub.hSub, HPow.hPow, Eq, Bool, bad_for_k
Proof uses: id, Eq.mpr, BEq.beq, HMod.hMod, HAdd.hAdd, HMul.hMul, sq_mod, congrArg, sq_mod_eq, ZMod, zmod_pow_mod, Eq.refl, Trans.trans, ZMod.val, Eq.symm, ZMod.val_natCast, Nat.cast_pow
44 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma check_271_all_eq line 365 source
no axioms what this means
Statement uses: Eq, Bool, check_271_all, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma check_523_all_eq line 368 source
no axioms what this means
Statement uses: Eq, Bool, check_523_all, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma p_not_div_271 line 370 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Ne, HMod.hMod, Eq, Not, Dvd.dvd, HAdd.hAdd, HPow.hPow
Proof uses: Bool, bad_for_k, Bool.true, Iff.mpr, bad_for_k_iff, Fact, Nat.Prime, Fact.mk, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.minFacHelper_2, Mathlib.Meta.NormNum.not_prime_mul_of_ble, Bool.false, Mathlib.Meta.NormNum.minFacHelper_3, Mathlib.Meta.NormNum.minFacHelper_0, bad_for_k_periodic, of_decide_eq_true and 34 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma p_not_div_523 line 398 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Ne, HMod.hMod, Eq, Not, Dvd.dvd, HAdd.hAdd, HPow.hPow
Proof uses: Bool, bad_for_k, Bool.true, Iff.mpr, bad_for_k_iff, Fact, Nat.Prime, Fact.mk, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.minFacHelper_2, Mathlib.Meta.NormNum.not_prime_mul_of_ble, Bool.false, Mathlib.Meta.NormNum.minFacHelper_3, Mathlib.Meta.NormNum.minFacHelper_0, bad_for_k_periodic, of_decide_eq_true and 34 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
def pow_mod_loop line 426 source
no axioms what this means
Statement uses: Nat
Proof uses: sq_mod.match_1, Unit, OfNat.ofNat, HMod.hMod, Nat.succ, HMul.hMul
7 instances, coercions and auxiliary constants left out.
def pow_mod_rec line 431 source
no axioms what this means
Statement uses: Nat
Proof uses: pow_mod_loop, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
lemma pow_mod_loop_eq line 434 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, pow_mod_loop, HMod.hMod, HMul.hMul, HPow.hPow
Proof uses: Nat.recAux, Eq.mpr, OfNat.ofNat, id, congrArg, sq_mod.match_1, Unit, pow_mod_loop.eq_def, pow_zero, mul_one, Eq.refl, HAdd.hAdd, Nat.ModEq.mul_right, Nat.mod_modEq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_mul and 14 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma pow_mod_rec_eq line 449 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, pow_mod_rec, HMod.hMod, HPow.hPow
Proof uses: id, Eq.mpr, pow_mod_loop, OfNat.ofNat, HMul.hMul, congrArg, pow_mod_loop_eq, one_mul, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def next_y line 454 source
no axioms what this means
Statement uses: Nat
Proof uses: HMod.hMod, HMul.hMul
4 instances, coercions and auxiliary constants left out.
lemma next_y_eq line 458 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, next_y, HMod.hMod, HPow.hPow, OfNat.ofNat
Proof uses: id, Nat.ModEq, HMul.hMul, Nat.mod_modEq, Nat.ModEq.mul, Eq.mpr, congrArg, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_mul, Mathlib.Tactic.Ring.mul_add, Mathlib.Tactic.Ring.mul_pp_pf_overlap, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_add, Eq.refl, Mathlib.Meta.NormNum.IsNat.of_raw and 13 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def sq_mod_iter line 467 source
no axioms what this means
Statement uses: Nat
Proof uses: sq_mod.match_1, Unit, OfNat.ofNat, Nat.succ, next_y
3 instances, coercions and auxiliary constants left out.
def check_p_fast_loop line 471 source
no axioms what this means
Statement uses: Nat, Bool
Proof uses: sq_mod.match_1, Unit, OfNat.ofNat, Bool.true, Nat.succ, ite, Eq, BEq.beq, HMod.hMod, HAdd.hAdd, HMul.hMul, Bool.false, next_y
12 instances, coercions and auxiliary constants left out.
lemma check_p_fast_loop_sound line 478 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Bool, check_p_fast_loop, Bool.true, LT.lt, Ne, HMod.hMod, HAdd.hAdd, HMul.hMul, OfNat.ofNat, sq_mod_iter
Proof uses: Nat.recAux, BEq.beq, Decidable, ite, Bool.false, next_y, Not, Eq.mpr, id, implies_congr, congrArg, if_neg, Eq.refl, Iff.mpr, beq_iff_eq, absurd, False, Eq.mp, Nat.casesAuxOn, sq_mod.match_1 and 10 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma sq_mod_iter_eq line 509 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMod.hMod, sq_mod_iter, HPow.hPow, OfNat.ofNat, HMul.hMul
Proof uses: Nat.recAux, Eq.mpr, id, congrArg, sq_mod.match_1, Unit, next_y, sq_mod_iter.eq_def, rfl, pow_one, Nat.mod_mod, HAdd.hAdd, next_y_eq, Nat.ModEq, Nat.ModEq.pow, Nat.mod_modEq, Eq.mp, Eq.symm, pow_mul, pow_add and 5 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma sq_mod_iter_eval line 540 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMod.hMod, sq_mod_iter, sq_mod, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: Eq.mpr, HPow.hPow, id, congrArg, sq_mod_eq, sq_mod_iter_eq, Eq.symm, pow_mul, pow_add, Eq.refl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma bad_for_k_from_loop line 550 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Bool, check_p_fast_loop, sq_mod, OfNat.ofNat, Bool.true, LT.lt, bad_for_k, HAdd.hAdd, HMul.hMul, Bool.false
Proof uses: id, Ne, HMod.hMod, sq_mod_iter, check_p_fast_loop_sound, Eq.mpr, congrArg, sq_mod_iter_eval, Eq.refl, Nat.ModEq, Nat.ModEq.mul_right, Nat.mod_modEq, Nat.ModEq.add_right, BEq.beq, mul_comm, beq_false_of_ne
22 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
def check_p_fast_with_P line 570 source
no axioms what this means
Statement uses: Nat, Bool
Proof uses: ite, Eq, BEq.beq, OfNat.ofNat, Bool.true, Bool.false, Bool.and, HMod.hMod, pow_mod_rec, HAdd.hAdd, HSub.hSub, check_p_fast_loop, sq_mod, HDiv.hDiv
12 instances, coercions and auxiliary constants left out.
def get_period_loop line 577 source
no axioms what this means
Statement uses: Nat
Proof uses: sq_mod.match_1, Unit, OfNat.ofNat, Nat.succ, HMod.hMod, HMul.hMul, ite, Eq, Bool, BEq.beq, Bool.true, HAdd.hAdd
12 instances, coercions and auxiliary constants left out.
def get_period line 585 source
no axioms what this means
Statement uses: Nat
Proof uses: HSub.hSub, OfNat.ofNat, pow_mod_rec, get_period_loop
3 instances, coercions and auxiliary constants left out.
def is_prime_loop line 590 source
no axioms what this means
Statement uses: Nat, Bool
Proof uses: sq_mod.match_1, Unit, OfNat.ofNat, Bool.true, Nat.succ, ite, GT.gt, HMul.hMul, Eq, BEq.beq, HMod.hMod, Bool.false, HAdd.hAdd
14 instances, coercions and auxiliary constants left out.
def is_prime_fast line 598 source
no axioms what this means
Statement uses: Nat, Bool
Proof uses: ite, LT.lt, OfNat.ofNat, Bool.false, is_prime_loop
3 instances, coercions and auxiliary constants left out.
def check_p_fast line 602 source
no axioms what this means
Statement uses: Nat, Bool
Proof uses: ite, Eq, Bool.or, BEq.beq, OfNat.ofNat, Bool.true, Bool.and, is_prime_fast, bne, check_p_fast_with_P, get_period
4 instances, coercions and auxiliary constants left out.
def check_chunk line 608 source
no axioms what this means
Statement uses: Nat, Bool
Proof uses: List.all, List.range, HSub.hSub, check_p_fast, HAdd.hAdd
4 instances, coercions and auxiliary constants left out.
lemma chunk1 line 613 source
no axioms what this means
Statement uses: Eq, Bool, check_chunk, OfNat.ofNat, Nat, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, 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 chunk2 line 616 source
no axioms what this means
Statement uses: Eq, Bool, check_chunk, OfNat.ofNat, Nat, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, 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 chunk3 line 619 source
no axioms what this means
Statement uses: Eq, Bool, check_chunk, OfNat.ofNat, Nat, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, 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 chunk4 line 622 source
no axioms what this means
Statement uses: Eq, Bool, check_chunk, OfNat.ofNat, Nat, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, 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 chunk5 line 625 source
no axioms what this means
Statement uses: Eq, Bool, check_chunk, OfNat.ofNat, Nat, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, 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 chunk6 line 628 source
no axioms what this means
Statement uses: Eq, Bool, check_chunk, OfNat.ofNat, Nat, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, 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 chunk7 line 631 source
no axioms what this means
Statement uses: Eq, Bool, check_chunk, OfNat.ofNat, Nat, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, 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 test_chunk line 633 source
no axioms what this means
Statement uses: Eq, Bool, check_chunk, OfNat.ofNat, Nat, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, 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 check_chunk_all line 635 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Bool, check_p_fast, Bool.true
Proof uses: Or, And, LE.le, Decidable.byContradiction, Not, check_chunk, chunk1, HAdd.hAdd, Iff.mp, List.all, List.range, HSub.hSub, Membership.mem, List, List.all_eq_true, Iff.mpr, List.mem_range, Eq.rec, chunk2, chunk3 and 4 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 58 steps
Open to load the checked before-and-after goal states.
lemma check_p_fast_eval line 674 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Eq, Bool, is_prime_fast, Bool.true, Ne, check_p_fast, check_p_fast_with_P, get_period
Proof uses: id, Bool.or, BEq.beq, Bool.false, of_eq_true, Eq.trans, And, True, congr, congrArg, Not, False, eq_false, not_false_eq_true, and_self, Bool.and, bne, Iff.mpr, bne_iff_ne, Bool.and_self and 5 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma p_fast_extract line 688 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Bool, check_p_fast, Bool.true, GE.ge, OfNat.ofNat, is_prime_fast, Ne, Exists, And, HMod.hMod, Nat.ModEq, HSub.hSub, HPow.hPow, HAdd.hAdd, GT.gt, LT.lt, HDiv.hDiv, bad_for_k and 2 more
Proof uses: check_p_fast_with_P, get_period, check_p_fast_eval, Eq.mp, congrArg, dite, BEq.beq, False.elim, False, ite, Bool.and, pow_mod_rec, check_p_fast_loop, sq_mod, Eq.refl, Not, eq_false_of_ne_true, Exists.intro, Iff.mp, beq_iff_eq and 8 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 47 steps
Open to load the checked before-and-after goal states.
lemma generic_period line 729 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Nat.ModEq, HPow.hPow, OfNat.ofNat, HAdd.hAdd, GE.ge
Proof uses: Eq, HSub.hSub, Eq.symm, Nat.add_sub_cancel', Eq.mpr, id, congrArg, Decidable.byContradiction, Not, HMul.hMul, pow_add, Nat.ModEq.mul_right
20 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma period_mod_ind_offset line 742 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, Nat.ModEq, HPow.hPow, OfNat.ofNat, HAdd.hAdd, HMul.hMul
Proof uses: Nat.recAux, Eq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_pf_add_lt, Mathlib.Tactic.Ring.add_pf_zero_add, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.zero_mul, Mathlib.Tactic.Ring.add_pf_add_zero, Eq.mpr, id, congrArg, Nat.ModEq.refl, Mathlib.Tactic.Ring.cast_pos and 10 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma p_mod_offset line 756 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, Nat.ModEq, HPow.hPow, OfNat.ofNat, HAdd.hAdd, HMod.hMod
Proof uses: Eq, HMul.hMul, HDiv.hDiv, Nat.mod_add_div, Eq.mpr, id, congrArg, mul_comm, Eq.symm, Decidable.byContradiction, Not, period_mod_ind_offset
29 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma is_prime_loop_of_prime line 769 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, GE.ge, OfNat.ofNat, Eq, Bool, is_prime_loop, Bool.true
Proof uses: id, Nat.rec, LE.le, sq_mod.match_1, Unit, Nat.succ, ite, GT.gt, HMul.hMul, BEq.beq, HMod.hMod, Bool.false, HAdd.hAdd, Dvd.dvd, Or, And, Nat.zero, Eq.mp, propext, Nat.prime_def and 85 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma is_prime_fast_of_prime line 775 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, LT.lt, OfNat.ofNat, Eq, Bool, is_prime_fast, Bool.true
Proof uses: id, GE.ge, Nat.Prime.two_le, Not, Eq.mpr, ite, Bool.false, is_prime_loop, congrArg, ite_cond_eq_false, eq_false, is_prime_loop_of_prime, Decidable.byContradiction
10 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma p_not_div_other line 782 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, LT.lt, OfNat.ofNat, Ne, GE.ge, Eq, HMod.hMod, Not, Dvd.dvd, HAdd.hAdd, HPow.hPow
Proof uses: GT.gt, Decidable.byContradiction, Nat.Prime.two_le, Eq.mp, LE.le, HMul.hMul, Eq.mpr, id, congrArg, pow_succ, mul_comm, Eq.refl, Nat.mod_eq_zero_of_dvd, Bool, bad_for_k, Bool.true, Iff.mpr, bad_for_k_iff, check_p_fast, check_chunk_all and 29 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 59 steps
Open to load the checked before-and-after goal states.
theorem target_theorem_0 line 841 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, And, Not, covered_by_C1, HAdd.hAdd, HMul.hMul, OfNat.ofNat, covered_by_C2, covered_by_C3, Eq, a
Proof uses: rfl, HMod.hMod, Decidable.byContradiction, GE.ge, And.left, And.right, Ne, not_C1_implies, not_C1_C2_implies, not_C1_C3_implies, Dvd.dvd, HPow.hPow, p_not_div_67, p_not_div_271, p_not_div_523, divides_1399, Nat.Prime, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 71 more
99 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_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: 47 steps
Open to load the checked before-and-after goal states.