Compfiles/Imo1985P4.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1985, Problem 4

Given a set M of 1985 distinct positive integers, none of which has a prime divisor greater than 23, prove that M contains a subset of 4 elements whose product is the 4th power of an integer.

Imports (2)
Imported by 1 file
  1. lemma Imo1985P4.extended_pigeonhole line 31 source

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

    Statement uses: DecidableEq, Finset, Membership.mem, Nat, LE.le, HSub.hSub, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Finset.card, Exists, And, Eq, Set.PairwiseDisjoint, id

    Proof uses: Nat.recAux, Exists.intro, EmptyCollection.emptyCollection, of_eq_true, Eq.trans, True, congr, congrArg, eq_self, forall_congr, False, implies_congr, Eq.refl, implies_true, Set, congrFun', Finset.coe_empty, and_self, SDiff.sdiff, Finset.disjiUnion and 45 more

    69 instances, coercions and auxiliary constants left out.

    Tactic trace: 92 steps

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

  2. lemma Imo1985P4.double_pigeonhole line 115 source

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

    Statement uses: DecidableEq, Finset, Membership.mem, LE.le, Nat, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Finset.card, Exists, And, Eq, Disjoint

    Proof uses: HSub.hSub, Set.PairwiseDisjoint, id, Imo1985P4.extended_pigeonhole, LT.lt, Set.MapsTo, Set, Eq.mpr, congrArg, propext, Finset.mem_coe, Eq.mp, Ne, Finset.exists_ne_map_eq_of_card_lt_of_maps_to, Exists.intro, And.intro

    33 instances, coercions and auxiliary constants left out.

    Tactic trace: 28 steps

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

  3. def Imo1985P4.pow_of_kth_prime_mod_two line 143 source

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

    Statement uses: Nat

    Proof uses: HMod.hMod, padicValNat, Nat.nth, Nat.Prime, OfNat.ofNat

    3 instances, coercions and auxiliary constants left out.

  4. def Imo1985P4.two_pow_k_finset line 146 source

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

    Statement uses: Nat, Finset, Membership.mem, Finset.range

    Proof uses: Finset.pi, OfNat.ofNat

    4 instances, coercions and auxiliary constants left out.

  5. def Imo1985P4.pow_of_first_k_prime_mod_two line 148 source

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

    Statement uses: Nat, Membership.mem, Finset, Finset.range

    Proof uses: Imo1985P4.pow_of_kth_prime_mod_two

    4 instances, coercions and auxiliary constants left out.

  6. lemma Imo1985P4.pow_of_first_k_prime_mod_two_mem_two_pow_k_finset line 151 source

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

    Statement uses: Nat, Membership.mem, Finset, Finset.range, Imo1985P4.two_pow_k_finset, Imo1985P4.pow_of_first_k_prime_mod_two

    Proof uses: Eq.mpr, Finset.pi, OfNat.ofNat, id, Eq, congrArg, Imo1985P4.two_pow_k_finset.eq_1, propext, Finset.mem_pi, LT.lt, HMod.hMod, padicValNat, Nat.nth, Nat.Prime, Nat.mod_lt, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  7. lemma Imo1985P4.square_of_pow_of_pow_of_kth_prime_mod_two_eq line 159 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, Eq, Imo1985P4.pow_of_kth_prime_mod_two, Exists, HMul.hMul, HPow.hPow

    Proof uses: Finset.prod, Finset.filter, Nat.Prime, Finset.range, HAdd.hAdd, HDiv.hDiv, padicValNat, Exists.intro, Nat.mul_ne_zero, Eq.mpr, id, congrArg, Eq.symm, Nat.prod_pow_prime_padicValNat, Finset.prod_pow, Finset.prod_congr, rfl, Finset, Membership.mem, And.right and 20 more

    41 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

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

  8. lemma Imo1985P4.padicValNat_eq_zero_of_divisors line 184 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, And, Nat.Prime, Dvd.dvd, LE.le, Nat.nth, LT.lt, Eq, padicValNat

    Proof uses: Decidable.byContradiction, Not, Fact, Fact.mk, Nat.prime_nth_prime, And.intro, Eq.mp, congrArg, Eq.symm, propext, dvd_iff_padicValNat_ne_zero, Nat.nth_le_nth, Nat.infinite_setOfPred_prime

    10 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  9. lemma Imo1985P4.square_of_pow_of_first_k_prime_mod_two_eq line 194 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, Eq, Membership.mem, Finset, Finset.range, HAdd.hAdd, Imo1985P4.pow_of_first_k_prime_mod_two, And, Nat.Prime, Dvd.dvd, LE.le, Nat.nth, Exists, HMul.hMul, HPow.hPow

    Proof uses: Imo1985P4.pow_of_kth_prime_mod_two, dite, Eq.mp, congrArg, propext, funext_iff, Iff.mpr, Nat.succ, Finset.mem_range_succ_iff, Not, id, Eq.mpr, HMod.hMod, padicValNat, Imo1985P4.padicValNat_eq_zero_of_divisors, LT.lt, Eq.refl, Imo1985P4.square_of_pow_of_pow_of_kth_prime_mod_two_eq

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  10. lemma Imo1985P4.prod_square_of_pow_of_first_k_prime_mod_two_eq line 216 source

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

    Statement uses: Finset, Nat, Membership.mem, And, Nat.Prime, Dvd.dvd, LE.le, Nat.nth, LT.lt, OfNat.ofNat, Eq, Finset.card, Exists, Finset.range, HAdd.hAdd, Imo1985P4.pow_of_first_k_prime_mod_two, Finset.prod, id, HPow.hPow

    Proof uses: Ne, Insert.insert, Singleton.singleton, Eq.mp, congrArg, propext, Finset.card_eq_two, Eq.mpr, HMul.hMul, Finset.prod_insert, Iff.mpr, Not, Finset.notMem_singleton, Finset.prod_singleton, id_eq, of_eq_true, Eq.trans, Or, True, congrFun' and 7 more

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  11. lemma Imo1985P4.sqrt_prod_subset_ne_zero line 238 source

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

    Statement uses: Finset, Nat, Membership.mem, LT.lt, OfNat.ofNat, LE.le, Eq, Finset.prod, id, HPow.hPow, Ne

    Proof uses: Mathlib.Tactic.Contrapose.contrapose₃, Not, Eq.mpr, congrArg, congr, Finset.prod_congr, Eq.refl, zero_pow, of_eq_true, Eq.trans, False, True, not_false_eq_true, Exists, And, propext, Finset.prod_eq_zero_iff, binderNameHint, forall_congr, Mathlib.Tactic.Push.not_and_eq and 2 more

    48 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  12. lemma Imo1985P4.sqrt_divisors_subset line 249 source

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

    Statement uses: Finset, Nat, Membership.mem, And, Nat.Prime, Dvd.dvd, LE.le, Nat.nth, Eq, Finset.prod, id, HPow.hPow, OfNat.ofNat

    Proof uses: Exists, Prime.exists_mem_finset_dvd, Nat.Prime.prime, Eq.mp, congrArg, Eq.symm, propext, Prime.dvd_pow_iff_dvd, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, And.intro

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  13. theorem Imo1985P4.generalized line 259 source

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

    Statement uses: Finset, Nat, LE.le, HAdd.hAdd, HMul.hMul, OfNat.ofNat, HPow.hPow, Finset.card, Membership.mem, LT.lt, And, Nat.Prime, Dvd.dvd, Nat.nth, Exists, Eq, Finset.prod, id

    Proof uses: Finset.range, Imo1985P4.pow_of_first_k_prime_mod_two, Imo1985P4.two_pow_k_finset, Imo1985P4.pow_of_first_k_prime_mod_two_mem_two_pow_k_finset, Nat.sqrt, Eq.mpr, Finset.pi, congrArg, Imo1985P4.two_pow_k_finset.eq_1, Finset.card_pi, Finset.card_range, Finset.prod_const, Disjoint, Imo1985P4.double_pigeonhole, Exists.intro, Union.union, And.intro, Finset.union_subset, Eq.mp, Eq.symm and 14 more

    50 instances, coercions and auxiliary constants left out.

    Tactic trace: 32 steps

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

  14. problem Imo1985P4.imo1985_p4 line 299 source

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

    Statement uses: Finset, Nat, Eq, Finset.card, OfNat.ofNat, Membership.mem, LT.lt, Nat.primeFactors, LE.le, Exists, And, Finset.prod, id, HPow.hPow

    Proof uses: Nat.Prime, Dvd.dvd, Eq.mpr, congrArg, Eq.symm, propext, Nat.mem_primeFactors_of_ne_zero, Ne.symm, LT.lt.ne, Nat.nth, Nat.count, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, Nat.nth_count, HAdd.hAdd, HMul.hMul, of_eq_true and 16 more

    39 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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