Compfiles/Imo1966P5.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1966, Problem 5

Solve the system of equations

|a_1 - a_2| x_2 +|a_1 - a_3| x_3 +|a_1 - a_4| x_4 = 1 |a_2 - a_1| x_1 +|a_2 - a_3| x_3 +|a_2 - a_4| x_4 = 1 |a_3 - a_1| x_1 +|a_3 - a_2| x_2 +|a_3 - a_4| x_4 = 1 |a_4 - a_1| x_1 +|a_4 - a_2| x_2 +|a_4 - a_3| x_3 = 1

where a_1, a_2, a_3, a_4 are four different real numbers.

Imports (2)
Imported by 1 file
  1. def Imo1966P5.raw_order line 37 source

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

    Statement uses: Nat, Fin, Real

    Proof uses: Finset.card, Finset.filter, LT.lt, Finset.univ

    3 instances, coercions and auxiliary constants left out.

  2. lemma Imo1966P5.raw_order_lt line 40 source

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

    Statement uses: Nat, Fin, Real, LT.lt, Imo1966P5.raw_order

    Proof uses: Eq.mpr, Finset.card, Finset.filter, Finset.univ, id, Eq, congrArg, Imo1966P5.raw_order.eq_1, lt_of_le_of_ne, card_finset_fin_le, Ne, Eq.symm, Finset.card_fin, Not, ne_eq, Membership.mem, Finset, propext, Finset.card_filter_eq_iff, Exists and 9 more

    15 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  3. def Imo1966P5.order line 53 source

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

    Statement uses: Nat, Fin, Real

    Proof uses: Fin.mk, Imo1966P5.raw_order, Imo1966P5.raw_order_lt

  4. lemma Imo1966P5.bijective_order line 56 source

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

    Statement uses: Nat, Fin, Real, Function.Injective, Function.Bijective, Imo1966P5.order

    Proof uses: Eq.mpr, And, Eq, Fintype.card, id, congrArg, propext, Fintype.bijective_iff_injective_and_card, And.intro, Mathlib.Tactic.Contrapose.contrapose₁, Not, Ne, LT.lt, Or, Classical.em, ne_of_lt, Finset.card, Finset.filter, Finset.univ, Imo1966P5.raw_order and 29 more

    23 instances, coercions and auxiliary constants left out.

    Tactic trace: 31 steps

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

  5. def Imo1966P5.nth_smallest_index line 83 source

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

    Statement uses: Nat, Fin, Real, Function.Injective

    Proof uses: Fintype.bijInv, Imo1966P5.order, Imo1966P5.bijective_order

    2 instances, coercions and auxiliary constants left out.

  6. lemma Imo1966P5.bijective_nth_smallest_index line 87 source

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

    Statement uses: Nat, Fin, Real, Function.Injective, Function.Bijective, Imo1966P5.nth_smallest_index

    Proof uses: Fintype.bijective_bijInv, Imo1966P5.order, Imo1966P5.bijective_order

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  7. lemma Imo1966P5.order_comp_nth_smallest_index_eq_id line 91 source

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

    Statement uses: Nat, Fin, Real, Function.Injective, Eq, Function.comp, Imo1966P5.order, Imo1966P5.nth_smallest_index, id

    Proof uses: Function.RightInverse.id, Fintype.bijInv, Imo1966P5.bijective_order, Fintype.rightInverse_bijInv

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  8. lemma Imo1966P5.nth_smallest_index_comp_order_eq_id line 95 source

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

    Statement uses: Nat, Fin, Real, Function.Injective, Eq, Function.comp, Imo1966P5.nth_smallest_index, Imo1966P5.order, id

    Proof uses: Function.LeftInverse.id, Fintype.bijInv, Imo1966P5.bijective_order, Fintype.leftInverse_bijInv

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  9. def Imo1966P5.nth_smallest line 99 source

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

    Statement uses: Nat, Fin, Real, Function.Injective

    Proof uses: Function.comp, Imo1966P5.nth_smallest_index

  10. lemma Imo1966P5.nth_smallest_strictMono line 102 source

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

    Statement uses: Nat, Fin, Real, Function.Injective, StrictMono, Imo1966P5.nth_smallest

    Proof uses: LT.lt, Eq.mpr, Function.comp, Imo1966P5.nth_smallest_index, id, Eq, congrArg, Imo1966P5.nth_smallest.eq_1, Function.comp_apply, Mathlib.Tactic.Contrapose.contrapose₁, Not, LE.le, implies_congr, Eq.symm, id_eq, Imo1966P5.order, Imo1966P5.order_comp_nth_smallest_index_eq_id, rfl, Fin.mk, Imo1966P5.raw_order and 18 more

    21 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

  11. lemma Imo1966P5.order_eq_id_of_strictMono line 117 source

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

    Statement uses: Nat, Fin, Real, StrictMono, Eq, Imo1966P5.order, id

    Proof uses: funext, Fin.ext, Eq.mpr, Fin.mk, Imo1966P5.raw_order, Imo1966P5.raw_order_lt, congrArg, Imo1966P5.order.eq_1, Fin.val_mk, id.eq_1, Finset.card, Finset.filter, LT.lt, Finset.univ, Imo1966P5.raw_order.eq_1, Finset.Iio, Eq.symm, Fin.card_Iio, Finset, Eq.rec and 11 more

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  12. lemma Imo1966P5.nth_smallest_index_eq_id_of_strictMono line 126 source

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

    Statement uses: Nat, Fin, Real, StrictMono, Eq, Imo1966P5.nth_smallest_index, StrictMono.injective, id

    Proof uses: Eq.mpr, Fintype.bijInv, Imo1966P5.order, Imo1966P5.bijective_order, congrArg, Imo1966P5.nth_smallest_index.eq_1, funext, Fin.ext, Function.LeftInverse, Fintype.leftInverse_bijInv, Eq.symm, Eq.mp, Function.LeftInverse.eq_1, Eq.rec, Eq.refl, Fintype, DecidableEq, Function.Bijective, Subsingleton.elim, Decidable and 1 more

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  13. lemma Imo1966P5.nth_smallest_nth_smallest_eq_nth_smallest line 137 source

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

    Statement uses: Nat, Fin, Real, Function.Injective, Eq, Imo1966P5.nth_smallest, StrictMono.injective, Imo1966P5.nth_smallest_strictMono

    Proof uses: Eq.mpr, Function.comp, Imo1966P5.nth_smallest_index, id, congrArg, Imo1966P5.nth_smallest.eq_1, Imo1966P5.nth_smallest_index_eq_id_of_strictMono, Function.comp_id, Eq.refl

    4 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  14. lemma Imo1966P5.order_nth_smallest_eq_id line 142 source

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

    Statement uses: Nat, Fin, Real, Function.Injective, Eq, Imo1966P5.order, Imo1966P5.nth_smallest, id

    Proof uses: Imo1966P5.order_eq_id_of_strictMono, Imo1966P5.nth_smallest_strictMono

    Tactic trace: 2 steps

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

  15. def Imo1966P5.solution_set_generalized line 147 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Real, Function.Injective, Set

    Proof uses: Singleton.singleton, ite, Or, Eq, Imo1966P5.order, Fin.mk, HSub.hSub, HDiv.hDiv, Imo1966P5.nth_smallest

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  16. theorem Imo1966P5.imo1966_p5_generalized line 155 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Real, Function.Injective, Iff, Eq, Finset.sum, Finset.univ, HMul.hMul, abs, HSub.hSub, Membership.mem, Set, Imo1966P5.solution_set_generalized

    Proof uses: StrictMono, Not, Or, Classical.em, Eq.mpr, Singleton.singleton, ite, Imo1966P5.order, Fin.mk, HDiv.hDiv, Imo1966P5.nth_smallest, id, congrArg, Imo1966P5.solution_set_generalized.eq_1, propext, Set.mem_singleton_iff, Imo1966P5.order_eq_id_of_strictMono, Function.comp, Imo1966P5.nth_smallest_index, Imo1966P5.nth_smallest.eq_1 and 179 more

    199 instances, coercions and auxiliary constants left out.

    Tactic trace: 232 steps (first 200 of 232)

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

  17. determine Imo1966P5.solution_set line 323 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Real, Function.Injective, Set

    Proof uses: Imo1966P5.solution_set_generalized

    3 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  18. problem Imo1966P5.imo1966_p5 line 327 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Real, Function.Injective, Iff, Eq, Finset.sum, Finset.univ, HMul.hMul, abs, HSub.hSub, Membership.mem, Set, Imo1966P5.solution_set

    Proof uses: Imo1966P5.imo1966_p5_generalized, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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