Compfiles/Imo1978P6.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1978, Problem 6

An international society has its members from six different countries. The list of members has 1978 names, numbered $1, 2, \ldots, 1978$. Prove that there is at least one member whose number is the sum of the numbers of two (not necessarily distinct) members from his own country.

Imports (2)
Imported by 1 file
  1. theorem Imo1978P6.Nat.ceilDiv_pos line 31 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, CeilDiv.ceilDiv

    Proof uses: Decidable.byContradiction, Not, False.elim, False, Eq.mp, Eq.trans, congrArg, id, Eq, LE.le, HMul.hMul, MulZeroClass.mul_zero, propext, ceilDiv_le_iff_le_mul

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  2. abbrev Imo1978P6.Name line 38 source

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

    Statement uses: Nat

    Proof uses: Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat

    5 instances, coercions and auxiliary constants left out.

  3. abbrev Imo1978P6.members_of line 42 source

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

    Statement uses: Nat, Imo1978P6.Name, Fin, Finset

    Proof uses: Finset.filter, Eq, Finset.univ, Finset.Icc, OfNat.ofNat

    5 instances, coercions and auxiliary constants left out.

  4. def Imo1978P6.motive line 45 source

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

    Statement uses: Nat, Imo1978P6.Name, Fin, Finset

    Proof uses: Exists, And, Membership.mem, Eq, Finset.Icc, OfNat.ofNat, HAdd.hAdd, Subtype.mk, Disjoint, Finset.image, LE.le, Finset.card

    12 instances, coercions and auxiliary constants left out.

  5. def Imo1978P6.motive' line 51 source

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

    Statement uses: Nat, Imo1978P6.Name, Fin

    Proof uses: Exists, Finset, And, Eq, Finset.card, Imo1978P6.motive

  6. theorem Imo1978P6.induction_begin line 53 source

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

    Statement uses: Nat, Imo1978P6.Name, Fin, Imo1978P6.motive', OfNat.ofNat

    Proof uses: Exists.intro, Finset, And, Eq, Finset.card, Imo1978P6.motive, EmptyCollection.emptyCollection, And.intro, of_eq_true, eq_self, id, Membership.mem, Exists, Finset.Icc, HAdd.hAdd, Subtype.mk, Disjoint, Finset.image, LE.le, Finset.univ and 23 more

    47 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  7. theorem Imo1978P6.induction_end line 59 source

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

    Statement uses: Nat, Imo1978P6.Name, Fin, LT.lt, OfNat.ofNat, Imo1978P6.motive', False

    Proof uses: Finset, Eq, Finset.card, Membership.mem, Exists, And, Finset.Icc, HAdd.hAdd, Subtype.mk, Disjoint, Finset.image, LE.le, Finset.univ, Finset.eq_univ_of_card, of_eq_true, Fintype.card, Eq.trans, True, congr, congrArg and 8 more

    23 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  8. theorem Imo1978P6.induction_step line 70 source

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

    Statement uses: Nat, Imo1978P6.Name, Fin, NeZero, Eq, Ne, HAdd.hAdd, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, LT.lt, Imo1978P6.motive', HSub.hSub, CeilDiv.ceilDiv

    Proof uses: Finset.card, Exists, And, Subtype.mk, Disjoint, Finset.image, LE.le, Not, Inter.inter, Imo1978P6.members_of, Subtype, Set, Set.image, Finset.filter, Finset.univ, Fintype.exists_lt_card_fiber_of_mul_lt_card, lt_of_le_of_lt, HMul.hMul, Fintype.card, Nat.mul_le_mul_right and 112 more

    172 instances, coercions and auxiliary constants left out.

    Tactic trace: 192 steps

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

  9. def Imo1978P6.compute_k line 231 source

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

    Statement uses: Nat

    2 instances, coercions and auxiliary constants left out.

  10. theorem Imo1978P6.compute_finite_induction line 236 source

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

    Statement uses: Nat, Imo1978P6.Name, Fin, NeZero, Eq, Ne, HAdd.hAdd, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, LT.lt, Imo1978P6.compute_k, False

    Proof uses: LE.le, Nat.decreasingInduction', Mathlib.Tactic.Contrapose.contrapose₁, HSub.hSub, CeilDiv.ceilDiv, Eq.mpr, Not, id, implies_congr, congrArg, Eq.mp, propext, nonpos_iff_eq_zero, of_eq_true, Eq.trans, True, congrFun', zero_ceilDiv, zero_tsub, Imo1978P6.compute_k.eq_def and 6 more

    51 instances, coercions and auxiliary constants left out.

    Tactic trace: 20 steps

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

  11. problem Imo1978P6.imo1978_p6 line 263 source

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

    Statement uses: Subtype, Nat, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Fin, Exists, And, Eq, HAdd.hAdd

    Proof uses: Decidable.byContradiction, Not, Imo1978P6.compute_finite_induction, Eq.mp, Ne, Eq.trans, binderNameHint, forall_congr, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl, of_decide_eq_true, LT.lt, Imo1978P6.compute_k, id, Bool, Decidable.decide, Bool.true

    25 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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