Compfiles/Imo2022P5.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma Imo2022P5.mylemma_1 line 36 source

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

   Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, HAdd.hAdd, HMul.hMul, HPow.hPow

   Proof uses: Nat.le_induction, Eq.mpr, id, Eq, congr, congrArg, Eq.trans, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add, Mathlib.Tactic.Ring.Common.mul_pf_left, Mathlib.Meta.NormNum.IsNat.to_raw_eq and 37 more

   53 instances, coercions and auxiliary constants left out.

   Tactic trace: 10 steps

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

2. lemma Imo2022P5.mylemma_3 line 51 source

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

   Statement uses: Nat, Nat.Prime, Eq, HPow.hPow, HAdd.hAdd, Nat.factorial, LE.le, Dvd.dvd

   Proof uses: Nat.dvd_factorial, Nat.Prime.pos, Iff.mpr, Nat.dvd_add_self_right, Eq.mpr, id, congrArg, Nat.Prime.dvd_of_dvd_pow

   16 instances, coercions and auxiliary constants left out.

   Tactic trace: 6 steps

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

3. lemma Imo2022P5.mylemma_42 line 65 source

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

   Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HAdd.hAdd, HMul.hMul

   Proof uses: add_lt_add_left, Eq.mpr, id, Eq, congrArg, Eq.symm, two_mul, mul_le_mul_left, lt_of_le_of_lt'

   50 instances, coercions and auxiliary constants left out.

   Tactic trace: 5 steps

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

4. lemma Imo2022P5.mylemma_43 line 76 source

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

   Statement uses: Nat, Eq, Finset.prod, Finset.Ico, HSub.hSub, HMul.hMul, OfNat.ofNat, HAdd.hAdd, Finset.range

   Proof uses: Eq.mpr, id, congrArg, Finset.prod_Ico_eq_prod_range, rfl

   21 instances, coercions and auxiliary constants left out.

   Tactic trace: 5 steps

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

5. lemma Imo2022P5.mylemma_44 line 84 source

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

   Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Finset.prod, Finset.range, HSub.hSub, HAdd.hAdd

   Proof uses: Nat.le_induction, Mathlib.Meta.NormNum.isNat_eq_true, Eq.rec, Finset.cons, Finset.notMem_range_self, Mathlib.Meta.NormNum.IsNat, HMul.hMul, Mathlib.Meta.NormNum.isNat_mul, Eq.refl, Mathlib.Meta.NormNum.isNat_add, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.isNat_ofNat, Finset.empty, Mathlib.Meta.NormNum.Finset.prod_empty, Eq.symm, congr_fun, EmptyCollection.emptyCollection, Finset, congr_arg, Mathlib.Meta.Finset.range_zero' and 46 more

   73 instances, coercions and auxiliary constants left out.

   Tactic trace: 16 steps

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

6. lemma Imo2022P5.mylemma_41 line 104 source

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

   Statement uses: Nat, Nat.Prime, LT.lt, HMul.hMul, OfNat.ofNat, HAdd.hAdd, Nat.factorial, HPow.hPow

   Proof uses: LE.le, HSub.hSub, Nat.factorial_le, Nat.le_pred_of_lt, Nat.sub, Nat.Prime.two_le, Eq, Nat.sub_add_cancel, Nat.one_le_of_lt, Finset.prod, Finset.range, Finset.Ico, Eq.symm, Finset.prod_range_mul_prod_Ico, Finset.prod_range_succ, Eq.mpr, id, congrArg, Imo2022P5.mylemma_43, Imo2022P5.mylemma_44 and 38 more

   64 instances, coercions and auxiliary constants left out.

   Tactic trace: 60 steps

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

7. lemma Imo2022P5.mylemma_4 line 178 source

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

   Statement uses: Nat, And, LT.lt, OfNat.ofNat, Nat.Prime, Eq, HPow.hPow, HAdd.hAdd, Nat.factorial, LE.le, Dvd.dvd, HMul.hMul

   Proof uses: Nat.le_of_dvd, And.left, Or, lt_or_eq_of_le, False.elim, False, Nat.pos_of_mul_pos_left, Nat.lt_of_lt_of_eq, Nat.zero_lt_of_lt, dite, dvd_pow_self, Eq.mpr, id, congrArg, mul_pow, dvd_mul_of_dvd_right, Nat.dvd_factorial, HSub.hSub, Nat.dvd_sub, Iff.mp and 10 more

   56 instances, coercions and auxiliary constants left out.

   Tactic trace: 39 steps

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

