Compfiles/Imo1981P2.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1981, Problem 2

Let $1 \le r \le n$ and consider all subsets of $r$ elements of the set $\{ 1, 2, \ldots , n \}$. Each of these subsets has a smallest member. Let $F(n,r)$ denote the arithmetic mean of these smallest numbers; prove that \[ F(n,r) = \frac{n+1}{r+1}. \]

Imports (2)
Imported by 1 file
  1. def Imo1981P2.arith_mean line 32 source

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

    Statement uses: Multiset, Nat, Rat

    Proof uses: HDiv.hDiv, Multiset.sum, Multiset.card

    5 instances, coercions and auxiliary constants left out.

  2. def Imo1981P2.F line 34 source

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

    Statement uses: Nat, Rat

    Proof uses: Imo1981P2.arith_mean, Multiset.map, Finset, Option.getD, Finset.min, OfNat.ofNat, Finset.val, Finset.powersetCard, Finset.Icc

    4 instances, coercions and auxiliary constants left out.

  3. def Imo1981P2.eraseMin line 40 source

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

    Statement uses: Finset, Nat

    Proof uses: dite, Finset.Nonempty, Finset.erase, Finset.min', Not

    3 instances, coercions and auxiliary constants left out.

  4. theorem Imo1981P2.insert_min'_eraseMin line 47 source

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

    Statement uses: Finset, Nat, Finset.Nonempty, Eq, Insert.insert, Finset.min', Imo1981P2.eraseMin

    Proof uses: id, Eq.mpr, dite, Finset.erase, Not, of_eq_true, eq_true, congrFun', congrArg, dite_eq_left_of_eq_true, Finset.insert_erase, Finset.min'_mem

    7 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  5. theorem Imo1981P2.eraseMin_insert line 53 source

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

    Statement uses: Finset, Nat, Membership.mem, LT.lt, Eq, Imo1981P2.eraseMin, Insert.insert

    Proof uses: id, Eq.mpr, dite, Finset.Nonempty, Finset.erase, Finset.min', Not, of_eq_true, congrFun', congrArg, dite_eq_left_of_eq_true, Eq.substr, True, True.intro, Eq.trans, forall_prop_domain_congr, Eq.refl, And, LE.le, propext and 2 more

    22 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  6. theorem Imo1981P2.eraseMin_mem_powersetCard line 64 source

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

    Statement uses: Nat, Finset, Membership.mem, Finset.powersetCard, HAdd.hAdd, OfNat.ofNat, Finset.Icc, Imo1981P2.eraseMin

    Proof uses: And, Eq, Finset.card, Not, And.intro, id, dite, Finset.Nonempty, Finset.erase, Finset.min', Eq.mpr, congrFun', congrArg, dite_eq_left, HSub.hSub, Finset.card_erase_of_mem, Finset.min'_mem, dite_eq_right, Ne, propext and 14 more

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 22 steps

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

  7. abbrev Imo1981P2.V line 81 source

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

    Statement uses: Nat

    Proof uses: Sum, Subtype, Finset, Membership.mem, Finset.powersetCard, HAdd.hAdd, OfNat.ofNat, Finset.Icc

    7 instances, coercions and auxiliary constants left out.

  8. def Imo1981P2.G line 83 source

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

    Statement uses: Nat, SimpleGraph, Imo1981P2.V

    Proof uses: SimpleGraph.mk, Imo1981P2.G.match_1, Prod, Prod.mk, Subtype, Finset, Membership.mem, Finset.powersetCard, HAdd.hAdd, OfNat.ofNat, Finset.Icc, Eq, Imo1981P2.eraseMin, False

    10 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  9. instance Imo1981P2.(instance at line 91) line 91 source
  10. theorem Imo1981P2.bipartite_edge line 97 source

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

    Statement uses: SimpleGraph, Sum, LE.le, completeBipartiteGraph, Sym2, Membership.mem, Set, SimpleGraph.edgeSet, Exists, Eq, Sym2.mk, Sum.inl, Sum.inr

    Proof uses: Eq.mpr, id, congrArg, Eq.symm, propext, Sym2.exists, Exists.intro, Eq.refl, SimpleGraph.Adj, Iff.mp, SimpleGraph.le_iff_adj, Eq.mp, SimpleGraph.mem_edgeSet, Or.elim, And, Bool, Sum.isLeft, Bool.true, Sum.isRight, Sum.getLeft and 1 more

    10 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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

  11. theorem Imo1981P2.G.bipartite line 115 source

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

    Statement uses: Nat, LE.le, SimpleGraph, Imo1981P2.V, Imo1981P2.G, completeBipartiteGraph, Subtype, Finset, Membership.mem, Finset.powersetCard, HAdd.hAdd, OfNat.ofNat, Finset.Icc

    Proof uses: Eq.mpr, SimpleGraph.Adj, id, Eq, congrArg, propext, SimpleGraph.le_iff_adj

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  12. theorem Imo1981P2.G.card_edgeFinset line 120 source

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

    Statement uses: Nat, Eq, Finset.card, Sym2, Imo1981P2.V, SimpleGraph.edgeFinset, Imo1981P2.G, Subtype, Finset, Membership.mem, Finset.powersetCard, HAdd.hAdd, OfNat.ofNat, Finset.Icc, Nat.choose

    Proof uses: Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, HSub.hSub, Nat.card_Icc, tsub_zero, eq_self, Eq.symm, Finset.card_powersetCard, propext, eq_comm, Finset.card_bij, Sym2.mk, Sum.inl, Subtype.mk, Sum.inr, Imo1981P2.eraseMin and 39 more

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  13. theorem Imo1981P2.G.degree_b line 135 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Subtype, Finset, Membership.mem, Finset.powersetCard, Finset.Icc, Eq, WithTop, SimpleGraph.degree, Imo1981P2.V, Imo1981P2.G, Sum.inr, HAdd.hAdd, Set, SimpleGraph.neighborSet, Finset.min

    Proof uses: Option.none, Eq.mp, Top.top, EmptyCollection.emptyCollection, congrArg, propext, Finset.min_eq_top, Option, WithTop.none_eq_top, Option.some, Finset.min_le_of_eq, Finset.mem_of_min, NatCast, Eq.rec, Eq.refl, Eq.mpr, Finset.card, SimpleGraph.neighborFinset, id, SimpleGraph.degree.eq_1 and 61 more

    58 instances, coercions and auxiliary constants left out.

    Tactic trace: 54 steps

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

  14. problem Imo1981P2.imo1981_p2 line 187 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Rat, Imo1981P2.F, HDiv.hDiv, HAdd.hAdd

    Proof uses: id, Imo1981P2.arith_mean, Multiset.map, Finset, Option.getD, Finset.min, Finset.val, Finset.powersetCard, Finset.Icc, Eq.mpr, Multiset.sum, Multiset.card, Finset.sum, Nat.choose, congrFun', congrArg, congr, Nat.cast_sum, Eq.trans, Multiset.card_map and 138 more

    154 instances, coercions and auxiliary constants left out.

    Tactic trace: 22 steps

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