Compfiles/Imo2021P6.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2021, Problem 6

Let m ≥ 2 be an integer, A a finite set of integers (not necessarily positive) and B₁, B₂, ... Bₘ subsets of A. Suppose that for every k = 1, 2, ..., m, the sum of the elements of Bₖ is m^k. Prove that A contains at least m/2 elements.

Imports (2)
Imported by 1 file
  1. def Imo2021P6.incidenceCoeff line 36 source

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

    Statement uses: Nat, Fin, Finset, Int

    Proof uses: ite, Membership.mem, OfNat.ofNat

    5 instances, coercions and auxiliary constants left out.

  2. lemma Imo2021P6.term_mul_subset_indicator line 38 source

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

    Statement uses: Nat, Int, Fin, Finset, Eq, HMul.hMul, ite, Membership.mem, OfNat.ofNat, Imo2021P6.incidenceCoeff

    8 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  3. lemma Imo2021P6.small_coeffs_eq_zero_of_sum_pow_eq_zero line 41 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Int, LT.lt, abs, Eq, Finset.sum, Finset.univ, HMul.hMul, HPow.hPow

    Proof uses: Nat.recAux, Fin.elim0, HAdd.hAdd, Dvd.dvd, Fin.succ, Finset.dvd_sum, Membership.mem, Finset, of_eq_true, Eq.trans, True, Function.swap, Eq.mp, congrFun', congrArg, pow_one, pow_dvd_pow, dvd_mul_of_dvd_right, Neg.neg, Fin.sum_univ_succ and 18 more

    109 instances, coercions and auxiliary constants left out.

    Tactic trace: 32 steps

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

  4. lemma Imo2021P6.card_pos_of_sum_powers line 71 source

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

    Statement uses: Nat, Finset, Int, Fin, LE.le, OfNat.ofNat, Eq, Finset.sum, HPow.hPow, HAdd.hAdd, LT.lt, Finset.card

    Proof uses: Decidable.byContradiction, Not, Fin.mk, EmptyCollection.emptyCollection

    37 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  5. lemma Imo2021P6.subset_sum_eq_subtype_sum line 77 source

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

    Statement uses: Finset, Int, LE.le, Eq, Finset.sum, Subtype, Membership.mem, Finset.univ, ite, OfNat.ofNat

    Proof uses: of_eq_true, Finset.attach, Eq.trans, True, congrArg, Eq.symm, Finset.sum_attach, eq_self, Eq.mpr, id, Finset.filter, Finset.sum_filter, AddCommMonoid, Eq.rec, Eq.refl

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  6. lemma Imo2021P6.siegel_incidence_relation line 86 source

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

    Statement uses: Nat, Finset, Int, Fin, LE.le, OfNat.ofNat, Eq, Finset.sum, HPow.hPow, HAdd.hAdd, LT.lt, HMul.hMul, Finset.card, Exists, And, Ne, Subtype, Membership.mem, Finset.univ, Imo2021P6.incidenceCoeff and 1 more

    Proof uses: Matrix, Fintype.card, Eq.mpr, id, congr, congrArg, Fintype.card_coe, Fintype.card_fin, Imo2021P6.card_pos_of_sum_powers, Finset.Nonempty, Eq.trans, Eq.mp, Matrix.mulVec, Real, Norm.norm, Max.max, Matrix.seminormedAddCommGroup, HDiv.hDiv, HSub.hSub, Int.Matrix.exists_ne_zero_int_vec_norm_le and 94 more

    192 instances, coercions and auxiliary constants left out.

    Tactic trace: 42 steps

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

  7. lemma Imo2021P6.incidence_relation_gives_power_relation line 125 source

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

    Statement uses: Nat, Finset, Int, Fin, LE.le, Eq, Finset.sum, HPow.hPow, HAdd.hAdd, OfNat.ofNat, Subtype, Membership.mem, Finset.univ, HMul.hMul, Imo2021P6.incidenceCoeff

    Proof uses: Trans.trans, ite, Finset.sum_congr, rfl, Eq.mpr, id, congrArg, Imo2021P6.subset_sum_eq_subtype_sum, Eq.refl, congr, Finset.mul_sum, Finset.sum_comm, Imo2021P6.term_mul_subset_indicator, Eq.mp, Finset.attach, Finset.sum_const_zero

    60 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  8. lemma Imo2021P6.small_relation_eq_zero line 141 source

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

    Statement uses: Nat, Fin, Int, LE.le, OfNat.ofNat, LT.lt, abs, Eq, Finset.sum, Finset.univ, HMul.hMul, HPow.hPow, HAdd.hAdd

    Proof uses: Or.resolve_left, Iff.mp, Or, mul_eq_zero, funext, Imo2021P6.small_coeffs_eq_zero_of_sum_pow_eq_zero

    56 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  9. problem Imo2021P6.imo2021_p6 line 152 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Finset, Int, Fin, Eq, Finset.sum, HPow.hPow, HAdd.hAdd, HMul.hMul, Finset.card

    Proof uses: Decidable.byContradiction, Not, And, Ne, Subtype, Membership.mem, Finset.univ, Imo2021P6.incidenceCoeff, LT.lt, abs, Exists, False, Imo2021P6.siegel_incidence_relation, Eq.mp, Imo2021P6.incidence_relation_gives_power_relation, Imo2021P6.small_relation_eq_zero

    55 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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