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

57 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

FormalConjectures.Util.ProblemImports

def A051293 A051293: Number of nonempty subsets of $\{1, 2, 3, \dots, n\}$ whose elements have an integer average line 59 source
Source documentation
A051293: Number of nonempty subsets of $\{1, 2, 3, \dots, n\}$ whose elements have an integer average.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.card, Finset, Finset.filter, And, Finset.Nonempty, Dvd.dvd, Finset.sum, id, Finset.powerset, Finset.Icc, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.
```
def A051293 (n : ℕ) : ℕ :=
…
```
def a_real line 65 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: A051293
2 instances, coercions and auxiliary constants left out.
def I_sum line 102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: Finset.sum, Finset.Icc, OfNat.ofNat, HMul.hMul, HDiv.hDiv, Nat.choose
13 instances, coercions and auxiliary constants left out.
def S_sum line 104 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: Finset.sum, Finset.Icc, OfNat.ofNat, HDiv.hDiv, HPow.hPow
14 instances, coercions and auxiliary constants left out.
def H_sum line 106 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: Finset.sum, Finset.Icc, OfNat.ofNat, HDiv.hDiv
11 instances, coercions and auxiliary constants left out.
lemma I_sum_eq line 108 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, I_sum, HSub.hSub, S_sum, H_sum
Proof uses: id, Nat.rec, Finset.sum, Finset.Icc, OfNat.ofNat, HMul.hMul, HDiv.hDiv, Nat.choose, HPow.hPow, Eq.symm, Nat.zero, sub_self, Eq.trans, Nat.succ, HAdd.hAdd, Finset.sum_Icc_succ_top, Nat.succ_pos, cast, congr, congrArg and 61 more
118 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
def M0 line 115 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
def P0 line 116 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: OfNat.ofNat
2 instances, coercions and auxiliary constants left out.
def M1 line 118 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
def P1 line 119 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HAdd.hAdd, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean:259 (different declaration text). Qualify references as P1@path.
def M2 line 121 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
def P2 line 122 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul
12 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean:599 (different declaration text). Qualify references as P2@path.
def M3 line 124 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
def P3 line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul
13 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean:1549 (different declaration text). Qualify references as P3@path.
def M4 line 127 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
def P4 line 128 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul
14 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_4.lean:977 (different declaration text). Qualify references as P4@path.
def M5 line 130 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
def P5 line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul
15 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean:2132 (different declaration text). Qualify references as P5@path.
lemma s0_eq line 133 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, Finset.sum, Finset.range, HDiv.hDiv, OfNat.ofNat, HPow.hPow, HSub.hSub, M0, HMul.hMul, P0
Proof uses: Eq.mpr, Mathlib.Meta.NormNum.instAtLeastTwo, Neg.neg, id, Eq.trans, congr, congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Mathlib.Meta.NormNum.IsNNRat.to_eq, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, Inv.inv, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Meta.NormNum.isNNRat_inv_pos, Nat.mul and 72 more
99 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma s1_eq line 135 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, Finset.sum, Finset.range, HDiv.hDiv, HPow.hPow, OfNat.ofNat, HSub.hSub, M1, HMul.hMul, P1
Proof uses: Eq.mpr, Inv.inv, HAdd.hAdd, id, congr, congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Eq.trans, div_eq_mul_inv, Nat.recAux, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.cast_zero, Eq.rec, Finset.empty, Mathlib.Meta.NormNum.IsNat, Mathlib.Meta.NormNum.Finset.sum_empty, Eq.symm and 70 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma s2_eq line 137 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, Finset.sum, Finset.range, HDiv.hDiv, HPow.hPow, OfNat.ofNat, HSub.hSub, M2, HMul.hMul, P2
Proof uses: id, symm, HAdd.hAdd, Eq.trans, Eq.mpr, congrArg, M2.eq_1, Eq.refl, Nat.recAux, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.sub_congr, Nat.rawCast, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.div_congr, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.pow_congr, Mathlib.Tactic.Ring.instCommSemiringNat and 81 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma s3_eq line 139 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, Finset.sum, Finset.range, HDiv.hDiv, HPow.hPow, OfNat.ofNat, HSub.hSub, M3, HMul.hMul, P3
Proof uses: Eq.mpr, HAdd.hAdd, id, congrArg, P3.eq_1, M3.eq_1, Finset.sum_range_induction, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.isInt_sub, Int.ofNat, Eq.refl, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.IsNNRat.to_isNat, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Inv.inv and 74 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma s4_eq line 142 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, Finset.sum, Finset.range, HDiv.hDiv, HPow.hPow, OfNat.ofNat, HSub.hSub, M4, HMul.hMul, P4
Proof uses: id, Eq.symm, HAdd.hAdd, Nat.recAux, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.sub_congr, Nat.rawCast, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.div_congr, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.pow_congr, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Tactic.Ring.pow_add, Mathlib.Tactic.Ring.zero_pow and 80 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma s5_eq line 145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, Finset.sum, Finset.range, HDiv.hDiv, HPow.hPow, OfNat.ofNat, HSub.hSub, M5, HMul.hMul, P5
Proof uses: Eq.mpr, Inv.inv, HAdd.hAdd, id, congr, congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Eq.trans, div_eq_mul_inv, Nat.recAux, of_eq_true, True, Mathlib.Meta.NormNum.IsNat.to_eq, Eq.rec, Finset.empty, Mathlib.Meta.NormNum.IsNat, Mathlib.Meta.NormNum.Finset.sum_empty and 88 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma frac_identity line 148 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Eq, Real, HDiv.hDiv, OfNat.ofNat, HSub.hSub, HAdd.hAdd, HPow.hPow, HMul.hMul
Proof uses: Eq.mpr, inferInstance, CommGroupWithZero, GroupWithZero, id, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq, Mathlib.Tactic.FieldSimp.NF.eval, List.nil, Prod, Int, Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk, Neg.neg, Eq.trans, congr_arg₂, rfl, Mathlib.Tactic.FieldSimp.NF.div_eq_eval, Mathlib.Tactic.FieldSimp.NF.one_eq_eval, Mathlib.Tactic.FieldSimp.subst_sub and 94 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma S_sum_expansion line 151 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Real, S_sum, HAdd.hAdd, HMul.hMul, HDiv.hDiv, HPow.hPow, Finset.sum, Finset.range, HSub.hSub
Proof uses: Eq.mpr, Finset.Icc, id, congrArg, Eq.trans, congr, Finset.mul_sum, Finset.sum_congr, Eq.refl, Finset, Membership.mem, mul_one_div, mul_div_mul_comm, Finset.Ico, Nat.succ, Finset.sum_Ico_eq_sub, Nat.succ_pos, Nat.rec, sub_self, Nat.zero and 158 more
172 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
def E_poly line 165 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HAdd.hAdd, HDiv.hDiv, HMul.hMul, OfNat.ofNat, P0, P1, HPow.hPow, Nat, P2, P3, P4, P5
14 instances, coercions and auxiliary constants left out.
lemma tendsto_pow_div_exp line 168 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Filter.Tendsto, Real, HDiv.hDiv, HPow.hPow, OfNat.ofNat, Filter.atTop, nhds
Proof uses: tendsto_pow_const_div_const_pow_of_one_lt, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.false
34 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma E_poly_limit line 171 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Tendsto, Nat, Real, HDiv.hDiv, E_poly, HPow.hPow, OfNat.ofNat, HAdd.hAdd, Filter.atTop, nhds
Proof uses: Eq.mpr, HMul.hMul, id, Eq, congrArg, funext, div_div_eq_mul_div, P0, P1, P2, P3, P4, P5, Inv.inv, Eq.trans, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Meta.NormNum.instAddMonoidWithOne', Mathlib.Tactic.Ring.div_congr, Mathlib.Tactic.Ring.mul_congr and 225 more
232 instances, coercions and auxiliary constants left out.

