Compfiles/Imo1976P4.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def Imo1976P4.IsMaxProd line 28 source

   standard axioms: propext what this means

   Statement uses: Nat

   Proof uses: IsGreatest, Set.ofPred, Exists, Multiset, And, Eq, Multiset.sum, Multiset.prod

   3 instances, coercions and auxiliary constants left out.

2. def Imo1976P4.IsMaxProdSet line 33 source

   standard axioms: propext what this means

   Statement uses: Multiset, Nat

   Proof uses: Imo1976P4.IsMaxProd, Multiset.sum, Multiset.prod

   2 instances, coercions and auxiliary constants left out.

3. def Imo1976P4.result line 36 source

   no axioms what this means

   Statement uses: Nat

   2 instances, coercions and auxiliary constants left out.

4. lemma Imo1976P4.prod_le_sum_pow_sum line 44 source

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

   Statement uses: Multiset, Nat, LE.le, Multiset.prod, HPow.hPow, Multiset.sum

   Proof uses: Multiset.induction, of_eq_true, OfNat.ofNat, Eq.trans, True, congrArg, pow_zero, Eq.mpr, Multiset.cons, HAdd.hAdd, id, Eq, Multiset.sum_cons, HMul.hMul, Multiset.prod_cons, dite, MulZeroClass.zero_mul, Nat.zero_le, Not, Trans.trans and 15 more

   51 instances, coercions and auxiliary constants left out.

   Tactic trace: 19 steps

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

5. lemma Imo1976P4.exists_mem_of_sum_lt_zero line 65 source

   standard axioms: propext what this means

   Statement uses: Multiset, Nat, LT.lt, OfNat.ofNat, Multiset.sum, Exists, Membership.mem

   Proof uses: Ne, Mathlib.Tactic.Contrapose.contrapose₃, Eq, Eq.mpr, Not, LE.le, id, implies_congr, Eq.refl, congrArg, Multiset.sum_zero, le_refl, Multiset.exists_mem_of_ne_zero

   20 instances, coercions and auxiliary constants left out.

   Tactic trace: 4 steps

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

6. lemma Imo1976P4.prod_with_given_sum_bddAbove line 72 source

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

   Statement uses: Nat, BddAbove, Set.ofPred, Exists, Multiset, And, Eq, Multiset.sum, Multiset.prod

   Proof uses: Exists.intro, Membership.mem, Set, upperBounds, HPow.hPow, LE.le, Eq.mpr, id, congrArg, Eq.symm, Imo1976P4.prod_le_sum_pow_sum

   13 instances, coercions and auxiliary constants left out.

   Tactic trace: 5 steps

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

7. lemma Imo1976P4.exists_max_prod line 80 source

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

   Statement uses: Nat, Exists, Imo1976P4.IsMaxProd

   Proof uses: BddAbove.exists_isGreatest_of_nonempty, Set.ofPred, Multiset, And, Eq, Multiset.sum, Multiset.prod, Imo1976P4.prod_with_given_sum_bddAbove, Exists.intro, Membership.mem, Set, Singleton.singleton, And.intro, Eq.mpr, id, congrArg, Multiset.sum_singleton, Eq.refl, Multiset.prod_singleton

   7 instances, coercions and auxiliary constants left out.

   Tactic trace: 11 steps

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

8. lemma Imo1976P4.exists_max_prod_set line 90 source

   standard axioms: propext what this means

   Statement uses: Nat, Imo1976P4.IsMaxProd, Exists, Multiset, And, Eq, Multiset.sum, Imo1976P4.IsMaxProdSet

   Proof uses: Multiset.prod, Membership.mem, Set, Set.ofPred, And.left, upperBounds, Exists.intro, And.intro, Eq.mpr, id, congrArg, Imo1976P4.IsMaxProdSet.eq_1

   7 instances, coercions and auxiliary constants left out.

   Tactic trace: 8 steps

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

9. lemma Imo1976P4.prod_le_max_prod line 99 source

   standard axioms: Quot.sound, propext what this means

   Statement uses: Nat, Imo1976P4.IsMaxProd, Multiset, Eq, Multiset.sum, LE.le, Multiset.prod

   Proof uses: Membership.mem, Set, upperBounds, Set.ofPred, Exists, And, And.right, Eq.mp, congrFun', congrArg, funext, Eq.trans, forall_congr

   10 instances, coercions and auxiliary constants left out.

   Tactic trace: 3 steps

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

10. lemma Imo1976P4.not_max_prod_set_of_prod_lt_prod line 105 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Multiset, Nat, Eq, Multiset.sum, LT.lt, Multiset.prod, Not, Imo1976P4.IsMaxProdSet

    Proof uses: Mathlib.Tactic.Contrapose.contrapose₃, Eq.mpr, LE.le, id, implies_congr, Eq.refl, Membership.mem, Set, upperBounds, Set.ofPred, Exists, And, And.right, Eq.mp, congrFun', congrArg, funext, Eq.trans, forall_congr, Eq.symm

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

