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

54 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

FormalConjectures.Util.ProblemImports

def Erdos846.NonTrilinearFor We say a subset A of points in the plane is ε-non-trilinear if any subset B of A, contains a non-trilinear subset C of size at least ε|B| line 50 source
Source documentation
We say a subset A of points in the plane is ε-non-trilinear if any subset B of A, contains a non-trilinear subset C of size at least ε|B|.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
Proof uses: Finset, HasSubset.Subset, Exists, And, LE.le, HMul.hMul, Finset.card, EuclideanGeometry.NonTrilinear, ENNReal
32 instances, coercions and auxiliary constants left out.
```
def NonTrilinearFor (A : Set ℝ²) (ε : ℝ) : Prop :=
…
```
def Erdos846.WeaklyNonTrilinear We say a subset A of points in the plane is weakly non-trilinear if it is a finite union of non-trilinear sets line 56 source
Source documentation
We say a subset A of points in the plane is weakly non-trilinear if it is a finite union of non-trilinear sets.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
Proof uses: Exists, Finset, And, Eq, SupSet.sSup, Membership.mem, EuclideanGeometry.NonTrilinear, ENNReal
27 instances, coercions and auxiliary constants left out.
```
def WeaklyNonTrilinear (A : Set ℝ²) : Prop :=
…
```
lemma Erdos846.bipartite_max_cut_nat line 96 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Nat, Membership.mem, LT.lt, Prod.fst, Prod.snd, Exists, GE.ge, HMul.hMul, OfNat.ofNat, Finset.card, Finset.filter, Or, And, Not
Proof uses: Exists.elim, Set, upperBounds, Set.image, Set.Finite.bddAbove, Set.Finite.image, Finset.finite_toSet, Finset.bddAbove, dite, Finset.sum, Finset.powerset, Finset.range, HAdd.hAdd, ite, False, Eq, LE.le.not_gt, Eq.rec, LE.le, Finset.sum_le_sum and 77 more
129 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.nontrilinear_of_no_collinear_triples line 107 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Membership.mem, Ne, Not, Collinear, ENNReal, Insert.insert, Set, Singleton.singleton, EuclideanGeometry.NonTrilinear
86 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Erdos846.FormsTriangle line 113 source
no axioms what this means
Statement uses: Prod, Nat
Proof uses: Exists, And, LT.lt, Eq, Set, Insert.insert, Singleton.singleton, Prod.mk
3 instances, coercions and auxiliary constants left out.
lemma Erdos846.bipartite_has_no_triangle line 117 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Prod, Membership.mem, Or, And, Prod.fst, Not, Prod.snd, Erdos846.FormsTriangle
Proof uses: id, Eq.mpr, Set, setOf, Exists, LT.lt, Eq, Insert.insert, Singleton.singleton, Prod.mk, Iff, Eq.trans, congrArg, funext, forall_congr, congr, implies_congr, Eq.refl, absurd, False and 6 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def Erdos846.IsGoodMap line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Nat, EuclideanSpace, Real, Fin, OfNat.ofNat
Proof uses: And, LT.lt, Prod.fst, Prod.snd, Ne, Iff, Collinear, ENNReal, Insert.insert, Set, Singleton.singleton, Erdos846.FormsTriangle
39 instances, coercions and auxiliary constants left out.
lemma Erdos846.elekes_identity line 132 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul, Eq, HSub.hSub
Proof uses: Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_pf_add_lt, Mathlib.Tactic.Ring.add_pf_zero_add, Mathlib.Tactic.Ring.add_pf_add_gt, Mathlib.Tactic.Ring.add_pf_add_zero, Mathlib.Tactic.Ring.sub_pf, Mathlib.Tactic.Ring.neg_add, Mathlib.Tactic.Ring.neg_mul, Mathlib.Tactic.Ring.neg_one_mul, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.isInt_mul and 30 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Erdos846.real_point line 140 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, EuclideanSpace, Fin, OfNat.ofNat, Nat
Proof uses: Matrix.vecCons, Matrix.vecEmpty, Equiv, WithLp, ENNReal, Equiv.symm, WithLp.equiv
10 instances, coercions and auxiliary constants left out.
lemma Erdos846.real_point_inj line 144 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, EuclideanSpace, Fin, OfNat.ofNat, Nat, Erdos846.real_point, And
Proof uses: of_eq_true, Eq.trans, True, congr, congrArg, id, Eq.mp, WithLp, ENNReal, WithLp.toLp, Matrix.vecCons, Matrix.vecEmpty, WithLp.toLp.injEq, Nat.succ, eq_self, and_true, and_self
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.collinear_iff_det2 line 148 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Iff, Collinear, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Insert.insert, Set, Erdos846.real_point, Singleton.singleton, Eq, HMul.hMul, HSub.hSub
Proof uses: Eq.mpr, Exists, And, WithLp.toLp, Matrix.vecCons, Matrix.vecEmpty, HAdd.hAdd, HSMul.hSMul, id, Eq.rec, Eq.refl, Eq.trans, Membership.mem, HVAdd.hVAdd, DivisionRing, AddCommGroup, Module, AddTorsor, propext, collinear_iff_of_mem and 146 more
286 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
def Erdos846.t_seq line 170 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: Erdos846.t_seq.match_1, Unit, OfNat.ofNat, Nat.succ, HPow.hPow
9 instances, coercions and auxiliary constants left out.
lemma Erdos846.t_seq_pos line 174 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, Real, Erdos846.t_seq, OfNat.ofNat
Proof uses: id, Nat.rec, Erdos846.t_seq.match_1, Unit, Nat.succ, HPow.hPow, le_rfl, LE.le.trans, le_self_pow₀, Mathlib.Tactic.LinearCombination.le_of_le, Mathlib.Tactic.LinearCombination.le_rearrange, HAdd.hAdd, Mathlib.Tactic.Ring.le_congr, HSub.hSub, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.sub_congr, Nat.rawCast, HMul.hMul, Mathlib.Tactic.Ring.instCommSemiringNat and 39 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.t_seq_int line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, Int, Eq, Real, Erdos846.t_seq
Proof uses: id, Nat.recAux, Erdos846.t_seq.match_1, Unit, OfNat.ofNat, Nat.succ, HPow.hPow, Exists.intro, Eq.refl, HAdd.hAdd, of_eq_true, Nat.brecOn.go, Nat.rec, PUnit, PProd, Eq.trans, True, congr, congrArg, Int.cast_pow and 1 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.abs_ge_one_of_int line 182 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Exists, Int, Eq, Ne, GE.ge, abs, HSub.hSub, OfNat.ofNat
Proof uses: Exists.elim, Eq.rec, cast, LT.lt, Eq.trans, Nat, congrArg, Eq.symm, Nat.cast_zero, LE.le, Nat.cast_one, Int.cast_one, Iff.mpr, abs_sub_pos, Not, Aesop.BuiltinRules.not_intro, False, Eq.refl
75 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.t_seq_bound_linear_pos line 185 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, GE.ge, OfNat.ofNat, LE.le, abs, HMul.hMul, Nat, HPow.hPow, GT.gt, HAdd.hAdd
Proof uses: lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, HSub.hSub, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.sub_congr and 66 more
101 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.t_seq_bound_linear_neg line 189 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, Neg.neg, OfNat.ofNat, abs, HMul.hMul, Nat, HPow.hPow, GE.ge, LT.lt, HAdd.hAdd
Proof uses: lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.pow_congr and 63 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.t_seq_strict_mono line 193 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: StrictMono, Nat, Real, Erdos846.t_seq
Proof uses: id, strictMono_nat_of_lt_succ, Erdos846.t_seq.match_1, Unit, OfNat.ofNat, Nat.succ, HPow.hPow, lt_self_pow₀, Nat.rec, LT.lt, Mathlib.Meta.NormNum.isNat_lt_true, Nat.zero, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.false, one_lt_pow₀, of_decide_eq_true and 4 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.t_seq_bound_A line 197 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, GE.ge, OfNat.ofNat, LE.le, abs, HMul.hMul, Nat, HPow.hPow, GT.gt, HAdd.hAdd
Proof uses: lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.neg_congr and 63 more
120 instances, coercions and auxiliary constants left out.

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

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.t_seq_sum_inj_of_lt line 207 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Or, And, Eq, Real, HAdd.hAdd, Erdos846.t_seq
Proof uses: id, Nat.rec, OfNat.ofNat, HPow.hPow, Eq.mpr, Erdos846.t_seq.match_1, Unit, Nat.succ, eq_of_heq, LT, HEq, Eq.refl, HEq.refl, Eq.symm, congr_arg₂, rfl, Nat.zero, congr_arg, GT.gt, Mathlib.Meta.NormNum.isNat_lt_true and 107 more
118 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.t_seq_sum_inj line 219 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Ne, Prod, Prod.mk, Real, HAdd.hAdd, Erdos846.t_seq
Proof uses: Or, Eq, lt_trichotomy, Erdos846.t_seq_sum_inj_of_lt, Or.inl, And, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, OfNat.ofNat, Eq.mp, HSub.hSub, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast and 40 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.t_seq_inj_sum line 237 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Ne, Prod, Prod.mk, Or, Real, HAdd.hAdd, Erdos846.t_seq, HPow.hPow, OfNat.ofNat, HMul.hMul
Proof uses: Or.inl, Erdos846.t_seq_sum_inj
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.t_seq_not_collinear_p1 line 243 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul, Eq, HSub.hSub
Proof uses: Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_pf_add_lt, Mathlib.Tactic.Ring.add_pf_zero_add, Mathlib.Tactic.Ring.sub_pf, Mathlib.Tactic.Ring.neg_add, Mathlib.Tactic.Ring.neg_mul, Mathlib.Tactic.Ring.neg_one_mul, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.isInt_mul, Int.ofNat, Eq.refl and 32 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.t_seq_not_collinear_p2 line 252 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul, Eq, HSub.hSub
Proof uses: Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_pf_add_lt, Mathlib.Tactic.Ring.add_pf_zero_add, Mathlib.Tactic.Ring.sub_pf, Mathlib.Tactic.Ring.neg_add, Mathlib.Tactic.Ring.neg_mul, Mathlib.Tactic.Ring.neg_one_mul, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.isInt_mul, Int.ofNat, Eq.refl and 30 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.t_seq_not_collinear_p3 line 261 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul, Eq, HSub.hSub
Proof uses: Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_pf_add_lt, Mathlib.Tactic.Ring.add_pf_zero_add, Mathlib.Tactic.Ring.add_pf_add_gt, Mathlib.Tactic.Ring.add_pf_add_zero, Mathlib.Tactic.Ring.sub_pf, Mathlib.Tactic.Ring.neg_add, Mathlib.Tactic.Ring.neg_mul, Mathlib.Tactic.Ring.neg_one_mul, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.isInt_mul and 30 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.FormsTriangle_symm12 line 270 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Nat, Iff, Erdos846.FormsTriangle
Proof uses: id, Iff.intro, Exists, And, LT.lt, Eq, Set, Insert.insert, Singleton.singleton, Prod.mk, Exists.intro, And.intro, Set.ext, Eq.mpr, Membership.mem, Or, congr, congrArg, Eq.trans, Iff.mpr and 4 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.FormsTriangle_symm23 line 281 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Nat, Iff, Erdos846.FormsTriangle
Proof uses: id, Iff.intro, Exists, And, LT.lt, Eq, Set, Insert.insert, Singleton.singleton, Prod.mk, Exists.intro, And.intro, Set.ext, Eq.mpr, Membership.mem, Or, congr, congrArg, Eq.trans, Iff.mpr and 4 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.FormsTriangle_symm13 line 292 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Nat, Iff, Erdos846.FormsTriangle
Proof uses: id, Iff.intro, Exists, And, LT.lt, Eq, Set, Insert.insert, Singleton.singleton, Prod.mk, Exists.intro, And.intro, Set.ext, Eq.mpr, Membership.mem, Or, congr, congrArg, Eq.trans, Iff.mpr and 4 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.t_seq_not_collinear_case3 line 303 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Ne, Real, HAdd.hAdd, Erdos846.t_seq, HPow.hPow, OfNat.ofNat, HMul.hMul, HSub.hSub
Proof uses: Eq.mpr, Not, Eq, id, Eq.trans, congr, congrArg, add_sub_add_right_eq_sub, StrictMono, strictMono_nat_of_lt_succ, lt_self_pow₀, Erdos846.t_seq.match_1, Unit, Nat.succ, Nat.rec, Mathlib.Meta.NormNum.isNat_lt_true, Nat.zero, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl and 70 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.case1_sum_neq line 316 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Ne, Prod, Prod.mk, Real, HSub.hSub, HAdd.hAdd, Erdos846.t_seq, OfNat.ofNat
Proof uses: Eq, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_pf_add_lt, Mathlib.Tactic.Ring.add_pf_zero_add, Mathlib.Tactic.Ring.sub_pf, Mathlib.Tactic.Ring.neg_add and 30 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.case2_sum_neq line 324 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Ne, Not, Erdos846.FormsTriangle, Prod.mk, Real, HSub.hSub, HAdd.hAdd, Erdos846.t_seq, OfNat.ofNat
Proof uses: Eq, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.neg_congr, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_pf_add_lt and 53 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.t_seq_le_of_le line 354 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, Erdos846.t_seq
Proof uses: StrictMono.monotone, Erdos846.t_seq_strict_mono
5 instances, coercions and auxiliary constants left out.
lemma Erdos846.case1_bounds line 356 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, LE.le, Erdos846.t_seq, GE.ge, OfNat.ofNat, HAdd.hAdd, HPow.hPow, HMul.hMul, HSub.hSub, And, abs
Proof uses: And.intro, Iff.mpr, Neg.neg, abs_le, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 68 more
120 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.case2_bounds line 373 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, LE.le, Erdos846.t_seq, GE.ge, OfNat.ofNat, HAdd.hAdd, HPow.hPow, HMul.hMul, HSub.hSub, abs
Proof uses: Eq.mpr, Neg.neg, id, Eq, congr, congrArg, Eq.trans, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.add_pf_add_lt, Mathlib.Tactic.Ring.add_pf_zero_add, Mathlib.Tactic.Ring.sub_pf, Mathlib.Tactic.Ring.neg_add and 85 more
130 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.t_seq_not_collinear_case2 line 386 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Ne, Not, Erdos846.FormsTriangle, Prod.mk, Real, HAdd.hAdd, Erdos846.t_seq, HPow.hPow, OfNat.ofNat, HMul.hMul, HSub.hSub
Proof uses: Eq, id, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_pf_add_lt, Mathlib.Tactic.Ring.add_pf_zero_add, Mathlib.Tactic.Ring.sub_pf, Mathlib.Tactic.Ring.neg_add, Mathlib.Tactic.Ring.neg_mul, Mathlib.Tactic.Ring.neg_one_mul, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.isInt_mul and 84 more
134 instances, coercions and auxiliary constants left out.