Tactic trace: 110 steps
Open to load the checked before-and-after goal states.
lemma R_n_limit line 198 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Tendsto, Nat, Real, Finset.sum, Finset.range, HDiv.hDiv, HPow.hPow, OfNat.ofNat, HMul.hMul, HAdd.hAdd, HSub.hSub, Filter.atTop, nhds
Proof uses: Summable, SummationFilter.unconditional, Summable.mul_left, summable_pow_mul_geometric_of_norm_lt_one, Eq.rec, Eq, LT.lt, one_half_lt_one, Norm.norm, Eq.symm, Real.norm_of_nonneg, LT.lt.le, one_half_pos, id, Eq.mp, tsum, ite, congrArg, funext, Eq.trans and 88 more
216 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma S_sum_diff_eq line 207 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Real, HDiv.hDiv, HSub.hSub, S_sum, HMul.hMul, HPow.hPow, HAdd.hAdd, Finset.sum, Finset.range, E_poly
Proof uses: S_sum_expansion, M0, P0, s0_eq, M1, P1, s1_eq, M2, P2, s2_eq, M3, P3, s3_eq, M4, P4, s4_eq, M5, P5, s5_eq, Eq.mpr and 137 more
158 instances, coercions and auxiliary constants left out.

Tactic trace: 52 steps
Open to load the checked before-and-after goal states.
lemma S_sum_asymp line 258 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Tendsto, Nat, Real, HDiv.hDiv, HSub.hSub, S_sum, HMul.hMul, HPow.hPow, OfNat.ofNat, HAdd.hAdd, Filter.atTop, nhds
Proof uses: Finset.sum, Finset.range, R_n_limit, E_poly, E_poly_limit, Filter.Tendsto.sub, Filter.EventuallyEq, Filter.mp_mem, setOf, LT.lt, Eq, Filter.eventually_gt_atTop, Filter.univ_mem', Membership.mem, Set, id, S_sum_diff_eq, Filter.Tendsto.congr', Filter.EventuallyEq.symm, Eq.mp and 2 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma H_sum_asymp line 268 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Tendsto, Nat, Real, HDiv.hDiv, H_sum, HPow.hPow, OfNat.ofNat, HAdd.hAdd, Filter.atTop, nhds
Proof uses: Eq.mpr, HMul.hMul, Finset.sum, Finset.Icc, id, Eq, congrArg, funext, Eq.trans, congr, pow_succ, div_div_eq_mul_div, squeeze_zero, HSMul.hSMul, Finset.card, Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos, mul_nonneg, Finset.sum_nonneg, Membership.mem, Finset and 87 more
139 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma I_asymp line 273 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Tendsto, Nat, Real, HDiv.hDiv, HSub.hSub, I_sum, HMul.hMul, HPow.hPow, OfNat.ofNat, HAdd.hAdd, Filter.atTop, nhds
Proof uses: S_sum, S_sum_asymp, H_sum, H_sum_asymp, Filter.Tendsto.sub, Eq, funext, Eq.mpr, id, congrArg, I_sum_eq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Inv.inv, NNRat.rawCast, Int.rawCast, Int.negOfNat, Rat.rawCast, Mathlib.Tactic.Ring.sub_congr and 63 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
def S_real line 285 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: Finset.card, Finset, Finset.filter, And, Eq, Dvd.dvd, Finset.sum, id, Finset.powerset, Finset.Icc, OfNat.ofNat
10 instances, coercions and auxiliary constants left out.
lemma a_real_eq_sum_S_real line 288 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, a_real, Finset.sum, Finset.Icc, OfNat.ofNat, S_real
Proof uses: id, Eq.mpr, A051293, Finset.card, Finset, Finset.filter, And, Dvd.dvd, Finset.powerset, ite, Finset.Nonempty, congr, congrArg, Eq.trans, Finset.filter.congr_simp, funext, Finset.sum_congr, Eq.refl, Membership.mem, Finset.card_filter and 29 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def P_poly S_real n k is the number of $k$-element subsets of $\{1, 2, \dots, n\}$ whose sum is divisible by $k$ line 302 source
Source documentation
S_real n k is the number of $k$-element subsets of $\{1, 2, \dots, n\}$ whose sum is divisible by $k$. By the roots of unity filter, this exact count can be written as: $S_{n,k} = \frac{1}{k} \sum_{j=0}^{k-1} \sum_{A \in \binom{n}{k}} \omega^{j \sum A}$. The main term $j=0$ yields exactly $\frac{1}{k} \binom{n}{k}$. For $j > 0$, the roots of unity evaluated over the subsets yield bounded periodic sums. The maximal magnitude of these periodic products is achieved when the order of the root is 2, which bounds the error term magnitude strictly by $2 \cdot 2^{n/2}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex, Polynomial
Proof uses: Finset.prod, Finset.Icc, OfNat.ofNat, HAdd.hAdd, HMul.hMul, RingHom, Polynomial.C, HPow.hPow, Polynomial.X
22 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/OEIS/oeis_228143_conjecture_1.lean:600 (different declaration text). Qualify references as P_poly@path.
```
noncomputable def P_poly (n : ℕ) (ω : ℂ) : Polynomial ℂ :=
…
```
lemma coeff_P_poly line 305 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex, Eq, Polynomial.coeff, P_poly, Finset.sum, Finset, Finset.filter, Finset.card, Finset.powerset, Finset.Icc, OfNat.ofNat, HPow.hPow, id
Proof uses: Eq.mpr, Finset.prod, Polynomial, HAdd.hAdd, HMul.hMul, RingHom, Polynomial.C, Polynomial.X, congr, congrArg, Finset.prod_congr, Eq.refl, Membership.mem, map_pow, Finset.sum_congr, Finset.powersetCard, Eq.trans, SDiff.sdiff, add_comm, Finset.prod_add and 23 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def sum_abs_coeff line 311 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Complex, Real
Proof uses: Finset.sum, Nat, Polynomial.support, Norm.norm, Polynomial.coeff
4 instances, coercions and auxiliary constants left out.
lemma coeff_le_sum_abs line 314 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Complex, Nat, LE.le, Real, Norm.norm, Polynomial.coeff, sum_abs_coeff
Proof uses: id, Or.elim, Eq, OfNat.ofNat, Not, Finset.sum, Polynomial.support, em, Eq.trans_le, Iff.mpr, norm_eq_zero, Finset.sum_nonneg, Membership.mem, Finset, norm_nonneg, Function.comp, Finset.single_le_sum, Ne, Polynomial.mem_support_iff
33 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma sum_abs_coeff_mul line 319 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Complex, LE.le, Real, sum_abs_coeff, HMul.hMul
Proof uses: Eq.mpr, Finset.sum, Nat, Polynomial.support, Norm.norm, Prod, Finset.HasAntidiagonal.antidiagonal, Polynomial.coeff, Prod.fst, Prod.snd, id, Eq, congr, congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Polynomial.coeff_mul, Finset.sum_mul_sum and 51 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma sum_abs_coeff_pow line 326 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Complex, Nat, LE.le, Real, sum_abs_coeff, HPow.hPow
Proof uses: id, LE.le.trans, Finset.sum, Polynomial.support, Norm.norm, Polynomial.coeff, Finset.range, HAdd.hAdd, Polynomial.natDegree, OfNat.ofNat, Finset.sum_le_sum_of_subset_of_nonneg, Polynomial.supp_subset_range_natDegree_succ, Membership.mem, Finset, Not, norm_nonneg, Nat.rec, of_eq_true, Nat.zero, Eq.trans and 109 more
154 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma sum_abs_coeff_one_add_C_X line 338 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, Real, Norm.norm, OfNat.ofNat, sum_abs_coeff, HAdd.hAdd, Polynomial, HMul.hMul, RingHom, Polynomial.C, Polynomial.X, Nat
Proof uses: Eq.mpr, Finset.sum, Polynomial.support, Polynomial.coeff, id, congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Eq.trans, Polynomial.coeff_add, Polynomial.coeff_C_mul, of_eq_true, True, Mathlib.Meta.NormNum.instAtLeastTwo, ite, Singleton.singleton, Insert.insert, Finset.ext and 52 more
129 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma sum_abs_coeff_one_sub_X_pow line 343 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Real, sum_abs_coeff, HSub.hSub, Polynomial, Complex, HPow.hPow, Neg.neg, Polynomial.X
Proof uses: Eq.mpr, Finset.sum, Polynomial.support, HAdd.hAdd, Norm.norm, ite, Polynomial.coeff, id, congrArg, Finset.sum_congr, Finset, sub_eq_add_neg, Membership.mem, Eq.trans, Polynomial.coeff_add, congr, Polynomial.coeff_one, Polynomial.coeff_neg, Even, Odd and 58 more
146 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma P_poly_split line 348 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Complex, IsPrimitiveRoot, Eq, Polynomial, P_poly, HMul.hMul, HPow.hPow, HSub.hSub, Neg.neg, Polynomial.X, HDiv.hDiv, Finset.prod, Finset.Ico, HAdd.hAdd, RingHom, Polynomial.C
Proof uses: id, Eq.trans, Eq.symm, Finset.prod_Ico_consecutive, of_eq_true, LE.le, Nat.Simproc.le_add_le, of_decide_eq_true, Eq.refl, Bool, Bool.true, True, Nat.Simproc.add_le_add_le, eq_true, Nat.div_mul_le_self, congr_arg, Finset.range, Finset.prod_Ico_eq_prod_range, Nat.rec, Eq.rec and 168 more
238 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
lemma sum_abs_coeff_prod_Ico line 368 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex, Eq, Real, Norm.norm, OfNat.ofNat, LE.le, sum_abs_coeff, Finset.prod, Polynomial, Finset.Ico, HAdd.hAdd, HMul.hMul, RingHom, Polynomial.C, HPow.hPow, Polynomial.X, HSub.hSub
Proof uses: Eq.mpr, Finset.sum, Polynomial.support, Finset, Finset.powerset, Polynomial.coeff, id, congrArg, Finset.sum_congr, Eq.trans, SDiff.sdiff, Finset.prod_congr, Eq.refl, Membership.mem, add_comm, Finset.prod_add, Finset.prod_const_one, mul_one, Polynomial.finset_sum_coeff, LE.le.trans and 52 more
151 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma P_poly_bound line 375 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex, LT.lt, OfNat.ofNat, IsPrimitiveRoot, Eq, Real, Norm.norm, LE.le, sum_abs_coeff, P_poly, HPow.hPow, HAdd.hAdd, HDiv.hDiv, HMod.hMod
Proof uses: Polynomial, HMul.hMul, HSub.hSub, Neg.neg, Polynomial.X, Finset.prod, Finset.Ico, RingHom, Polynomial.C, P_poly_split, Eq.mpr, id, congrArg, sum_abs_coeff_mul, Finset.sum, Polynomial.support, Finset.range, Nat.choose, Polynomial.coeff, Finset.sum_congr and 124 more
237 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
lemma S_real_eq_sum_roots line 398 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Complex, S_real, HMul.hMul, HDiv.hDiv, Finset.sum, Finset.range, Polynomial.coeff, P_poly, Complex.exp, Real.pi, Complex.I
Proof uses: IsPrimitiveRoot, Complex.isPrimitiveRoot_exp, False.elim, False, Eq.mp, Eq.trans, congrArg, Eq.mpr, Finset.card, Finset, Finset.filter, And, Dvd.dvd, Finset.powerset, Finset.Icc, Inv.inv, Finset.prod, Polynomial, HAdd.hAdd, HPow.hPow and 80 more
161 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma P_poly_one line 408 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Complex, Polynomial.coeff, P_poly, OfNat.ofNat, Nat.choose
Proof uses: id, of_eq_true, Finset.prod, Polynomial, Finset.Icc, HAdd.hAdd, HMul.hMul, RingHom, Polynomial.C, HPow.hPow, Polynomial.X, Eq.trans, True, congrArg, HSub.hSub, Finset.card, Finset.prod_congr, Eq.refl, Finset, Membership.mem and 9 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma bound_for_d line 413 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HAdd.hAdd, HDiv.hDiv, HMod.hMod
Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, HMul.hMul, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, HPow.hPow, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 68 more
118 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma root_norm_eq_one line 417 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, Norm.norm, Complex, Complex.exp, HDiv.hDiv, HMul.hMul, OfNat.ofNat, Real.pi, Complex.I
Proof uses: Eq.rec, Real.exp, Complex.re, of_eq_true, Eq.trans, True, congrArg, Complex.div_natCast_re, HSub.hSub, HAdd.hAdd, congr, MulZeroClass.mul_zero, sub_zero, MulZeroClass.zero_mul, add_zero, mul_one, sub_self, zero_div, Real.exp_zero, eq_self and 2 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma order_of_root line 421 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Exists, And, LE.le, IsPrimitiveRoot, Complex, Complex.exp, HDiv.hDiv, HMul.hMul, Real.pi, Complex.I
Proof uses: order_of_root.match_2, HAdd.hAdd, Eq.rec, Eq, HPow.hPow, by_contra, Not, absurd, Iff, Dvd.dvd, False, IsPrimitiveRoot.pow_eq_one_iff_dvd, Complex.isPrimitiveRoot_exp, order_of_root.match_1, Exists.intro, orderOf, And.intro, Ne.lt_of_le', Function.comp, Nat.eq_zero_of_dvd_of_lt and 19 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma S_real_approx_complex line 428 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, Real, Norm.norm, Complex, HSub.hSub, S_real, HMul.hMul, HDiv.hDiv, Nat.choose, HPow.hPow
Proof uses: Eq, Finset.sum, Finset.Ico, Polynomial.coeff, P_poly, Complex.exp, Real.pi, Complex.I, Eq.mpr, Finset.card, Finset, Finset.filter, And, Dvd.dvd, Finset.powerset, Finset.Icc, Inv.inv, Finset.range, Finset.prod, Polynomial and 206 more
260 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
lemma S_real_approx line 460 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, abs, HSub.hSub, S_real, HMul.hMul, HDiv.hDiv, OfNat.ofNat, Nat.choose, HPow.hPow
Proof uses: dite, Eq, Eq.mpr, Finset.card, Finset, Finset.filter, And, EmptyCollection.emptyCollection, Membership.mem, Finset.powerset, Finset.Icc, id, congrArg, Dvd.dvd, Finset.sum, Eq.trans, congr, Finset.filter.congr_simp, funext, Finset.sum_congr and 66 more
151 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma a_real_diff_bound line 472 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, abs, HSub.hSub, a_real, I_sum, HMul.hMul, HPow.hPow, OfNat.ofNat, HAdd.hAdd, HDiv.hDiv
Proof uses: Eq, Finset.sum, Finset.Icc, S_real, a_real_eq_sum_S_real, Nat.choose, rfl, LE.le.trans', Dist.dist, dist_sum_sum_le, Eq.le, congr_arg, congr_arg₂, Finset.sum_le_sum, Membership.mem, Finset, S_real_approx, Eq.trans, HSMul.hSMul, Finset.card and 110 more
141 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma a_real_diff line 492 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Tendsto, Nat, Real, HDiv.hDiv, HSub.hSub, a_real, I_sum, HPow.hPow, OfNat.ofNat, HAdd.hAdd, Filter.atTop, nhds
Proof uses: Filter.Eventually, LE.le, abs, HMul.hMul, Filter.mp_mem, setOf, LT.lt, Filter.eventually_gt_atTop, Filter.univ_mem', Membership.mem, Set, id, div_pos, pow_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble and 115 more
159 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
theorem target_theorem_0 OEIS A051293: a six-term asymptotic expansion for subsets with integer average line 517 source
L4DEL explanation
has an integer average if and only if the sum of its elements is divisible by its cardinality |S|.
— Human-written proof companion for OEIS A051293
a(n) is asymptotic to 2^(n+1)/n.
— Benoit Cloitre's OEIS A051293 comment (2002)
Let a(n) count the nonempty subsets of {1,…,n} whose arithmetic mean is an integer. After subtracting the displayed expansion through 541/n⁵, the error is little-o of 2^(n+1)/n⁶; the Lean limit states that normalized remainder tends to zero.
1. Replace “integer average” by divisibility of the subset sum by its cardinality.
2. A roots-of-unity filter counts the size-k subsets satisfying that divisibility condition and separates the principal term from oscillatory terms.
3. Summing and estimating those terms produces the coefficients 1, 1, 3, 13, 75, 541 and controls the normalized remainder.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written proof companion for OEIS A051293, Benoit Cloitre's OEIS A051293 comment (2002)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Tendsto, Nat, Real, HDiv.hDiv, HSub.hSub, a_real, HMul.hMul, HPow.hPow, OfNat.ofNat, HAdd.hAdd, Filter.atTop, nhds
Proof uses: I_sum, I_asymp, a_real_diff, Filter.Tendsto.add, Eq, funext, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Inv.inv, NNRat.rawCast, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.add_congr, Rat.rawCast, Mathlib.Tactic.Ring.div_congr, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.sub_pf, Mathlib.Tactic.Ring.neg_add and 65 more
106 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_363347_conjecture_2.lean:848 (different declaration text), APNOutputs/OEIS/oeis_372761_conjecture_2.lean:756 (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: 9 steps
Open to load the checked before-and-after goal states.
```
theorem target_theorem_0
  : Tendsto (fun n : ℕ => (a_real n - ((2 : ℝ) ^ (n + 1) / (n : ℝ)) * ((1 : ℝ) + 1 / (n : ℝ) + 3 / ((n : ℝ) ^ 2) + 13 / ((n : ℝ) ^ 3) + 75 / ((n : ℝ) ^ 4) + 541 / ((n : ℝ) ^ 5))) / (((2 : ℝ) ^ (n + 1)) / ((n : ℝ) ^ 6))) atTop (nhds 0) := by
…
```
Mentions: a_real