Compfiles/Imo1989P1.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev Imo1989P1.S line 26 source

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

   Statement uses: Finset, Nat

   Proof uses: Finset.Icc, OfNat.ofNat

   3 instances, coercions and auxiliary constants left out.

2. def Imo1989P1.n line 30 source

   no axioms what this means

   Statement uses: Nat

   Proof uses: OfNat.ofNat

   1 instances, coercions and auxiliary constants left out.

3. lemma Imo1989P1.fin_n_card line 32 source

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

   Statement uses: Eq, Nat, Fintype.card, Fin, Imo1989P1.n, OfNat.ofNat

   Proof uses: id, of_eq_true, Eq.trans, True, congrFun', congrArg, Fintype.card_fin, eq_self

   4 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

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

4. def Imo1989P1.row line 36 source

   no axioms what this means

   Statement uses: Nat, Fin, Imo1989P1.n

   Proof uses: ite, LT.lt, OfNat.ofNat, Eq, HMod.hMod, HAdd.hAdd, HMul.hMul, HSub.hSub

   13 instances, coercions and auxiliary constants left out.

5. def Imo1989P1.A line 44 source

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

   Statement uses: Fin, Imo1989P1.n, Finset, Nat

   Proof uses: Finset.image, Imo1989P1.row, Finset.range, OfNat.ofNat

   2 instances, coercions and auxiliary constants left out.

6. lemma Imo1989P1.row_quot line 46 source

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

   Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, Imo1989P1.n, Eq, HDiv.hDiv, HSub.hSub, Imo1989P1.row

   Proof uses: id, dite, ite, HMod.hMod, HAdd.hAdd, HMul.hMul, Eq.mpr, congrFun', congrArg, ite_eq_left, add_tsub_cancel_right, Not, ite_eq_right, Eq.mp, LE.le

   47 instances, coercions and auxiliary constants left out.

   Tactic trace: 5 steps

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

7. lemma Imo1989P1.row_inj line 49 source

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

   Statement uses: Nat, Fin, Imo1989P1.n, LT.lt, OfNat.ofNat, Iff, Eq, Imo1989P1.row, And

   Proof uses: Iff.intro, HDiv.hDiv, HSub.hSub, Imo1989P1.row_quot, Eq.trans, Eq.symm, Eq.mp, congrArg, And.intro, Fin.ext, dite, HMod.hMod, id, HAdd.hAdd, HMul.hMul, ite, congr, ite_eq_left, Not, ite_eq_right and 1 more

   26 instances, coercions and auxiliary constants left out.

   Tactic trace: 15 steps

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

8. lemma Imo1989P1.row_injOn line 57 source
9. lemma Imo1989P1.row_image_inj line 62 source
10. lemma Imo1989P1.A_card line 66 source

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

    Statement uses: Fin, Imo1989P1.n, Eq, Nat, Finset.card, Imo1989P1.A, OfNat.ofNat

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.image, Imo1989P1.row, Finset.range, Finset.card_image_of_injOn, Finset.card_range, eq_self

    4 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

11. lemma Imo1989P1.A_sum line 69 source

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

    Statement uses: Fin, Imo1989P1.n, Eq, Nat, Finset.sum, Imo1989P1.A, id, OfNat.ofNat

    Proof uses: Eq.mpr, Finset.image, Imo1989P1.row, Finset.range, congrArg, Finset.sum_image, Membership.mem, Set, Finset, HAdd.hAdd, ite, LT.lt, True, HMul.hMul, HSub.hSub, HMod.hMod, congrFun', Eq.trans, Finset.sum_range_succ, congr and 23 more

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

12. lemma Imo1989P1.A_injective line 77 source

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

    Statement uses: Function.Injective, Fin, Imo1989P1.n, Finset, Nat, Imo1989P1.A

    Proof uses: Eq, Membership.mem, Imo1989P1.row, OfNat.ofNat, Eq.rec, Iff.mpr, Finset.image, Finset.range, Exists, And, Finset.mem_image, Exists.intro, And.intro, of_eq_true, Eq.trans, LT.lt, True, rfl, Iff.mp, And.right and 3 more

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

13. lemma Imo1989P1.A_le_S line 83 source

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

    Statement uses: Fin, Imo1989P1.n, LE.le, Finset, Nat, Imo1989P1.A, Imo1989P1.S

    Proof uses: Membership.mem, And, Finset.range, OfNat.ofNat, Eq, Imo1989P1.row, Exists, Iff.mp, Finset.image, Finset.mem_image, id, Eq.mpr, ite, LT.lt, HMod.hMod, HAdd.hAdd, HMul.hMul, HSub.hSub, Finset.Icc, congrArg and 11 more

    67 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

14. lemma Imo1989P1.A_disjoint line 87 source

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

    Statement uses: Fin, Imo1989P1.n, Ne, Disjoint, Finset, Nat, Imo1989P1.A

    Proof uses: Eq.mpr, Membership.mem, Not, id, Eq, congrArg, propext, Finset.disjoint_left, And, Finset.range, OfNat.ofNat, Imo1989P1.row, Exists, False, Iff.mp, Finset.image, Finset.mem_image, And.right, Imo1989P1.row_inj, LT.lt and 2 more

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

15. def Imo1989P1.P line 94 source

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

    Statement uses: Finpartition, Finset, Nat, Imo1989P1.S

    Proof uses: Finpartition.mk, Finset.image, Fin, Imo1989P1.n, Imo1989P1.A, Finset.univ

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

16. problem Imo1989P1.imo1989_p1 line 114 source

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

    Statement uses: Exists, Finpartition, Finset, Nat, Imo1989P1.S, And, Eq, Finset.card, Finpartition.parts, OfNat.ofNat, Membership.mem, Finset.sum, id

    Proof uses: Exists.intro, Imo1989P1.P, And.intro, Eq.mpr, Finpartition.mk, Finset.image, Fin, Imo1989P1.n, Imo1989P1.A, Finset.univ, congrArg, Imo1989P1.P.eq_1, Finset.card_image_of_injective, Imo1989P1.A_injective, Imo1989P1.n.eq_1, of_eq_true, Eq.trans, True, congrFun', Fintype.card_fin and 7 more

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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