Compfiles/Usa2014P3.lean

GitHub source file

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

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

4 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2014, Problem 3

Prove that there exists an infinite set of points

… , P₋₃, P₋₂, P₋₁, P₀, P₁, P₂, P₃, …

in the plane with the following property: For any three distinct integers a, b, and c, points Pₐ, P_b, P_c are collinear if and only if a+b+c=2014.

Imports (2)
Imported by 1 file
  1. def Usa2014P3.f Our construction (valid for x ∈ ℝ) is P_x := (x-2014/3, (x-2014/3)^3) line 42 source

    Source comment

    Our construction (valid for x ∈ ℝ) is P_x := (x-2014/3, (x-2014/3)^3).

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, EuclideanSpace, Fin, OfNat.ofNat, Nat

    Proof uses: WithLp.toLp, ENNReal, Matrix.vecCons, HSub.hSub, HDiv.hDiv, HPow.hPow, Matrix.vecEmpty

    19 instances, coercions and auxiliary constants left out.

    noncomputable def f (x : ℝ) : Pt :=
…
  2. lemma Usa2014P3.f_injective f is in an injective function (needed for Finset later) line 46 source

    Source comment

    f is in an injective function (needed for Finset later)

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, Ne, EuclideanSpace, Fin, OfNat.ofNat, Nat, Usa2014P3.f

    Proof uses: id, Eq, False.elim, False, Eq.mp, WithLp.toLp, ENNReal, Matrix.vecCons, HSub.hSub, HDiv.hDiv, HPow.hPow, Matrix.vecEmpty, Eq.trans, WithLp, WithLp.toLp.injEq, Nat.succ, And, congr, congrArg, eq_false and 5 more

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

    lemma f_injective {x y : ℝ} (hxy : x ≠ y) :
    f x ≠ f y := by
…

    Mentions: Usa2014P3.f

  3. lemma Usa2014P3.collinear_iff_sum line 52 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, Ne, Iff, Collinear, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Insert.insert, Set, Usa2014P3.f, Singleton.singleton, Eq, HAdd.hAdd

    Proof uses: Eq.mpr, id, congrArg, rfl, Usa2014P3.f_injective, Finset, LE.le, Module.finrank, Subtype, Membership.mem, Submodule, vectorSpan, propext, collinear_iff_finrank_le_one, of_eq_true, Eq.trans, True, Finset.coe_insert, Finset.coe_singleton, eq_self and 92 more

    169 instances, coercions and auxiliary constants left out.

    Tactic trace: 44 steps

    Open to load the checked before-and-after goal states.

  4. problem Usa2014P3.usa2014_p3 line 98 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Exists, Int, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, And, Ne, Iff, Collinear, ENNReal, Insert.insert, Set, Singleton.singleton, Eq, HAdd.hAdd

    Proof uses: Exists.intro, Usa2014P3.f, Eq.mpr, id, Eq.trans, implies_congr, Eq.refl, eq_of_heq, HEq, HEq.refl, Eq.symm, propext, of_eq_true, True, congrFun', congrArg, Rat, congr, Int.cast_add, Int.cast_ofNat and 5 more

    98 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

    Open to load the checked before-and-after goal states.