11. lemma Imo1976P4.exists_cons_le_of_le_of_sum_lt_sum line 112 source

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

    Statement uses: Multiset, Nat, LE.le, LT.lt, Multiset.sum, Exists, Multiset.cons

    Proof uses: Ne, HSub.hSub, OfNat.ofNat, Mathlib.Tactic.Contrapose.contrapose₃, Eq, Eq.mpr, Not, id, implies_congr, Eq.refl, le_of_eq, Trans.trans, HAdd.hAdd, congrArg, Multiset.sub_add_cancel, Multiset.sum_add, Multiset.sum_zero, zero_add, Membership.mem, Multiset.exists_mem_of_ne_zero and 7 more

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

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

12. lemma Imo1976P4.exists_le_of_mem_of_lt_sum line 128 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Nat, Multiset, Membership.mem, LT.lt, Multiset.sum, Exists, LE.le, Insert.insert, Singleton.singleton

    Proof uses: Eq, Multiset.cons, Multiset.exists_cons_of_mem, Ne, OfNat.ofNat, Mathlib.Tactic.Contrapose.contrapose₃, Eq.mpr, Not, id, implies_congr, Eq.refl, congrArg, HAdd.hAdd, Multiset.sum_cons, Multiset.sum_zero, add_zero, le_refl, Multiset.exists_mem_of_ne_zero, Exists.intro, Multiset.insert_eq_cons and 3 more

    31 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

13. lemma Imo1976P4.zero_not_in_max_prod_set line 139 source

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

    Statement uses: Multiset, Nat, Imo1976P4.IsMaxProdSet, Not, Membership.mem, OfNat.ofNat

    Proof uses: Mathlib.Tactic.Contrapose.contrapose₃, Eq, Multiset.sum, Multiset.replicate, Eq.mpr, HSMul.hSMul, id, congrArg, Multiset.sum_replicate, HMul.hMul, Nat.nsmul_eq_mul, mul_one, Eq.refl, Imo1976P4.not_max_prod_set_of_prod_lt_prod, LT.lt, Multiset.prod, HPow.hPow, Multiset.prod_replicate, one_pow, Multiset.prod_eq_zero and 4 more

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

14. lemma Imo1976P4.max_prod_set_of_subset_of_max_prod_set line 148 source

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

    Statement uses: Multiset, Nat, LE.le, Imo1976P4.IsMaxProdSet

    Proof uses: And.intro, Membership.mem, Set, Set.ofPred, Exists, And, Eq, Multiset.sum, Multiset.prod, upperBounds, Exists.intro, Eq.refl, GT.gt, HSub.hSub, OfNat.ofNat, Nat.zero_lt_of_ne_zero, Multiset.prod_ne_zero, Imo1976P4.zero_not_in_max_prod_set, Eq.mpr, LT.lt and 21 more

    51 instances, coercions and auxiliary constants left out.

    Tactic trace: 25 steps

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

15. lemma Imo1976P4.one_not_in_max_prod_set_of_one_lt_sum line 174 source

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

    Statement uses: Multiset, Nat, LT.lt, OfNat.ofNat, Multiset.sum, Imo1976P4.IsMaxProdSet, Not, Membership.mem

    Proof uses: LE.le, Insert.insert, Singleton.singleton, Exists, False, Imo1976P4.exists_le_of_mem_of_lt_sum, Imo1976P4.max_prod_set_of_subset_of_max_prod_set, Mathlib.Tactic.Contrapose.contrapose₁, Eq.mpr, True, id, Eq, implies_congr, not_false_eq_true, Eq.refl, HAdd.hAdd, congrArg, Multiset.sum_singleton, Multiset.cons, Multiset.insert_eq_cons and 6 more

    27 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

16. lemma Imo1976P4.not_in_max_prod_set_of_five_le line 186 source

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

    Statement uses: Multiset, Nat, LT.lt, OfNat.ofNat, Imo1976P4.IsMaxProdSet, Not, Membership.mem

    Proof uses: Singleton.singleton, Imo1976P4.max_prod_set_of_subset_of_max_prod_set, Iff.mpr, LE.le, Multiset.singleton_le, Mathlib.Tactic.Contrapose.contrapose₁, False, Eq.mpr, True, id, Eq, implies_congr, not_false_eq_true, Eq.refl, Multiset.sum, Insert.insert, HSub.hSub, congrArg, Multiset.sum_singleton, Multiset.cons and 10 more

    27 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

17. lemma Imo1976P4.lt_and_gt_of_in_max_prod_set_of_four_lt_sum line 200 source

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

    Statement uses: Multiset, Nat, Membership.mem, LT.lt, OfNat.ofNat, Multiset.sum, Imo1976P4.IsMaxProdSet, And

    Proof uses: Ne, Mathlib.Tactic.Contrapose.contrapose₃, Eq, Eq.mpr, Not, id, congrArg, Imo1976P4.zero_not_in_max_prod_set, Imo1976P4.one_not_in_max_prod_set_of_one_lt_sum, LE.le, Mathlib.Tactic.Contrapose.contrapose₁, implies_congr, Eq.refl, Imo1976P4.not_in_max_prod_set_of_five_le

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

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