8. lemma Imo2022P5.mylemma_53 line 220 source

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

   Statement uses: Nat, LE.le, OfNat.ofNat, Int.ModEq, HPow.hPow, Int, HAdd.hAdd, HMul.hMul, Neg.neg, HSub.hSub

   Proof uses: Eq, of_eq_true, Eq.trans, True, congrArg, add_sub_cancel_right, eq_self, Eq.mpr, id, Eq.symm, Int.ModEq.refl, Finset.sum, Finset.Ico, Nat.choose, sub_eq_add_neg, Finset.range, add_pow, one_le_two, Finset.sum_range_add_sum_Ico, congrFun' and 69 more

   102 instances, coercions and auxiliary constants left out.

   Tactic trace: 26 steps

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

9. lemma Imo2022P5.mylemma_52 line 259 source

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

   Statement uses: Nat, Nat.Prime, LE.le, OfNat.ofNat, Dvd.dvd, HPow.hPow, HAdd.hAdd, HSub.hSub, False

   Proof uses: Int.ModEq, Int, HMul.hMul, Nat.choose, Neg.neg, Int.ModEq.sub_right, Eq.mpr, id, Eq, congr, congrFun', congrArg, Eq.trans, Nat.cast_add, Nat.cast_one, Nat.choose_one_right, Imo2022P5.mylemma_53, Odd, Nat.Prime.odd_of_ne_two, Not.intro and 90 more

   140 instances, coercions and auxiliary constants left out.

   Tactic trace: 65 steps

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

10. lemma Imo2022P5.mylemma_51 line 328 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HAdd.hAdd, Nat.factorial, HPow.hPow

    Proof uses: Nat.le_induction, Nat.lt_of_sub_eq_succ, rfl, HSub.hSub, Eq, HMul.hMul, Eq.mpr, id, congrArg, add_mul, one_mul, Nat.factorial_succ, add_comm, mul_comm, Eq.refl, pow_add, pow_one, Nat.mul_lt_mul_of_pos_right, Nat.pow_lt_pow_left, lt_add_one

    57 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

11. lemma Imo2022P5.mylemma_5 line 346 source

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

    Statement uses: Nat, Nat.Prime, LE.le, Eq, HPow.hPow, HAdd.hAdd, Nat.factorial, OfNat.ofNat, False

    Proof uses: dite, LT.lt, Imo2022P5.mylemma_51, False.elim, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HMul.hMul, Nat.rawCast, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.cast_pos and 112 more

    124 instances, coercions and auxiliary constants left out.

    Tactic trace: 51 steps

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

12. lemma Imo2022P5.mylemma_6 line 401 source

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

    Statement uses: Nat, Nat.Prime, Dvd.dvd, LE.le, HMul.hMul, OfNat.ofNat, HPow.hPow, HSub.hSub, Nat.factorial

    Proof uses: pow_dvd_pow_of_dvd, Nat.Prime.two_le, Nat.pow_dvd_of_le_of_pow_dvd, Nat.factorial_dvd_factorial, HAdd.hAdd, Nat.factorial_mul_factorial_dvd_factorial_add, Nat.dvd_factorial, dvd_trans, Eq.mp, congrArg, Eq.symm, two_mul, pow_two, Nat.dvd_sub

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

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

13. determine Imo2022P5.solution_set line 422 source

    no axioms what this means

    Statement uses: Set, Prod, Nat

    Proof uses: Insert.insert, Prod.mk, OfNat.ofNat, Singleton.singleton

    3 instances, coercions and auxiliary constants left out.

14. problem Imo2022P5.imo2022_p5 line 424 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Nat.Prime, Iff, Membership.mem, Prod, Set, Imo2022P5.solution_set, Prod.mk, Eq, HPow.hPow, HAdd.hAdd, Nat.factorial

    Proof uses: Iff.intro, And, Or, Eq.mp, congr, congrArg, Eq.trans, Prod.mk.injEq, Insert.insert, Singleton.singleton, of_eq_true, True, eq_self, Eq.mpr, id, HSub.hSub, Nat.Simproc.eq_add_le, of_decide_eq_true, LE.le, Eq.refl and 120 more

    116 instances, coercions and auxiliary constants left out.

    Tactic trace: 100 steps

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