Compfiles/Imo1970P4.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1970, Problem 4

Determine the set of all positive integers n with the property that the set {n, n + 1, n + 2, n + 3, n + 4, n + 5} can be partitioned into two sets such that the product of the numbers in one set equals the product of the numbers in the other set.

Imports (5)
Imported by 1 file
  1. lemma Imo1970P4.no_partition line 44 source

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

    Statement uses: Nat, Finset, Eq, Union.union, Finset.Icc, HAdd.hAdd, OfNat.ofNat, Inter.inter, EmptyCollection.emptyCollection, Finset.prod, False

    Proof uses: HMul.hMul, Eq.mpr, id, congrArg, Eq.symm, Finset.prod_union, Iff.mpr, Disjoint, Finset.disjoint_iff_inter_eq_empty, Eq.refl, Prime, Nat.Prime.prime, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.minFacHelper_0, Bool.false and 72 more

    100 instances, coercions and auxiliary constants left out.

    Tactic trace: 59 steps

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

  2. determine Imo1970P4.SolutionSet line 110 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Finset, PNat

    Proof uses: EmptyCollection.emptyCollection

    1 instances, coercions and auxiliary constants left out.

  3. problem Imo1970P4.imo1970_p4 line 112 source

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

    Statement uses: PNat, Iff, Membership.mem, Finset, Imo1970P4.SolutionSet, Exists, Nat, And, Eq, Union.union, Finset.Icc, HAdd.hAdd, OfNat.ofNat, Inter.inter, EmptyCollection.emptyCollection, Finset.prod

    Proof uses: Iff.intro, absurd, Finset.notMem_empty, False.elim, Imo1970P4.no_partition

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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