18. lemma Imo1976P4.three_in_max_prod_set_of_four_lt_sum line 216 source

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

    Statement uses: Multiset, Nat, LT.lt, OfNat.ofNat, Multiset.sum, Imo1976P4.IsMaxProdSet, Membership.mem

    Proof uses: Eq.mpr, Ne, Multiset.count, id, Eq, congrArg, Eq.symm, propext, Multiset.count_ne_zero, Nat.ne_zero_iff_zero_lt, LE.le, Finset, Multiset.toFinset, Insert.insert, Singleton.singleton, And, Imo1976P4.lt_and_gt_of_in_max_prod_set_of_four_lt_sum, Eq.mp, Multiset.mem_toFinset, And.left and 60 more

    57 instances, coercions and auxiliary constants left out.

    Tactic trace: 79 steps

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

19. lemma Imo1976P4.max_prod_zero line 289 source

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

    Statement uses: Imo1976P4.IsMaxProd, OfNat.ofNat, Nat

    Proof uses: And.intro, Membership.mem, Set, Set.ofPred, Exists, Multiset, And, Eq, Multiset.sum, Multiset.prod, upperBounds, Exists.intro, Eq.refl, LE.le, dite, Eq.mpr, id, congrArg, Eq.symm, Multiset.prod_zero and 7 more

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

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

20. lemma Imo1976P4.max_prod_one line 304 source

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

    Statement uses: Imo1976P4.IsMaxProd, OfNat.ofNat, Nat

    Proof uses: And.intro, Membership.mem, Set, Set.ofPred, Exists, Multiset, And, Eq, Multiset.sum, Multiset.prod, upperBounds, Exists.intro, Singleton.singleton, Eq.refl, LE.le, Imo1976P4.exists_mem_of_sum_lt_zero, Eq.mpr, id, congrArg, Eq.symm and 25 more

    41 instances, coercions and auxiliary constants left out.

    Tactic trace: 24 steps

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

21. lemma Imo1976P4.max_prod_two line 324 source

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

    Statement uses: Imo1976P4.IsMaxProd, OfNat.ofNat, Nat

    Proof uses: And.intro, Membership.mem, Set, Set.ofPred, Exists, Multiset, And, Eq, Multiset.sum, Multiset.prod, upperBounds, Exists.intro, Singleton.singleton, Eq.refl, LE.le, Imo1976P4.exists_mem_of_sum_lt_zero, Eq.mpr, id, congrArg, Eq.symm and 26 more

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 27 steps

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

22. lemma Imo1976P4.max_prod_three line 346 source

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

    Statement uses: Imo1976P4.IsMaxProd, OfNat.ofNat, Nat

    Proof uses: And.intro, Membership.mem, Set, Set.ofPred, Exists, Multiset, And, Eq, Multiset.sum, Multiset.prod, upperBounds, Exists.intro, Singleton.singleton, Eq.refl, LE.le, Imo1976P4.exists_mem_of_sum_lt_zero, Eq.mpr, id, congrArg, Eq.symm and 27 more

    43 instances, coercions and auxiliary constants left out.

    Tactic trace: 30 steps

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

23. lemma Imo1976P4.max_prod_four line 370 source

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

    Statement uses: Imo1976P4.IsMaxProd, OfNat.ofNat, Nat

    Proof uses: And.intro, Membership.mem, Set, Set.ofPred, Exists, Multiset, And, Eq, Multiset.sum, Multiset.prod, upperBounds, Exists.intro, Singleton.singleton, Eq.refl, LE.le, Imo1976P4.exists_mem_of_sum_lt_zero, Eq.mpr, id, congrArg, Eq.symm and 28 more

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 33 steps

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

24. theorem Imo1976P4.generalized line 396 source

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

    Statement uses: Nat, Imo1976P4.IsMaxProd, Imo1976P4.result

    Proof uses: Imo1976P4.result.induct_unfolding, Imo1976P4.max_prod_zero, Imo1976P4.max_prod_one, Imo1976P4.max_prod_two, Imo1976P4.max_prod_three, Imo1976P4.max_prod_four, Eq, OfNat.ofNat, False, HAdd.hAdd, Exists, Nat.succ, HMul.hMul, Imo1976P4.exists_max_prod, Multiset, And, Multiset.sum, Imo1976P4.IsMaxProdSet, Imo1976P4.exists_max_prod_set, LT.lt and 31 more

    35 instances, coercions and auxiliary constants left out.

    Tactic trace: 33 steps

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

25. determine Imo1976P4.solution line 435 source

    no axioms what this means

    Statement uses: Nat

    Proof uses: Imo1976P4.result, OfNat.ofNat

    1 instances, coercions and auxiliary constants left out.

26. problem Imo1976P4.imo1976_p4 line 437 source

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

    Statement uses: IsGreatest, Nat, Set.ofPred, Exists, Multiset, And, Eq, Multiset.sum, OfNat.ofNat, Multiset.prod, Imo1976P4.solution

    Proof uses: Imo1976P4.generalized

    5 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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