Compfiles/Imo2015P2.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. determine Imo2015P2.SolutionSet line 26 source

   no axioms what this means

   Statement uses: Set, Prod, Int

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

   3 instances, coercions and auxiliary constants left out.

2. def Imo2015P2.is_power_of_two line 35 source

   standard axioms: propext what this means

   Statement uses: Int

   Proof uses: Exists, Nat, Eq, HPow.hPow, OfNat.ofNat

   5 instances, coercions and auxiliary constants left out.

3. lemma Imo2015P2.pow_of_two_coprime_odd line 39 source

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

   Statement uses: Nat, Int, Not, Dvd.dvd, OfNat.ofNat, IsCoprime, HPow.hPow

   Proof uses: Eq.mpr, Nat.Coprime, Int.natAbs, id, Eq, congrArg, propext, Int.isCoprime_iff_nat_coprime, Int.natAbs_pow, Eq.symm, Int.ofNat_two, Int.natAbs_natCast, Nat.coprime_comm, Nat.Prime.coprime_pow_of_not_dvd, Nat.prime_two, Int.ofNat_dvd, Int.dvd_natAbs

   21 instances, coercions and auxiliary constants left out.

   Tactic trace: 5 steps

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

4. lemma Imo2015P2.pow_of_two_dvd_odd_mul_self_sub_1 line 47 source

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

   Statement uses: Nat, Int, Not, Dvd.dvd, OfNat.ofNat, LT.lt, HPow.hPow, HSub.hSub, LE.le, HAdd.hAdd, HMul.hMul

   Proof uses: Eq, Exists, Eq.mp, Odd, congrArg, propext, odd_iff_exists_bit1, HMod.hMod, Eq.symm, Int.odd_iff, Int.two_dvd_ne_zero, Eq.mpr, id, dite, IsCoprime.dvd_of_dvd_mul_right, Imo2015P2.pow_of_two_coprime_odd, Even, even_iff_two_dvd, Int.not_even_iff_odd, Even.add_one and 54 more

   75 instances, coercions and auxiliary constants left out.

   Tactic trace: 25 steps

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

5. lemma Imo2015P2.dvd_pow_of_two line 72 source

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

   Statement uses: Nat, Int, LE.le, OfNat.ofNat, Dvd.dvd, HPow.hPow, Exists, Eq

   Proof uses: CanLift.prf, And, Iff.mp, Nat.dvd_prime_pow, Nat.prime_two, Eq.mp, Eq.trans, congrArg, Exists.intro, cast, Eq.symm

   36 instances, coercions and auxiliary constants left out.

   Tactic trace: 5 steps

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

6. lemma Imo2015P2.odd_dvd_pow_of_two line 79 source

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

   Statement uses: Nat, Int, Not, Dvd.dvd, OfNat.ofNat, LE.le, HPow.hPow, Eq

   Proof uses: Exists, Imo2015P2.dvd_pow_of_two, Eq.mpr, id, congrArg, Mathlib.Tactic.Contrapose.contrapose₂, Ne, dvd_pow_self, Mathlib.Tactic.Contrapose.contrapose₄, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_pow, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.natPow_zero, Eq.mp

   21 instances, coercions and auxiliary constants left out.

   Tactic trace: 7 steps

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

7. lemma Imo2015P2.sq_pow_of_two_sub_two line 89 source

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

   Statement uses: Nat, Int, LE.le, OfNat.ofNat, Dvd.dvd, HPow.hPow, HSub.hSub, Eq

   Proof uses: Eq.mpr, id, congrArg, propext, sub_nonneg, Trans.trans, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.bit0, Bool, Bool.true, Iff.mpr, pow_le_pow_iff_left₀, Mathlib.Meta.NormNum.isNat_eq_false, Bool.false, Exists, Imo2015P2.dvd_pow_of_two and 86 more

   143 instances, coercions and auxiliary constants left out.

   Tactic trace: 46 steps

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

8. lemma Imo2015P2.swap_ab_solution line 134 source

   standard axioms: propext what this means

   Statement uses: Int, Iff, Membership.mem, Prod, Set, Imo2015P2.SolutionSet, Prod.mk

   Proof uses: Eq.mpr, Or, And, Eq, OfNat.ofNat, id, congr, congrArg, Eq.trans, Insert.insert, Singleton.singleton, Prod.mk.injEq, Iff.intro, of_eq_true, True, False, eq_true, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 12 more

   13 instances, coercions and auxiliary constants left out.

   Tactic trace: 7 steps

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

9. lemma Imo2015P2.swap_bc_solution line 139 source

   standard axioms: propext what this means

   Statement uses: Int, Iff, Membership.mem, Prod, Set, Imo2015P2.SolutionSet, Prod.mk

   Proof uses: Eq.mpr, Or, And, Eq, OfNat.ofNat, id, congr, congrArg, Eq.trans, Insert.insert, Singleton.singleton, Prod.mk.injEq, Iff.intro, of_eq_true, True, False, eq_true, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 12 more

   13 instances, coercions and auxiliary constants left out.

   Tactic trace: 7 steps

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

10. problem Imo2015P2.imo2015_p2 line 146 source

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

    Statement uses: Int, Iff, Membership.mem, Prod, Set, Imo2015P2.SolutionSet, Prod.mk, And, LT.lt, OfNat.ofNat, Imo2015P2.is_power_of_two, HSub.hSub, HMul.hMul

    Proof uses: LE.le, Not, Or, Classical.em, Iff.intro, Eq.mpr, Eq, Exists, Nat, HPow.hPow, id, implies_congr, Insert.insert, Singleton.singleton, Eq.trans, congr, congrArg, Prod.mk.injEq, Eq.refl, Exists.intro and 186 more

    217 instances, coercions and auxiliary constants left out.

    Tactic trace: 309 steps (first 200 of 309)

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