Tactic trace: 65 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.t_seq_not_collinear_case1 line 445 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Ne, Prod, Prod.mk, Real, HAdd.hAdd, Erdos846.t_seq, HPow.hPow, OfNat.ofNat, HMul.hMul, HSub.hSub
Proof uses: Eq, id, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_pf_add_lt, Mathlib.Tactic.Ring.add_pf_zero_add, Mathlib.Tactic.Ring.sub_pf, Mathlib.Tactic.Ring.neg_add, Mathlib.Tactic.Ring.neg_mul, Mathlib.Tactic.Ring.neg_one_mul, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.isInt_mul and 85 more
126 instances, coercions and auxiliary constants left out.

Tactic trace: 62 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.t_seq_not_collinear_symm12 line 500 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Ne, Prod, Prod.mk, Not, Erdos846.FormsTriangle, Real, HAdd.hAdd, Erdos846.t_seq, HPow.hPow, OfNat.ofNat, HMul.hMul, Iff, HSub.hSub
Proof uses: Function.comp, Eq, Neg.neg, not_congr, Iff.symm, Iff.trans, Eq.mpr, id, congrArg, Eq.symm, neg_mul_neg, neg_sub, Iff.rfl, Iff.intro, Mathlib.Tactic.LinearCombination.eq_of_eq, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.sub_congr, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat and 51 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.t_seq_not_collinear_symm23 line 515 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Ne, Prod, Prod.mk, Not, Erdos846.FormsTriangle, Real, HAdd.hAdd, Erdos846.t_seq, HPow.hPow, OfNat.ofNat, HMul.hMul, Iff, HSub.hSub
Proof uses: Iff.intro, Ne.symm
22 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.t_seq_not_collinear_n_max line 531 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, LE.le, Ne, Prod, Prod.mk, Not, Erdos846.FormsTriangle, Real, HAdd.hAdd, Erdos846.t_seq, HPow.hPow, OfNat.ofNat, HMul.hMul, HSub.hSub
Proof uses: Or, Eq, lt_trichotomy, Erdos846.t_seq_not_collinear_case1, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Int.rawCast, Int.negOfNat, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.neg_congr, Mathlib.Tactic.Ring.cast_pos and 46 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 100 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.t_seq_not_collinear line 609 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Ne, Prod, Prod.mk, Not, Erdos846.FormsTriangle, Real, HAdd.hAdd, Erdos846.t_seq, HPow.hPow, OfNat.ofNat, HMul.hMul, HSub.hSub
Proof uses: Or, And, LE.le, Decidable.byContradiction, Erdos846.t_seq_not_collinear_n_max, Iff.mpr, Erdos846.FormsTriangle_symm23, Ne.symm, Iff, Erdos846.t_seq_not_collinear_symm23, Erdos846.FormsTriangle_symm13, id, Eq, Neg.neg, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Int.rawCast, Int.negOfNat and 59 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.triangle_is_collinear line 655 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Erdos846.FormsTriangle, Prod.mk, HAdd.hAdd, HPow.hPow, OfNat.ofNat, HMul.hMul, Eq, HSub.hSub
Proof uses: id, Membership.mem, Set, setOf, Exists, And, LT.lt, Prod, Insert.insert, Singleton.singleton, Eq.mpr, congr, congrArg, add_assoc, Exists.elim, Iff, Or, Eq.mp, Eq.trans, funext and 15 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.exists_good_t line 666 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Nat, Real, And, StrictMono, LT.lt, Ne, Prod, Prod.mk, Or, HAdd.hAdd, HPow.hPow, OfNat.ofNat, HMul.hMul, Iff, Eq, HSub.hSub, Erdos846.FormsTriangle
Proof uses: Exists.intro, Erdos846.t_seq, And.intro, Erdos846.t_seq_strict_mono, Erdos846.t_seq_inj_sum, Iff.intro, Decidable.byContradiction, Not, Erdos846.t_seq_not_collinear, Erdos846.triangle_is_collinear
27 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.exists_good_map line 689 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Prod, Nat, EuclideanSpace, Real, Fin, OfNat.ofNat, Erdos846.IsGoodMap
Proof uses: And, StrictMono, LT.lt, Ne, Prod.mk, Or, HAdd.hAdd, HPow.hPow, HMul.hMul, Iff, Eq, HSub.hSub, Erdos846.FormsTriangle, Erdos846.exists_good_t, Erdos846.real_point, Prod.fst, Prod.snd, Exists.intro, And.intro, Collinear and 14 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
def Erdos846.A_set line 711 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Nat, EuclideanSpace, Real, Fin, OfNat.ofNat, Set
Proof uses: setOf, Exists, And, LT.lt, Eq, Prod.mk
3 instances, coercions and auxiliary constants left out.
lemma Erdos846.A_set_infinite line 714 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Nat, EuclideanSpace, Real, Fin, OfNat.ofNat, Erdos846.IsGoodMap, Set.Infinite, Erdos846.A_set
Proof uses: id, Set.infinite_of_injective_forall_mem, setOf, Exists, And, LT.lt, Eq, Prod.mk, Nat.succ, congr_arg, Prod.fst, by_contra, Not, And.left, Prod.snd, Ne, Iff, Collinear, ENNReal, Insert.insert and 7 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.A_set_nontrilinear line 718 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Nat, EuclideanSpace, Real, Fin, OfNat.ofNat, Erdos846.IsGoodMap, Erdos846.NonTrilinearFor, Erdos846.A_set, HDiv.hDiv
Proof uses: Finset, HasSubset.Subset, Set, LT.lt, Prod.fst, Prod.snd, Eq, Decidable.byContradiction, Not, Ne, And.left, Iff, Collinear, ENNReal, Insert.insert, Singleton.singleton, Erdos846.FormsTriangle, Exists, And, Membership.mem and 114 more
150 instances, coercions and auxiliary constants left out.

