Compfiles/Imo1989P6.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1989, Problem 6

A permutation $\{x_1, \ldots, x_{2n}\}$ of the set $\{1,2, \ldots, 2n\}$ where $n$ is a positive integer, is said to have property $T$ if $|x_i - x_{i + 1}| = n$ for at least one $i \in \{1,2, \ldots, 2n - 1\}$. Show that, for each $n$, there are more permutations with property $T$ than without.

Imports (3)
Imported by 1 file
  1. def Imo1989P6.T line 33 source

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

    Statement uses: Nat, Equiv.Perm, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul

    Proof uses: Exists, HSub.hSub, Eq, Nat.dist, Subtype.mk, HAdd.hAdd

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  2. instance Imo1989P6.instOne line 44 source

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

    Statement uses: Nat, NeZero, OfNat, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul

    Proof uses: OfNat.mk, Subtype.mk

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  3. def Imo1989P6.A line 46 source

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

    Statement uses: Nat, Set, Equiv.Perm, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul

    Proof uses: Set.ofPred, Not, Imo1989P6.T

    14 instances, coercions and auxiliary constants left out.

  4. def Imo1989P6.B line 49 source

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

    Statement uses: Nat, Set, Prod, Equiv.Perm, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul, HSub.hSub

    Proof uses: Set.ofPred, Imo1989P6.B.match_1, Iff, Eq, Nat.dist, Subtype.mk, HAdd.hAdd

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  5. theorem Imo1989P6.unique_ndiff line 53 source

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

    Statement uses: Nat, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul, Iff, Eq, Nat.dist, ite, LE.le, HAdd.hAdd, HSub.hSub

    Proof uses: Eq.mpr, Max.max, Min.min, id, congrFun', congrArg, Nat.dist_eq_max_sub_min

    31 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  6. def Imo1989P6.fin_equiv line 57 source

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

    Statement uses: Nat, Equiv, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul, Fin

    Proof uses: Equiv.mk, Fin.mk, HSub.hSub, Subtype.mk, HAdd.hAdd

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  7. def Imo1989P6.perm_fin_equiv line 63 source

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

    Statement uses: Nat, Equiv, Equiv.Perm, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul, Fin

    Proof uses: Equiv.equivCongr, Imo1989P6.fin_equiv

    14 instances, coercions and auxiliary constants left out.

  8. theorem Imo1989P6.one_le_val line 67 source

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

    Statement uses: Nat, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul, LE.le

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  9. theorem Imo1989P6.val_le_2n line 70 source

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

    Statement uses: Nat, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul, LE.le

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  10. def Imo1989P6.partial_cycle line 73 source

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

    Statement uses: Nat, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul, Equiv.Perm

    Proof uses: Equiv.mk, Equiv, Fin, Equiv.symm, Imo1989P6.perm_fin_equiv, Fin.cycleRange, Imo1989P6.fin_equiv

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  11. theorem Imo1989P6.partial_cycle.apply_of_eq line 79 source

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

    Statement uses: Nat, NeZero, Equiv.Perm, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul, Eq, Imo1989P6.partial_cycle

    Proof uses: id, Equiv.mk, Equiv, Fin, Equiv.symm, Imo1989P6.perm_fin_equiv, Fin.cycleRange, Imo1989P6.fin_equiv, Equiv.equivCongr, Eq.mpr, OfNat.mk, Subtype.mk, congrFun', congrArg, Eq.trans, Function.LeftInverse, funext, Equiv.equivCongr_symm, Function.RightInverse, Equiv.mk.congr_simp and 11 more

    46 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  12. theorem Imo1989P6.partial_cycle.apply_of_gt line 88 source

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

    Statement uses: Nat, NeZero, Equiv.Perm, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul, LT.lt, Eq, Imo1989P6.partial_cycle

    Proof uses: id, Equiv.mk, Equiv, Fin, Equiv.symm, Imo1989P6.perm_fin_equiv, Fin.cycleRange, Imo1989P6.fin_equiv, Eq.mpr, Equiv.equivCongr, congrFun', congrArg, Eq.trans, Function.LeftInverse, funext, Equiv.equivCongr_symm, Function.RightInverse, Equiv.mk.congr_simp, Equiv.symm_apply_apply, Fin.cycleRange_of_gt and 5 more

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  13. theorem Imo1989P6.partial_cycle.apply_of_lt line 99 source

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

    Statement uses: Nat, NeZero, Equiv.Perm, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul, LT.lt, Eq, Imo1989P6.partial_cycle, Subtype.mk, HAdd.hAdd

    Proof uses: id, Equiv.mk, Equiv, Fin, Equiv.symm, Imo1989P6.perm_fin_equiv, Fin.cycleRange, Imo1989P6.fin_equiv, Eq.mpr, Equiv.equivCongr, congrFun', congrArg, Eq.trans, Function.LeftInverse, funext, Equiv.equivCongr_symm, Function.RightInverse, Equiv.mk.congr_simp, Equiv.symm_apply_apply, Fin.cycleRange_of_lt and 19 more

    59 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

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

  14. theorem Imo1989P6.partial_cycle.symm.apply_of_eq line 119 source

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

    Statement uses: Nat, NeZero, Equiv.Perm, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul, Eq, Equiv, Equiv.symm, Imo1989P6.partial_cycle

    Proof uses: id, Equiv.mk, Fin, Imo1989P6.perm_fin_equiv, Fin.cycleRange, Imo1989P6.fin_equiv, Eq.mpr, Equiv.equivCongr, Eq.trans, congrFun', congrArg, Function.LeftInverse, funext, Equiv.equivCongr_symm, Function.RightInverse, Equiv.mk.congr_simp, Equiv.symm_apply_apply, Fin.cycleRange_of_eq, Eq.refl, Fin.mk and 10 more

    56 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  15. theorem Imo1989P6.partial_cycle.symm.apply_of_gt line 131 source

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

    Statement uses: Nat, NeZero, Equiv.Perm, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul, LT.lt, Eq, Equiv, Equiv.symm, Imo1989P6.partial_cycle

    Proof uses: id, Equiv.mk, Fin, Imo1989P6.perm_fin_equiv, Fin.cycleRange, Imo1989P6.fin_equiv, Eq.mpr, Equiv.equivCongr, Eq.trans, congrFun', congrArg, Function.LeftInverse, funext, Equiv.equivCongr_symm, Function.RightInverse, Equiv.mk.congr_simp, Equiv.symm_apply_apply, Fin.cycleRange_of_gt, Nat.sub_lt_sub_right, Imo1989P6.one_le_val and 1 more

    37 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  16. theorem Imo1989P6.partial_cycle.symm.apply_of_le line 142 source

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

    Statement uses: Nat, NeZero, Equiv.Perm, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul, LE.le, LT.lt, Eq, Equiv, Equiv.symm, Imo1989P6.partial_cycle, Subtype.mk, HSub.hSub

    Proof uses: id, Equiv.mk, Fin, Imo1989P6.perm_fin_equiv, Fin.cycleRange, Imo1989P6.fin_equiv, Eq.mpr, Equiv.equivCongr, congrFun', congrArg, Eq.trans, Function.LeftInverse, funext, Equiv.equivCongr_symm, Function.RightInverse, Equiv.mk.congr_simp, Equiv.symm_apply_apply, Eq.mp, OfNat.mk, Eq.symm and 13 more

    69 instances, coercions and auxiliary constants left out.

    Tactic trace: 30 steps

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

  17. def Imo1989P6.transform_A_to_B line 164 source

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

    Statement uses: Nat, NeZero, Equiv.Perm, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul, Imo1989P6.A, Prod, HSub.hSub, Imo1989P6.B

    Proof uses: Set, Subtype.mk, ite, LE.le, HAdd.hAdd, Eq, Nat.dist, Equiv, Equiv.symm, Prod.mk, Imo1989P6.partial_cycle

    39 instances, coercions and auxiliary constants left out.

    Tactic trace: 112 steps

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

  18. def Imo1989P6.transform_B_to_A line 233 source

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

    Statement uses: Nat, NeZero, Prod, Equiv.Perm, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul, HSub.hSub, Imo1989P6.B, Imo1989P6.A

    Proof uses: Imo1989P6.transform_B_to_A.match_1, Set, Prod.mk, Subtype.mk, HAdd.hAdd, Eq, Nat.dist, Equiv, Equiv.symm, Imo1989P6.partial_cycle

    35 instances, coercions and auxiliary constants left out.

    Tactic trace: 93 steps

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

  19. def Imo1989P6.A_equiv_B line 293 source

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

    Statement uses: Nat, NeZero, Equiv, Equiv.Perm, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul, Imo1989P6.A, Prod, HSub.hSub, Imo1989P6.B

    Proof uses: Equiv.mk, Imo1989P6.transform_A_to_B, Imo1989P6.transform_B_to_A

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 52 steps

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

  20. def Imo1989P6.embed_B line 337 source

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

    Statement uses: Nat, Function.Embedding, Prod, Equiv.Perm, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul, HSub.hSub, Imo1989P6.B, Set.ofPred, Imo1989P6.T

    Proof uses: Function.Embedding.mk, Imo1989P6.transform_B_to_A.match_1, Set, Prod.mk, Subtype.mk, Eq

    23 instances, coercions and auxiliary constants left out.

    Tactic trace: 32 steps

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

  21. theorem Imo1989P6.embed_B.not_Surjective line 367 source

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

    Statement uses: Nat, NeZero, Not, Function.Surjective, Prod, Equiv.Perm, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul, HSub.hSub, Imo1989P6.B, Set.ofPred, Imo1989P6.T, Function.Embedding, Imo1989P6.embed_B

    Proof uses: LT.lt, Nat.pos_of_neZero, Eq.mpr, Exists, Eq, id, congrArg, Function.Surjective.eq_1, propext, Classical.not_forall, ite, Subtype.mk, HAdd.hAdd, Equiv.mk, dite, congrFun', ite_congr, ite_eq_left, Eq.refl, ite_eq_right and 28 more

    103 instances, coercions and auxiliary constants left out.

    Tactic trace: 38 steps

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

  22. theorem Imo1989P6.embed_B.card line 406 source

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

    Statement uses: Nat, NeZero, LT.lt, Set.ncard, Prod, Equiv.Perm, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HMul.hMul, HSub.hSub, Imo1989P6.B, Set.ofPred, Imo1989P6.T

    Proof uses: Eq.mpr, Set.univ, id, Eq, congrArg, Eq.symm, Set.ncard_coe, Set.image, Function.Embedding, Imo1989P6.embed_B, Set.ncard_image_of_injective, Function.Embedding.injective, Set.ncard_lt_card, Set, Ne, Not, Set.range, congrFun', Eq.trans, Set.image_congr and 6 more

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  23. problem Imo1989P6.imo1989_p6 line 416 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, GT.gt, Set.ncard, Equiv.Perm, Subtype, Membership.mem, Finset, Finset.Icc, HMul.hMul, Set.ofPred, Imo1989P6.T, Not

    Proof uses: NeZero, NeZero.of_pos, Trans.trans, Eq, Imo1989P6.A, Prod, HSub.hSub, Imo1989P6.B, Imo1989P6.embed_B.card, Eq.mpr, id, congrArg, Set.ncard_congr', Equiv.symm, Imo1989P6.A_equiv_B, Eq.refl, Set, Imo1989P6.A.eq_1

    22 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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