erdos_26.variants.tenenbaum.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

72 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

FormalConjectures.Util.ProblemImports

def Erdos26.IsThick A sequence of naturals $(a_i)$ is thick if their sum of reciprocals diverges: $$ \sum_i \frac{1}{a_i} = \infty $$ line 46 source
Source documentation
A sequence of naturals $(a_i)$ is thick if their sum of reciprocals diverges: $$ \sum_i \frac{1}{a_i} = \infty $$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Not, Summable, Real, HDiv.hDiv, OfNat.ofNat, SummationFilter.unconditional
11 instances, coercions and auxiliary constants left out.
```
def IsThick {ι : Type*} (A : ι → ℕ) : Prop := ¬Summable (fun i ↦ (1 : ℝ) / A i)
```
def Erdos26.MultiplesOf The set of multiples of a sequence $(a_i)$ is $\{na_i | n \in \mathbb{N}, i\}$ line 49 source
Source documentation
The set of multiples of a sequence $(a_i)$ is $\{na_i | n \in \mathbb{N}, i\}$.

no axioms what this means
Statement uses: Nat, Set
Proof uses: Set.range, Prod, Erdos26.MultiplesOf.match_1, HMul.hMul
2 instances, coercions and auxiliary constants left out.
```
def MultiplesOf {ι : Type*} (A : ι → ℕ) : Set ℕ := Set.range fun (n, i) ↦ n * A i
```
def Erdos26.IsBehrend A sequence of naturals $(a_i)$ is Behrend if almost all integers are a multiple of some $a_i$ line 53 source
Source documentation
A sequence of naturals $(a_i)$ is Behrend if almost all integers are a multiple of some $a_i$. In other words, if the set of multiples has natural density $1$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Set.HasDensity, Erdos26.MultiplesOf, OfNat.ofNat, Real, Set.univ
6 instances, coercions and auxiliary constants left out.
```
def IsBehrend {ι : Type*} (A : ι → ℕ) : Prop := (MultiplesOf A).HasDensity 1
```
Mentions: Erdos26.MultiplesOf
def Erdos26.IsWeaklyBehrend A sequence of naturals $(a_i)$ is weakly Behrend with respect to $\varepsilon \in \mathbb{R}$ if at least $1 - \varepsilon$ density of all numbers are a multiple of $A$ line 57 source
Source documentation
A sequence of naturals $(a_i)$ is weakly Behrend with respect to $\varepsilon \in \mathbb{R}$ if at least $1 - \varepsilon$ density of all numbers are a multiple of $A$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: LE.le, HSub.hSub, OfNat.ofNat, Set.lowerDensity, Erdos26.MultiplesOf, Set.univ
9 instances, coercions and auxiliary constants left out.
```
def IsWeaklyBehrend {ι : Type*} (A : ι → ℕ) (ε : ℝ) : Prop := 1 - ε ≤ (MultiplesOf A).lowerDensity
…
```
Mentions: Erdos26.MultiplesOf
lemma Erdos26.exists_x_P_ind line 94 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, And, GT.gt, OfNat.ofNat, LE.le, HPow.hPow, Nat.Prime, Dvd.dvd, HAdd.hAdd
Proof uses: Nat.recAux, Max.max, Nat.exists_infinite_primes, Nat.succ, LE.le.trans_lt, le_sup_left, le_sup_right, Exists.intro, LT.lt.pos, And.intro, Eq, Decidable.byContradiction, Not, dvd_rfl, of_eq_true, Eq.trans, True, congrArg, add_zero, Eq.symm and 54 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 70 steps
Open to load the checked before-and-after goal states.
def Erdos26.sum_ap line 145 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, HAdd.hAdd, HMul.hMul
15 instances, coercions and auxiliary constants left out.
lemma Erdos26.sum_ap_zero line 147 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, Erdos26.sum_ap, OfNat.ofNat
Proof uses: id, of_eq_true, Finset.sum, Finset.Icc, HDiv.hDiv, HAdd.hAdd, HMul.hMul, Eq.trans, EmptyCollection.emptyCollection, Finset, Inv.inv, True, congrArg, Finset.sum_congr, Finset.Icc_eq_empty_of_lt, LT.lt, Membership.mem, one_div, eq_self
36 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.sum_ap_succ line 151 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, Erdos26.sum_ap, HAdd.hAdd, OfNat.ofNat, HDiv.hDiv, HMul.hMul
Proof uses: id, of_eq_true, Finset.sum, Finset.Icc, Eq.trans, True, congrArg, Finset.sum_Icc_succ_top, LE.le, Nat.Simproc.le_add_le, of_decide_eq_true, Eq.refl, Bool, Bool.true, Nat.cast_add, Nat.cast_one, eq_self
43 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.exists_L_ge line 155 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, Exists, GE.ge, Real, Erdos26.sum_ap, HDiv.hDiv
Proof uses: id, dite, LE.le, Star.star, List.foldr, HAdd.hAdd, List.map, HMul.hMul, List.range', HSub.hSub, Summable, SummationFilter.unconditional, absurd, Norm.norm, Exists.intro, LE.le.trans, Eq.mpr, Eq, congrArg, Real.norm_of_nonneg and 126 more
180 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.exists_L_sum line 162 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, Exists, And, LE.le, Real, HDiv.hDiv, Erdos26.sum_ap
Proof uses: GE.ge, Erdos26.exists_L_ge, Nat.find, Nat.find_spec, Decidable.byContradiction, Not, Eq, Eq.mp, Trans.trans, Eq.mpr, id, congrArg, Eq.refl, False.elim, False, eq_false, Mathlib.Meta.NormNum.isRat_le_false, Int.ofNat, Mathlib.Meta.NormNum.IsNNRat.to_isRat, Mathlib.Meta.NormNum.isNNRat_div and 106 more
155 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
def Erdos26.ValidStep line 199 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset
Proof uses: And, LE.le, Exists, GT.gt, HPow.hPow, OfNat.ofNat, Nat.Prime, Membership.mem, Dvd.dvd, HAdd.hAdd, Real, HDiv.hDiv, Finset.sum, Eq, Finset.card, GE.ge, HMul.hMul, Finset.Nonempty
24 instances, coercions and auxiliary constants left out.
lemma Erdos26.exists_next_state line 211 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, Finset, Erdos26.ValidStep
Proof uses: And, GT.gt, OfNat.ofNat, Max.max, LE.le, HPow.hPow, Nat.Prime, Dvd.dvd, HAdd.hAdd, Erdos26.exists_x_P_ind, GE.ge, le_max_right, Decidable.byContradiction, Not, Real, HDiv.hDiv, Erdos26.sum_ap, Erdos26.exists_L_sum, Finset.image, HMul.hMul and 95 more
146 instances, coercions and auxiliary constants left out.