Tactic trace: 69 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.weakly_nontrilinear_coloring line 774 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Erdos846.WeaklyNonTrilinear, Exists, And, Membership.mem, LT.lt, Ne, Eq, Not, Collinear, ENNReal, Insert.insert, Singleton.singleton
Proof uses: Finset, SupSet.sSup, EuclideanGeometry.NonTrilinear, List, Finset.toList, List.length, List.findIdx, Decidable.decide, Exists.intro, And.intro, Eq.symm, Iff.mpr, Bool, Bool.true, List.findIdx_lt_length, of_eq_true, Eq.trans, True, congr, congrArg and 27 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.ramsey_sequence line 804 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Nat, LT.lt, Exists, And, StrictMono, Eq, Prod.mk
Proof uses: Set.Finite.exists_lt_map_eq_of_forall_mem, setOf, Set.finite_lt_nat, Exists.elim, Membership.mem, Set, Set.Icc, OfNat.ofNat, Filter.Tendsto, Function.comp, Filter.atTop, nhds, IsCompact.tendsto_subseq, isCompact_pi_infinite, CompactIccSpace.isCompact_Icc, And.intro, LE.le, zero_le, le_of_lt, Eq.mpr and 34 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.pidgeonhole_3 line 817 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Exists, And, Eq
Proof uses: Eq.mpr, id, congrArg, funext, Exists.elim, Membership.mem, Set, setOf, StrictMono, Filter.Tendsto, Function.comp, Filter.atTop, nhds, IsCompact.isSeqCompact, Set.Finite.isCompact, Set.finite_lt_nat, Filter.Eventually, forall_congr, Eq.trans, implies_congr and 16 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.ramsey_for_triangles line 824 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Nat, LT.lt, Exists, And, Eq, Prod.mk
Proof uses: StrictMono, Erdos846.ramsey_sequence, HAdd.hAdd, OfNat.ofNat, Decidable.byContradiction, Not, Eq.mpr, id, congrArg, Eq.symm, Erdos846.pidgeonhole_3, Exists.intro, lt_trans, And.intro
10 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.A_set_not_weakly line 850 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Nat, EuclideanSpace, Real, Fin, OfNat.ofNat, Erdos846.IsGoodMap, Not, Erdos846.WeaklyNonTrilinear, Erdos846.A_set
Proof uses: Exists, And, Membership.mem, Set, LT.lt, Ne, Eq, Collinear, ENNReal, Insert.insert, Singleton.singleton, Erdos846.weakly_nontrilinear_coloring, False, dite, Prod.fst, Prod.snd, HAdd.hAdd, id, ite, Eq.mpr and 20 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 63 steps
Open to load the checked before-and-after goal states.
lemma Erdos846.target_false line 897 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Not, Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, GT.gt, Set.Infinite, Erdos846.NonTrilinearFor, Erdos846.WeaklyNonTrilinear
Proof uses: Exists, Prod, Erdos846.IsGoodMap, Erdos846.exists_good_map, False, Erdos846.A_set, Erdos846.A_set_infinite, HDiv.hDiv, Erdos846.A_set_nontrilinear, 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 and 5 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem Erdos846.target_theorem_0 Erdős problem 846: robustly non-collinear sets need not split into finitely many general-position sets line 909 source
L4DEL explanation
Three points in A are collinear if and only if their corresponding edges form a triangle in K∞.
— Human-written proof companion for Erdős 846
A cannot be separated into finitely many subsets such that each subset has no three points collinear
— Moe Putterman, Mehtaab Sawhney, and Gregory Valiant (2026), arXiv v1 abstract
The asserted implication is false. An infinite planar set can have the property that every finite subset contains a line-free subset of at least half its size, yet the whole set is not a finite union of sets with no three collinear.
1. Map each edge of the countably infinite complete graph to a planar point using a rapidly growing algebraic parametrization.
2. The construction makes three image points collinear exactly when their three edges form a triangle.
3. Triangle-free subgraphs supply large non-collinear subsets, while finite colourings of the complete graph force a monochromatic triangle and rule out any finite decomposition.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written proof companion for Erdős 846, Erdős Problems 846 source record, Moe Putterman, Mehtaab Sawhney, and Gregory Valiant (2026), arXiv v1 abstract
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Iff, False, Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, GT.gt, Set.Infinite, Erdos846.NonTrilinearFor, Erdos846.WeaklyNonTrilinear
Proof uses: Iff.intro, False.elim, Not, Erdos846.target_false
8 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem target_theorem_0
  : answer(
  -- EVOLVE-VALUE-START
  False
  -- EVOLVE-VALUE-END
  ) ↔ ∀ᵉ (A : Set ℝ²) (ε > 0), A.Infinite → NonTrilinearFor A ε → WeaklyNonTrilinear A := by
…
```
Mentions: Erdos846.NonTrilinearFor, Erdos846.WeaklyNonTrilinear