Compfiles/Imo1966P1.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1966, Problem 1.

In a mathematical contest, three problems, A, B, C were posed. Among the participants there were 25 students who solved at least one problem each. Of all the contestants who did not solve problem A, the number who solved B was twice the number who solved C. The number of students who solved only problem A was one more than the number of students who solved A and at least one other problem. Of all students who solved just one problem, half did not solve problem A. How many students solved only problem B?

Imports (2)
Imported by 1 file
  1. example Imo1966P1.(example at line 36) line 36 source

    Source comment

    outline of the proof, modified from https://prase.cz/kalva/imo/isoln/isoln661.html
    example (a b c d e : ℕ)
  (_ : a + b + c + d + e = 25)
  (h2 : b + d = 2 * (c + d))
  (h3 : a = 1 + 25 - a - b - c - d)
  (h4 : a = b + c) : b = 6 := by lia
  2. lemma Imo1966P1.lemma2 line 42 source

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

    Statement uses: DecidableEq, Finset, Eq, Union.union, Inter.inter, SDiff.sdiff

    Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, Or, And, Not, id, congrArg, Eq.trans, congr, Iff.intro, Iff.mpr, Classical.or_iff_not_imp_left, And.intro, False, Iff.mp, Decidable.not_and_iff_not_or_not', False.elim

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  3. lemma Imo1966P1.lemma4 line 45 source

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

    Statement uses: DecidableEq, Finset, Eq, SDiff.sdiff, Inter.inter

    Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, And, Not, id, congr, congrArg, Eq.trans, congrFun', Iff.intro, And.intro

    9 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  4. lemma Imo1966P1.lemma5 line 49 source

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

    Statement uses: DecidableEq, Finset, Eq, Inter.inter, SDiff.sdiff

    Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, Not, id, Eq.trans, And, congr, congrArg, congrFun', implies_congr, Eq.refl, False.elim, False

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  5. determine Imo1966P1.solution line 55 source

    no axioms what this means

    Statement uses: Nat

    Proof uses: OfNat.ofNat

    1 instances, coercions and auxiliary constants left out.

  6. problem Imo1966P1.imo1966_p1 line 57 source

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

    Statement uses: DecidableEq, Finset, Eq, Nat, Finset.card, Union.union, OfNat.ofNat, SDiff.sdiff, HMul.hMul, HAdd.hAdd, Inter.inter, Imo1966P1.solution

    Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, Or, And, Not, id, congr, congrArg, Eq.trans, congrFun', Finset.union_assoc, Iff.intro, Iff.mpr, Classical.or_iff_not_imp_left, Iff.mp, Decidable.not_and_iff_not_or_not', False.elim, Decidable.of_not_not and 20 more

    47 instances, coercions and auxiliary constants left out.

    Tactic trace: 48 steps

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