Tactic trace: 91 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.exists_next_state_tuple line 290 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, Prod, Finset, Erdos26.ValidStep, Prod.fst, Prod.snd
Proof uses: Erdos26.exists_next_state, Exists.intro, Prod.mk
1 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Erdos26.seqState line 295 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Finset
Proof uses: Prod.mk, EmptyCollection.emptyCollection, OfNat.ofNat, Classical.choose, Erdos26.ValidStep, HAdd.hAdd, Prod.fst, Prod.snd
6 instances, coercions and auxiliary constants left out.
def Erdos26.A_j line 300 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset
Proof uses: Prod.fst, Prod, Erdos26.seqState
def Erdos26.K_j line 301 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Prod.fst, Prod, Prod.snd, Finset, Erdos26.seqState
def Erdos26.max_A_j line 302 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Prod.fst, Prod.snd, Prod, Finset, Erdos26.seqState
def Erdos26.S_j line 303 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Prod.snd, Prod, Finset, Erdos26.seqState
lemma Erdos26.step_valid line 305 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Erdos26.ValidStep, Erdos26.K_j, HSub.hSub, Erdos26.max_A_j, Erdos26.S_j, Erdos26.A_j
Proof uses: Exists, Eq, HAdd.hAdd, Exists.intro, Decidable.byContradiction, Not, Eq.mpr, id, congrArg, Prod.fst, Finset, Prod, Classical.choose, Prod.snd, Erdos26.exists_next_state_tuple, Classical.choose_spec, Erdos26.seqState, Prod.mk, EmptyCollection.emptyCollection, Eq.refl and 2 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
def Erdos26.seqA_set line 324 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat
Proof uses: Set.iUnion, GE.ge, OfNat.ofNat, Finset, Erdos26.A_j
4 instances, coercions and auxiliary constants left out.
lemma Erdos26.seqA_set_infinite line 326 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set.Infinite, Nat, Erdos26.seqA_set
Proof uses: Set.Finite, BddAbove, Set.Finite.bddAbove, Membership.mem, Set, upperBounds, False, GE.ge, OfNat.ofNat, GT.gt, Erdos26.max_A_j, HSub.hSub, Erdos26.ValidStep, Erdos26.K_j, Erdos26.S_j, Erdos26.A_j, Erdos26.step_valid, Finset.Nonempty, And.right, Finset and 28 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 47 steps
Open to load the checked before-and-after goal states.
def Erdos26.seqA line 372 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Nat.nth, Erdos26.seqA_set
lemma Erdos26.seqA_strict_mono line 374 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: StrictMono, Nat, Erdos26.seqA
Proof uses: Set.Infinite, Erdos26.seqA_set, Erdos26.seqA_set_infinite, Nat.nth_strictMono
1 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.seqA_range line 378 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Set, Nat, Set.range, Erdos26.seqA, Erdos26.seqA_set
Proof uses: Nat.range_nth_of_infinite, Erdos26.seqA_set_infinite

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.seqA_bijective line 381 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Function.Bijective, Nat, Subtype, Membership.mem, Set, Erdos26.seqA_set, Subtype.mk, Erdos26.seqA, Set.range, Set.mem_range_self, Eq.mp, congrArg, Erdos26.seqA_range
Proof uses: And.intro, Function.Injective, Function.Surjective, Eq, StrictMono.injective, Erdos26.seqA_strict_mono, Subtype.mk.injEq, Erdos26.seqA_bijective.match_1, Exists, Eq.symm, Exists.intro, Eq.mpr, id
5 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
def Erdos26.seqA_equiv line 397 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Equiv, Nat, Subtype, Membership.mem, Set, Erdos26.seqA_set
Proof uses: Equiv.ofBijective, Subtype.mk, Erdos26.seqA, Erdos26.seqA_bijective
3 instances, coercions and auxiliary constants left out.
lemma Erdos26.seqA_sum_1 line 400 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Summable, Real, Nat, HDiv.hDiv, OfNat.ofNat, Erdos26.seqA, SummationFilter.unconditional, Subtype, Membership.mem, Set, Erdos26.seqA_set
Proof uses: Eq, Function.comp, Equiv, Erdos26.seqA_equiv, funext, Eq.refl, Iff.mp, Equiv.summable_iff, Eq.mp, congrArg
29 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.max_A_j_mono line 408 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Erdos26.max_A_j
Proof uses: Nat.le_induction, le_refl, Erdos26.ValidStep, HAdd.hAdd, OfNat.ofNat, Erdos26.K_j, HSub.hSub, Erdos26.S_j, Erdos26.A_j, Erdos26.step_valid, Decidable.byContradiction, GE.ge, Not, And.left, Finset.Nonempty, And.right, Membership.mem, Finset, And, GT.gt and 12 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.A_j_disjoint_lt line 418 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, LT.lt, Membership.mem, Finset, Erdos26.A_j
Proof uses: Erdos26.ValidStep, Erdos26.K_j, HSub.hSub, Erdos26.max_A_j, Erdos26.S_j, Erdos26.step_valid, And.left, And, Finset.Nonempty, And.right, GT.gt, HMul.hMul, HPow.hPow, HAdd.hAdd, Eq, Finset.card, LE.le, Real, Finset.sum, HDiv.hDiv and 6 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.A_j_unique line 427 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Membership.mem, Finset, Erdos26.A_j, Eq
Proof uses: LT.lt, Or, lt_trichotomy, False.elim, Erdos26.A_j_disjoint_lt
13 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.seqA_sigma_bijective line 438 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Function.Bijective, Sigma, Subtype, Nat, LE.le, OfNat.ofNat, Membership.mem, Finset, Erdos26.A_j, Set, Erdos26.seqA_set, Subtype.mk, Sigma.fst, Sigma.snd, Eq.mpr, Set.iUnion, GE.ge, id, Eq, congrArg and 6 more
Proof uses: And.intro, Function.Injective, Function.Surjective, Erdos26.A_j_unique, Eq.mp, Subtype.mk.injEq, Subtype.ext, Sigma.mk, Eq.refl, Eq.symm, Erdos26.seqA_bijective.match_1
17 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
def Erdos26.seqA_sigma_equiv line 464 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Equiv, Sigma, Subtype, Nat, LE.le, OfNat.ofNat, Membership.mem, Finset, Erdos26.A_j, Set, Erdos26.seqA_set
Proof uses: Equiv.ofBijective, Subtype.mk, Sigma.fst, Sigma.snd, Erdos26.seqA_sigma_bijective
11 instances, coercions and auxiliary constants left out.
lemma Erdos26.seqA_sum_blocks_2 line 467 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Summable, Real, Subtype, Nat, Membership.mem, Set, Erdos26.seqA_set, HDiv.hDiv, OfNat.ofNat, SummationFilter.unconditional, Sigma, LE.le, Finset, Erdos26.A_j, Sigma.fst, Sigma.snd
Proof uses: Eq, Function.comp, Equiv, Erdos26.seqA_sigma_equiv, funext, Eq.refl, Eq.mpr, id, congrArg, Iff.mpr, Equiv.summable_iff
35 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.tsum_Finset_eq_sum_Finset line 476 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Eq, Real, tsum, Subtype, Membership.mem, HDiv.hDiv, OfNat.ofNat, SummationFilter.unconditional, Finset.sum
Proof uses: Finset.tsum_subtype'
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.seqA_sum_blocks_3 line 479 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Summable, Real, Sigma, Subtype, Nat, LE.le, OfNat.ofNat, Membership.mem, Finset, Erdos26.A_j, HDiv.hDiv, Sigma.fst, Sigma.snd, SummationFilter.unconditional, Finset.sum
Proof uses: tsum, Summable.sigma, Eq, funext, Erdos26.tsum_Finset_eq_sum_Finset, Eq.mp, congrArg
33 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.seqA_sum_blocks_4 line 489 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Summable, Real, Subtype, Nat, LE.le, OfNat.ofNat, Finset.sum, Erdos26.A_j, HDiv.hDiv, SummationFilter.unconditional
Proof uses: Summable.of_nonneg_of_le, Mathlib.Meta.NormNum.isRat_le_true, Int.ofNat, Mathlib.Meta.NormNum.IsNNRat.to_isRat, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, HMul.hMul, Inv.inv, Eq.refl, Nat.cast_one, Mathlib.Meta.NormNum.isNNRat_inv_pos, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.mul, Bool, Bool.true, Erdos26.ValidStep, Erdos26.K_j and 20 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.seqA_sum_blocks_5 line 499 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Summable, Real, Subtype, Nat, LE.le, OfNat.ofNat, HDiv.hDiv, SummationFilter.unconditional, False
Proof uses: Filter.Tendsto, Filter.cofinite, nhds, Summable.tendsto_cofinite_zero, tendsto_const_nhds, Eq, tendsto_nhds_unique, False.elim, Eq.mp, eq_false, Mathlib.Meta.NormNum.isNNRat_eq_false, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, HMul.hMul, Inv.inv, Eq.refl, Nat.cast_one and 5 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.seqA_thick line 505 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Erdos26.IsThick, Nat, Erdos26.seqA
Proof uses: id, Summable, Real, HDiv.hDiv, OfNat.ofNat, SummationFilter.unconditional, Subtype, Membership.mem, Set, Erdos26.seqA_set, Erdos26.seqA_sum_1, Sigma, LE.le, Finset, Erdos26.A_j, Sigma.fst, Sigma.snd, Erdos26.seqA_sum_blocks_2, Finset.sum, Erdos26.seqA_sum_blocks_3 and 2 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
def Erdos26.M_val line 514 source
no axioms what this means
Statement uses: Nat, Set
Proof uses: Set.range, HMul.hMul
2 instances, coercions and auxiliary constants left out.
lemma Erdos26.M_val_card_bound line 516 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, LE.le, Real, Finset.card, Finset.filter, Membership.mem, Set, Erdos26.M_val, Finset.Icc, HDiv.hDiv
Proof uses: Eq, Finset, Finset.image, HMul.hMul, Finset.ext, Eq.mpr, Iff, And, id, congrArg, propext, Finset.mem_filter, Exists, Finset.mem_image, Iff.intro, Eq.mp, Set.range, Set.mem_range, Exists.intro, Decidable.byContradiction and 87 more
132 instances, coercions and auxiliary constants left out.

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.exists_j1 line 559 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Exists, And, LT.lt, Erdos26.K_j, HAdd.hAdd
Proof uses: Exists.intro, Nat.recAux, le_refl, Erdos26.ValidStep, HSub.hSub, Erdos26.max_A_j, Erdos26.S_j, Erdos26.A_j, Erdos26.step_valid, Decidable.byContradiction, Not, GT.gt, And.left, Membership.mem, Finset, Finset.Nonempty, And.right, HMul.hMul, HPow.hPow, Eq and 18 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
def Erdos26.block_multiples_A line 591 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set
Proof uses: Set.iUnion, Membership.mem, Finset, Erdos26.A_j, Erdos26.M_val, HAdd.hAdd
3 instances, coercions and auxiliary constants left out.
lemma Erdos26.seqA_multiples_subset line 594 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, HasSubset.Subset, Set, Erdos26.MultiplesOf, HAdd.hAdd, Erdos26.seqA, Set.iUnion, GE.ge, OfNat.ofNat, Erdos26.block_multiples_A
Proof uses: Membership.mem, Prod, Eq, Erdos26.MultiplesOf.match_1, HMul.hMul, Exists, Eq.mp, Set.range, congrArg, propext, Set.mem_range, Prod.mk, Erdos26.seqA_set, Set.mem_range_self, Erdos26.seqA_range, Finset, Erdos26.A_j, Eq.trans, funext, Erdos26.seqA_set.eq_1 and 5 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.block_multiples_A_subset_prime line 621 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, LE.le, Erdos26.K_j, HSub.hSub, Exists, And, GT.gt, HPow.hPow, Nat.Prime, HasSubset.Subset, Set, Erdos26.block_multiples_A, Erdos26.M_val
Proof uses: Erdos26.ValidStep, Erdos26.max_A_j, Erdos26.S_j, Erdos26.A_j, Erdos26.step_valid, Membership.mem, Finset, Dvd.dvd, HAdd.hAdd, And.left, Real, HDiv.hDiv, Finset.sum, Eq, Finset.card, HMul.hMul, Finset.Nonempty, Exists.intro, And.intro, id and 20 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.card_future_blocks_bound line 640 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, LE.le, Erdos26.K_j, HSub.hSub, Real, Finset.card, Finset.filter, Membership.mem, Set, Erdos26.block_multiples_A, Finset.Icc, HDiv.hDiv, HPow.hPow
Proof uses: And, GT.gt, Nat.Prime, HasSubset.Subset, Erdos26.M_val, Exists, Erdos26.block_multiples_A_subset_prime, Finset, Eq.mpr, id, Eq, congrArg, propext, Finset.mem_filter, And.intro, And.left, Eq.mp, And.right, cast, Eq.symm and 85 more
146 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.filter_bUnion_le_sum_card line 659 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Set, Nat, LE.le, Real, Finset.card, Finset.filter, Membership.mem, Set.iUnion, Finset.Icc, OfNat.ofNat, Finset.sum
Proof uses: Finset.induction_on, of_eq_true, EmptyCollection.emptyCollection, Eq.trans, True, congrArg, False, Finset.filter.congr_simp, funext, Set.iUnion_congr_Prop, Iff.of_eq, Eq.refl, Set.iUnion_of_empty, Set.iUnion_empty, Finset.filter_false, CharP.cast_eq_zero, Not, Eq, Insert.insert, Union.union and 61 more
100 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.filter_Union_le_sum_card_Icc line 681 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set, LE.le, Real, Finset.card, Finset.filter, Membership.mem, Set.iUnion, Finset, Finset.Icc, OfNat.ofNat, Finset.sum
Proof uses: Erdos26.filter_bUnion_le_sum_card
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.max_A_j_ge line 685 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, Erdos26.max_A_j
Proof uses: Nat.recAux, le_refl, OfNat.ofNat, Erdos26.ValidStep, HAdd.hAdd, Erdos26.K_j, HSub.hSub, Erdos26.S_j, Erdos26.A_j, Erdos26.step_valid, Decidable.byContradiction, Not, LE.le, Exists, And, GT.gt, HPow.hPow, Nat.Prime, Membership.mem, Finset and 10 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.filter_Union_ge_empty line 698 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Eq, Finset, Finset.filter, Membership.mem, Set, Set.iUnion, Erdos26.block_multiples_A, Finset.Icc, Max.max
Proof uses: Finset.ext, Eq.mpr, Iff, And, LE.le, Exists, Erdos26.A_j, HMul.hMul, HAdd.hAdd, id, congr, congrArg, Eq.trans, Finset.filter.congr_simp, funext, Set.range, Set.iUnion_congr_Prop, Iff.of_eq, Eq.refl, Erdos26.M_val and 30 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.filter_Union_ge_le_sum line 726 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, LE.le, Real, Finset.card, Finset.filter, Membership.mem, Set, Set.iUnion, Erdos26.block_multiples_A, Finset.Icc, Finset.sum, Max.max
Proof uses: Eq.mpr, Finset, id, Eq, congrArg, Erdos26.filter_Union_ge_empty, Erdos26.filter_Union_le_sum_card_Icc
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.sigma_A_j_card line 733 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Sigma, Finset.sigma, Finset.Icc, OfNat.ofNat, Erdos26.A_j, Erdos26.S_j
Proof uses: Nat.recAux, Finset, EmptyCollection.emptyCollection, Finset.Icc_eq_empty, LE.le, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, Finset.sum, True, Finset.card_sigma, eq_self, HAdd.hAdd, Insert.insert, Finset.ext, Iff, Membership.mem, Or and 25 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.bUnion_block_multiples_A_eq_sigma line 762 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Set, Set.iUnion, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Erdos26.block_multiples_A, Sigma, Finset.sigma, Erdos26.A_j, Erdos26.M_val, HAdd.hAdd, Sigma.snd
Proof uses: Set.ext, Eq.mpr, Iff, Exists, And, id, congr, congrArg, Eq.trans, funext, Set.iUnion_congr_Prop, Iff.of_eq, Eq.refl, propext, exists_prop_congr, Sigma.fst, Sigma.mk, Iff.intro, Exists.intro, And.intro
18 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.sum_filter_M_val_le line 772 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GT.gt, Erdos26.K_j, LE.le, Real, Finset.sum, Sigma, Finset.sigma, Finset.Icc, OfNat.ofNat, Erdos26.A_j, Finset.card, Finset.filter, Membership.mem, Set, Erdos26.M_val, HAdd.hAdd, Sigma.snd, HDiv.hDiv
Proof uses: Finset.sum_le_sum, Finset, Decidable.byContradiction, Not, Erdos26.M_val_card_bound, cast, Eq.symm, Eq.trans, congrArg, LT.lt, Nat.cast_zero, Nat.cast_nonneg', Eq, Eq.mpr, id, Nat.cast_add, Eq.refl, div_le_div_of_nonneg_left, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl and 64 more
127 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.S_j_le_k_div_10 line 789 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GT.gt, Erdos26.K_j, LE.le, Real, HDiv.hDiv, Erdos26.S_j, OfNat.ofNat
Proof uses: Eq, LT.lt, Or, eq_zero_or_pos, rfl, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, Mathlib.Meta.NormNum.instAtLeastTwo, congr, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Nat.cast_zero, zero_div, Mathlib.Meta.NormNum.IsNNRat.to_eq and 104 more
139 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.card_past_elements_bound line 813 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GT.gt, Erdos26.K_j, LE.le, Real, Finset.card, Finset.filter, Membership.mem, Set, Set.iUnion, Finset, Finset.Icc, OfNat.ofNat, Erdos26.block_multiples_A, HMul.hMul, HDiv.hDiv
Proof uses: Eq, Sigma, Finset.sigma, Erdos26.A_j, Erdos26.M_val, HAdd.hAdd, Sigma.snd, Erdos26.bUnion_block_multiples_A_eq_sigma, Eq.mpr, id, congrArg, Finset.sum, Erdos26.filter_bUnion_le_sum_card, Erdos26.sum_filter_M_val_le, HSMul.hSMul, Finset.sum_const, nsmul_eq_mul, Eq.refl, Erdos26.S_j, cast and 92 more
128 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.card_current_block_bound line 831 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, LE.le, Real, Finset.card, Finset.filter, Membership.mem, Set, Erdos26.block_multiples_A, Finset.Icc, HMul.hMul, HDiv.hDiv
Proof uses: Erdos26.ValidStep, Erdos26.K_j, HSub.hSub, Erdos26.max_A_j, Erdos26.S_j, Erdos26.A_j, Erdos26.step_valid, id, Set.iUnion, Finset, Erdos26.M_val, HAdd.hAdd, Finset.sum, Erdos26.filter_bUnion_le_sum_card, Finset.sum_le_sum, GT.gt, And.left, And, Eq, HPow.hPow and 103 more
153 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.geom_sum_eq line 864 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, Finset.sum, Finset.Icc, OfNat.ofNat, HDiv.hDiv, HPow.hPow, HMul.hMul, HSub.hSub
Proof uses: Nat.recAux, Finset, EmptyCollection.emptyCollection, Finset.Icc_eq_empty_of_lt, Decidable.byContradiction, LT.lt, Not, Eq.mpr, id, congrArg, Finset.sum_empty, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.IsNNRat.to_isNat, Mathlib.Meta.NormNum.isNNRat_mul, Eq.refl, Mathlib.Meta.NormNum.isNNRat_div, Inv.inv, Mathlib.Meta.NormNum.IsNat.to_isNNRat and 94 more
122 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.geom_sum_bound line 891 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, Finset.sum, Finset.Icc, OfNat.ofNat, HDiv.hDiv, HPow.hPow
Proof uses: Eq.mpr, HMul.hMul, HSub.hSub, id, Eq, congrArg, Erdos26.geom_sum_eq, le_of_lt, div_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Bool, Nat.ble, pow_pos, Mathlib.Meta.NormNum.instAtLeastTwo, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl and 79 more
113 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.geom_sum_bound2 line 896 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, LE.le, Real, Finset.sum, Finset.Icc, HDiv.hDiv, HPow.hPow
Proof uses: dite, LE.le.trans, Function.comp, HasSubset.Subset, Finset, Membership.mem, Not, Finset.sum_le_sum_of_subset_of_nonneg, Finset.Icc_subset_Icc_left, le_of_lt, div_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Bool, Nat.ble, pow_pos, Mathlib.Meta.NormNum.instAtLeastTwo, Eq.trans_le and 65 more
166 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.card_all_blocks_zero line 900 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, Finset.card, Finset.filter, Membership.mem, Set, Set.iUnion, GE.ge, OfNat.ofNat, Erdos26.block_multiples_A, Finset.Icc, HMul.hMul, HDiv.hDiv
Proof uses: Finset.sum, Max.max, Erdos26.filter_Union_ge_le_sum, Decidable.byContradiction, Not, HPow.hPow, Finset.sum_le_sum, Finset, Erdos26.card_future_blocks_bound, And.left, Eq.mp, And, congrArg, propext, Finset.mem_Icc, Erdos26.K_j, HSub.hSub, Eq, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd and 95 more
130 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.multiples_card_bound_zero line 917 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, Finset.card, Finset.filter, Membership.mem, Set, Erdos26.MultiplesOf, HAdd.hAdd, Erdos26.seqA, OfNat.ofNat, Finset.Icc, HMul.hMul, HDiv.hDiv
Proof uses: HasSubset.Subset, Set.iUnion, GE.ge, Erdos26.block_multiples_A, Erdos26.seqA_multiples_subset, Finset, Eq.mpr, And, id, Eq, congrArg, propext, Finset.mem_filter, And.intro, And.left, Eq.mp, And.right, cast, Eq.symm, Finset.card_le_card and 83 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.card_union_three_le line 929 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, LE.le, Nat, Finset.card, Union.union, HAdd.hAdd
Proof uses: Finset.card_union_le, Decidable.byContradiction, Not
10 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.K_j_mono line 935 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Erdos26.K_j
Proof uses: Nat.le_induction, le_refl, Erdos26.ValidStep, HAdd.hAdd, OfNat.ofNat, HSub.hSub, Erdos26.max_A_j, Erdos26.S_j, Erdos26.A_j, Erdos26.step_valid, Decidable.byContradiction, GE.ge, Not, Exists, And, GT.gt, HPow.hPow, Nat.Prime, Membership.mem, Finset and 10 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.union_split line 945 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, HasSubset.Subset, Finset, Finset.filter, Membership.mem, Set, Set.iUnion, GE.ge, OfNat.ofNat, Erdos26.block_multiples_A, Finset.Icc, Union.union, HAdd.hAdd
Proof uses: And, Eq.mp, congrArg, propext, Finset.mem_filter, Eq.mpr, Exists, id, Eq, congr, Finset.filter.congr_simp, funext, Eq.trans, Eq.refl, Or, Finset.mem_union, LT.lt, lt_trichotomy, Or.inl, And.intro and 7 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.multiples_card_bound_pos line 966 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, LE.le, Real, Finset.card, Finset.filter, Membership.mem, Set, Erdos26.MultiplesOf, HAdd.hAdd, Erdos26.seqA, Finset.Icc, HMul.hMul, HDiv.hDiv
Proof uses: Exists, And, LT.lt, Erdos26.K_j, Erdos26.exists_j1, HasSubset.Subset, Set.iUnion, Erdos26.block_multiples_A, Erdos26.seqA_multiples_subset, Finset, Eq.mpr, id, Eq, congrArg, propext, Finset.mem_filter, And.intro, And.left, Eq.mp, And.right and 116 more
145 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.multiples_card_bound line 1007 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, Finset.card, Finset.filter, Membership.mem, Set, Erdos26.MultiplesOf, HAdd.hAdd, Erdos26.seqA, Finset.Icc, OfNat.ofNat, HMul.hMul, HDiv.hDiv
Proof uses: Eq, LT.lt, Or, eq_zero_or_pos, Erdos26.multiples_card_bound_zero, Eq.symm, Erdos26.multiples_card_bound_pos
47 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def Erdos26.X_seq line 1014 source
no axioms what this means
Statement uses: Nat
Proof uses: HAdd.hAdd, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
lemma Erdos26.tendsto_X_seq line 1016 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Tendsto, Nat, Erdos26.X_seq, Filter.atTop
Proof uses: StrictMono, LT.lt, id, Decidable.byContradiction, HAdd.hAdd, OfNat.ofNat, Not, StrictMono.tendsto_atTop
8 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.lowerDensity_le_of_seq line 1023 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Real, LE.le, Finset.card, Finset.filter, Membership.mem, Finset.Icc, OfNat.ofNat, Erdos26.X_seq, HMul.hMul, Set.lowerDensity, Set.univ
Proof uses: id, Eq.mpr, Filter.liminf, Set.partialDensity, Filter.atTop, SupSet.sSup, setOf, Exists, HDiv.hDiv, Set.ncard, Inter.inter, Set.Iio, Eq, congrArg, Eq.trans, funext, congr, Set.inter_univ, Set.univ_inter, Nat.ncard_Iio and 88 more
164 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.seqA_density_bound line 1036 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Real, Set.lowerDensity, Erdos26.MultiplesOf, HAdd.hAdd, Erdos26.seqA, Set.univ, HDiv.hDiv, OfNat.ofNat
Proof uses: LE.le, Finset.card, Finset.filter, Membership.mem, Set, Finset.Icc, Erdos26.X_seq, HMul.hMul, Erdos26.multiples_card_bound, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, HPow.hPow and 75 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Erdos26.not_weakly_behrend_seqA line 1045 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, Erdos26.IsWeaklyBehrend, HAdd.hAdd, Erdos26.seqA, HDiv.hDiv, Real, OfNat.ofNat
Proof uses: id, LT.lt, Set.lowerDensity, Erdos26.MultiplesOf, Set.univ, Erdos26.seqA_density_bound, Not.intro, LE.le, HSub.hSub, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HMul.hMul, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Int.rawCast, Int.negOfNat and 67 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Erdos26.target_theorem_0 Erdős problem 26 variant: a thick sequence whose shifted multiples stay sparse line 1053 source
L4DEL explanation
We construct the sequence iteratively in finite blocks
— Human-written proof companion for Erdős 26
The universal weak-Behrend assertion is false. There is a strictly increasing sequence with divergent reciprocal sum such that every additive shift still leaves a fixed positive proportion of integers uncovered by its multiples.
1. Construct the sequence in finite arithmetic-progression blocks, with prime congruences assigned to each stage.
2. The reciprocal mass of the blocks diverges, so the resulting sequence is thick.
3. For any fixed shift, the congruence structure bounds the upper density of its multiples below 1-ε, contradicting the claimed weak-Behrend conclusion.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written proof companion for Erdős 26, Erdős Problems 26 source record
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Iff, False, Nat, StrictMono, Erdos26.IsThick, Real, GT.gt, OfNat.ofNat, Exists, Erdos26.IsWeaklyBehrend, HAdd.hAdd
Proof uses: Iff.intro, False.elim, Erdos26.seqA, Erdos26.seqA_strict_mono, Erdos26.seqA_thick, HDiv.hDiv, Mathlib.Meta.NormNum.isNNRat_lt_true, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, HMul.hMul, Inv.inv, Eq.refl, Nat.cast_one, Mathlib.Meta.NormNum.isNNRat_inv_pos, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.mul, Bool and 3 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
theorem target_theorem_0
  : answer(False) ↔ ∀ᵉ (A : ℕ → ℕ), StrictMono A → IsThick A → (∀ ε > (0 : ℝ), ∃ k, IsWeaklyBehrend (A · + k) ε) := by
…
```
Mentions: Erdos26.IsThick, Erdos26.IsWeaklyBehrend