Compfiles/Bulgaria1998P1.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Bulgarian Mathematical Olympiad 1998, Problem 1

We will be considering colorings in 2 colors of n (distinct) points A₁, A₂, ..., Aₙ. Call such a coloring "good" if there exist three points Aᵢ, Aⱼ, A₂ⱼ₋ᵢ, 1 ≤ i < 2j - i ≤ n, which are colored the same color.

Find the least natural number n (n ≥ 3) such that all colorings of n points are good.

Imports (2)
Imported by 1 file
  1. abbrev Bulgaria1998P1.coloring_is_good line 30 source

    no axioms what this means

    Statement uses: Nat, Set.Icc, OfNat.ofNat, Fin

    Proof uses: Exists, And, LT.lt, Membership.mem, Set, HSub.hSub, HMul.hMul, Eq, Subtype.mk

    14 instances, coercions and auxiliary constants left out.

  2. abbrev Bulgaria1998P1.all_colorings_are_good line 36 source

    no axioms what this means

    Statement uses: Nat

    Proof uses: And, LE.le, OfNat.ofNat, Set.Icc, Fin, Bulgaria1998P1.coloring_is_good

    4 instances, coercions and auxiliary constants left out.

  3. lemma Bulgaria1998P1.lemma1 line 41 source

    standard axioms: propext what this means

    Statement uses: Nat, LE.le, Bulgaria1998P1.all_colorings_are_good

    Proof uses: And.intro, OfNat.ofNat, Set.Icc, Fin, Bulgaria1998P1.coloring_is_good, LE.le.trans, And.left, Subtype.mk, Membership.mem, Set, Eq.mpr, And, id, Eq, congrArg, propext, Set.mem_Icc, Subtype.prop, And.right, Exists and 14 more

    27 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

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

  4. def Bulgaria1998P1.coloring_of_eight line 63 source

    standard axioms: propext what this means

    Statement uses: Nat, Set.Icc, OfNat.ofNat, Fin

    Proof uses: Bulgaria1998P1.coloring_of_eight.match_1, Membership.mem, Set

    9 instances, coercions and auxiliary constants left out.

  5. lemma Bulgaria1998P1.lemma2 line 74 source

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

    Statement uses: Exists, Nat, Set.Icc, OfNat.ofNat, Fin, Not, Bulgaria1998P1.coloring_is_good

    Proof uses: Exists.intro, Bulgaria1998P1.coloring_of_eight, of_decide_eq_true, And, LT.lt, Membership.mem, Set, HSub.hSub, HMul.hMul, Eq, Subtype.mk, id, Bool, Decidable.decide, Bool.true, Eq.refl

    25 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  6. determine Bulgaria1998P1.solution_value line 81 source

    no axioms what this means

    Statement uses: Nat

    Proof uses: OfNat.ofNat

    1 instances, coercions and auxiliary constants left out.

  7. def Bulgaria1998P1.check9 line 83 source
  8. def Bulgaria1998P1.toFin9 line 91 source
  9. lemma Bulgaria1998P1.of_check9 line 94 source
  10. problem Bulgaria1998P1.bulgaria1998_p1 line 116 source

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

    Statement uses: IsLeast, Nat, Set.ofPred, Bulgaria1998P1.all_colorings_are_good, Bulgaria1998P1.solution_value

    Proof uses: And.intro, Membership.mem, Set, lowerBounds, Eq.mpr, id, Eq, congrArg, Set.mem_ofPred_eq, LE.le, OfNat.ofNat, Set.Icc, Fin, Bulgaria1998P1.coloring_is_good, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, propext and 12 more

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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