Compfiles/Imo2000P5.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma Imo2000P5.extend_divisibility line 31 source

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

   Statement uses: Nat, Dvd.dvd, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Nat.Prime, Ne, HMul.hMul

   Proof uses: Odd, Nat.Prime.odd_of_ne_two, Eq, Int, Finset.sum, Finset.range, Neg.neg, HSub.hSub, geom_sum_mul, Finset.sum_congr, rfl, Finset, Membership.mem, Mathlib.Tactic.Ring.of_eq, Int.rawCast, inferInstance, Ring, Int.negOfNat, Nat.rawCast, Mathlib.Tactic.Ring.Common.pow_congr and 98 more

   127 instances, coercions and auxiliary constants left out.

   Tactic trace: 21 steps

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

2. lemma Imo2000P5.quotient_not_dvd_of_ne line 62 source

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

   Statement uses: Nat, Nat.Prime, Ne, OfNat.ofNat, Dvd.dvd, HAdd.hAdd, HPow.hPow, Not, HDiv.hDiv, HMul.hMul

   Proof uses: Int, Finset.sum, Finset.range, Neg.neg, Eq, rfl, Odd, Nat.Prime.odd_of_ne_two, HSub.hSub, geom_sum_mul, Finset.sum_congr, Finset, Membership.mem, Mathlib.Tactic.Ring.of_eq, Int.rawCast, inferInstance, Ring, Int.negOfNat, Nat.rawCast, Mathlib.Tactic.Ring.Common.pow_congr and 108 more

   136 instances, coercions and auxiliary constants left out.

   Tactic trace: 37 steps

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

3. lemma Imo2000P5.quotient_val_q line 104 source

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

   Statement uses: Nat, Nat.Prime, Ne, OfNat.ofNat, Dvd.dvd, HAdd.hAdd, HPow.hPow, HMul.hMul, Eq, ENat, emultiplicity, HDiv.hDiv

   Proof uses: LT.lt, add_pos', pow_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble, Odd, Nat.Prime.odd_of_ne_two, Not, mt, Iff.mp, Nat.prime_dvd_prime_iff_eq, Nat.prime_two, Nat.Prime.dvd_of_dvd_pow, Top.top, FiniteMultiplicity, finiteMultiplicity_iff_emultiplicity_ne_top, Iff.mpr and 20 more

   72 instances, coercions and auxiliary constants left out.

   Tactic trace: 11 steps

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

4. lemma Imo2000P5.exists_new_prime_factor line 126 source

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

   Statement uses: Nat, LE.le, OfNat.ofNat, Nat.Prime, Ne, Dvd.dvd, HAdd.hAdd, HPow.hPow, Exists, And, HMul.hMul, Not

   Proof uses: HDiv.hDiv, Eq, rfl, Nat.Prime.two_le, Eq.mpr, id, congrArg, congrFun', pow_mul, Eq.mp, one_pow, Odd.nat_add_dvd_pow_add_pow, Nat.Prime.odd_of_ne_two, LT.lt, Nat.div_pos, Nat.le_of_dvd, add_pos', pow_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat and 119 more

   159 instances, coercions and auxiliary constants left out.

   Tactic trace: 54 steps

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

5. lemma Imo2000P5.increase_prime_factors line 173 source

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

   Statement uses: Nat, LT.lt, OfNat.ofNat, Dvd.dvd, HAdd.hAdd, HPow.hPow, Exists, And, Eq, Finset.card, Nat.primeFactors

   Proof uses: dite, LE.le, Nat.one_le_two_pow, Nat.Prime, Ne, Exists.intro, Nat.minFac, And.intro, Nat.minFac_prime, LT.lt.ne', Nat.minFac_dvd, Eq.mp, congrArg, dvd_pow_self, HMul.hMul, Not, Imo2000P5.exists_new_prime_factor, Nat.mul_pos, Nat.Prime.pos, False and 52 more

   64 instances, coercions and auxiliary constants left out.

   Tactic trace: 48 steps

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

6. theorem Imo2000P5.exists_dvd_two_pow_add_one line 220 source

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

   Statement uses: Nat, Exists, And, LT.lt, OfNat.ofNat, Eq, Finset.card, Nat.primeFactors, Dvd.dvd, HAdd.hAdd, HPow.hPow

   Proof uses: Nat.recAux, Exists.intro, And.intro, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, of_eq_true, Eq.trans, True, congrFun', congrArg, Finset, EmptyCollection.emptyCollection, Nat.primeFactors_one, eq_self, eq_true, True.intro, Mathlib.Meta.NormNum.isNat_dvd_true and 4 more

   33 instances, coercions and auxiliary constants left out.

   Tactic trace: 9 steps

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

7. determine Imo2000P5.solution line 231 source

   no axioms what this means

   Statement uses: Bool

   Proof uses: Bool.true

8. problem Imo2000P5.imo2000_p5 line 233 source

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

   Statement uses: Exists, Nat, Iff, And, LT.lt, OfNat.ofNat, Eq, Finset.card, Nat.primeFactors, Dvd.dvd, HAdd.hAdd, HPow.hPow, Bool, Imo2000P5.solution, Bool.true

   Proof uses: Imo2000P5.exists_dvd_two_pow_add_one, Exists.intro, Eq.mpr, id, Eq.trans, True, congrArg, eq_self, iff_true, And.intro

   20 instances, coercions and auxiliary constants left out.

   Tactic trace: 4 steps

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