Compfiles/ZeroesOnesAndTwos.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

(From Mathematical Puzzles: A Connoisseur's Collection by Peter Winkler.)

Let n be a natural number. Prove that

(a) n has a (nonzero) multiple whose representation in base 10 contains only zeroes and ones; and (b) 2^n has a multiple whose representation contains only ones and twos.

Imports (3)
Imported by 1 file
  1. def ZerosOnesAndTwos.ones line 32 source

    standard axioms: propext what this means

    Statement uses: Nat

    Proof uses: Nat.ofDigits, List.replicate, OfNat.ofNat

    2 instances, coercions and auxiliary constants left out.

  2. lemma ZerosOnesAndTwos.ones_add line 35 source

    standard axioms: propext what this means

    Statement uses: Nat, Eq, ZerosOnesAndTwos.ones, HAdd.hAdd, Nat.ofDigits, HAppend.hAppend, List, List.replicate, OfNat.ofNat

    Proof uses: id, Eq.mpr, congrArg, List.replicate_add, HMul.hMul, HPow.hPow, List.length, Nat.ofDigits_append, List.length_replicate, Nat.ofDigits_replicate_zero, zero_add, Eq.refl

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  3. def ZerosOnesAndTwos.map_mod line 41 source

    no axioms what this means

    Statement uses: Nat, LT.lt, OfNat.ofNat, Fin

    Proof uses: Fin.mk, HMod.hMod

    7 instances, coercions and auxiliary constants left out.

  4. lemma ZerosOnesAndTwos.pigeonhole line 44 source

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

    Statement uses: Nat, Fin, Exists, And, LT.lt, Eq

    Proof uses: Ne, Finite.exists_ne_map_eq_of_infinite, Or.elim, Ne.lt_or_gt, Exists.intro, And.intro, Eq.symm

    10 instances, coercions and auxiliary constants left out.

  5. lemma ZerosOnesAndTwos.lemma_3 line 49 source

    standard axioms: propext what this means

    Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, HMod.hMod, Exists, PNat, HMul.hMul

    Proof uses: exists_eq_mul_right_of_dvd, Nat.dvd_of_mod_eq_zero, lt_of_mul_lt_mul_left', Eq.rec, Exists.intro, Subtype.mk

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  6. lemma ZerosOnesAndTwos.two_le_ten line 54 source

    standard axioms: propext what this means

    Statement uses: LE.le, Nat, OfNat.ofNat

    Proof uses: Iff.mp, Eq, HSub.hSub, tsub_eq_zero_iff_le, rfl

    16 instances, coercions and auxiliary constants left out.

  7. lemma ZerosOnesAndTwos.one_lt_ten line 55 source

    standard axioms: propext what this means

    Statement uses: LE.le, Nat, OfNat.ofNat

    Proof uses: Iff.mp, Eq, HSub.hSub, tsub_eq_zero_iff_le, rfl

    16 instances, coercions and auxiliary constants left out.

  8. lemma ZerosOnesAndTwos.one_le_ten line 56 source

    standard axioms: propext what this means

    Statement uses: LE.le, Nat, OfNat.ofNat

    Proof uses: Iff.mp, Eq, HSub.hSub, tsub_eq_zero_iff_le, rfl

    16 instances, coercions and auxiliary constants left out.

  9. problem ZerosOnesAndTwos.zeroes_and_ones line 60 source

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

    Statement uses: Nat, Exists, PNat, Membership.mem, List, Nat.digits, OfNat.ofNat, HMul.hMul, Or, Eq

    Proof uses: GT.gt, Nat.eq_zero_or_pos, Exists.intro, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, forall_congr, False, implies_congr, List.nil, congrFun', mul_one, Nat.digits_zero, Eq.refl, implies_true, And, LT.lt and 58 more

    68 instances, coercions and auxiliary constants left out.

    Tactic trace: 37 steps

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

  10. abbrev ZerosOnesAndTwos.all_one_or_two line 105 source

    no axioms what this means

    Statement uses: List, Nat

    Proof uses: Membership.mem, Or, Eq, OfNat.ofNat

    2 instances, coercions and auxiliary constants left out.

  11. def ZerosOnesAndTwos.prepend_one line 107 source

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

    Statement uses: Nat

    Proof uses: HAdd.hAdd, HPow.hPow, OfNat.ofNat, List.length, Nat.digits

    7 instances, coercions and auxiliary constants left out.

  12. lemma ZerosOnesAndTwos.prepend_one_pos line 109 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, ZerosOnesAndTwos.prepend_one

    Proof uses: Nat.casesAuxOn, Eq, of_eq_true, Eq.trans, True, congrArg, HAdd.hAdd, HPow.hPow, List.length, Nat.digits, congrFun', List, List.nil, Nat.digits_zero, pow_zero, add_zero, eq_self, Eq.symm, Eq.mpr, id and 21 more

    79 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  13. lemma ZerosOnesAndTwos.digits_len' line 114 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, List.length, Nat.digits, HAdd.hAdd, HDiv.hDiv

    Proof uses: Eq.mpr, List.cons, HMod.hMod, id, congrArg, List, Nat.digits_def', ZerosOnesAndTwos.two_le_ten, List.length.eq_2, add_comm

    16 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  14. lemma ZerosOnesAndTwos.prepend_one_div line 119 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, HDiv.hDiv, ZerosOnesAndTwos.prepend_one

    Proof uses: Eq.mpr, HAdd.hAdd, HPow.hPow, List.length, Nat.digits, id, congrArg, ZerosOnesAndTwos.prepend_one.eq_1, Nat.casesAuxOn, False.elim, Nat.lt_asymm, Eq.symm, Nat.succ, ZerosOnesAndTwos.digits_len', Nat.succ_pos, HMul.hMul, pow_add, pow_one, add_comm, Nat.add_mul_div_left and 1 more

    23 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  15. lemma ZerosOnesAndTwos.prepend_one_mod line 129 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, HMod.hMod, ZerosOnesAndTwos.prepend_one

    Proof uses: Eq.mpr, HAdd.hAdd, HPow.hPow, List.length, Nat.digits, id, congrArg, ZerosOnesAndTwos.prepend_one.eq_1, Nat.log, Nat.length_digits, ZerosOnesAndTwos.two_le_ten, ne_of_gt

    16 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  16. lemma ZerosOnesAndTwos.prepend_one_eq_append line 134 source

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

    Statement uses: Nat, Eq, List, Nat.digits, OfNat.ofNat, ZerosOnesAndTwos.prepend_one, HAppend.hAppend, List.cons, List.nil

    Proof uses: Nat.strong_induction_on, LT.lt, Nat.casesAuxOn, of_eq_true, Eq.trans, True, congr, congrArg, HMod.hMod, HDiv.hDiv, HAdd.hAdd, HPow.hPow, List.length, congrFun', Nat.digits_zero, pow_zero, add_zero, Nat.digits_of_two_le_of_pos, LE.le, eq_true_of_decide and 17 more

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  17. lemma ZerosOnesAndTwos.prepend_one_all_one_or_two line 147 source

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

    Statement uses: Nat, ZerosOnesAndTwos.all_one_or_two, Nat.digits, OfNat.ofNat, ZerosOnesAndTwos.prepend_one

    Proof uses: Eq.mpr, HAppend.hAppend, List, List.cons, List.nil, id, Eq, congrArg, ZerosOnesAndTwos.prepend_one_eq_append, Membership.mem, Or, ZerosOnesAndTwos.all_one_or_two.eq_1, Eq.mp, propext, List.mem_append, of_eq_true, Eq.trans, True, False, congr and 4 more

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  18. def ZerosOnesAndTwos.prepend_two line 158 source

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

    Statement uses: Nat

    Proof uses: HAdd.hAdd, HMul.hMul, OfNat.ofNat, HPow.hPow, List.length, Nat.digits

    9 instances, coercions and auxiliary constants left out.

  19. lemma ZerosOnesAndTwos.prepend_two_pos line 160 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, ZerosOnesAndTwos.prepend_two

    Proof uses: of_eq_true, HAdd.hAdd, HMul.hMul, HPow.hPow, List.length, Nat.digits, Eq.trans, Or, True, congrFun', congrArg, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.false, eq_true, True.intro and 1 more

    45 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  20. lemma ZerosOnesAndTwos.prepend_two_div line 162 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, HDiv.hDiv, ZerosOnesAndTwos.prepend_two

    Proof uses: Eq.mpr, HAdd.hAdd, HMul.hMul, HPow.hPow, List.length, Nat.digits, id, congrArg, ZerosOnesAndTwos.prepend_two.eq_1, Nat.casesAuxOn, False, Nat.lt_asymm, Eq.refl, Eq.symm, Nat.succ, ZerosOnesAndTwos.digits_len', Nat.succ_pos

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  21. lemma ZerosOnesAndTwos.prepend_two_mod line 170 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, HMod.hMod, ZerosOnesAndTwos.prepend_two

    Proof uses: Eq.mpr, HAdd.hAdd, HMul.hMul, HPow.hPow, List.length, Nat.digits, id, congrArg, ZerosOnesAndTwos.prepend_two.eq_1, Nat.log, Nat.length_digits, ZerosOnesAndTwos.two_le_ten, ne_of_gt

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  22. lemma ZerosOnesAndTwos.prepend_two_eq_append line 175 source

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

    Statement uses: Nat, Eq, List, Nat.digits, OfNat.ofNat, ZerosOnesAndTwos.prepend_two, HAppend.hAppend, List.cons, List.nil

    Proof uses: Nat.strong_induction_on, LT.lt, Nat.casesAuxOn, of_eq_true, Eq.trans, True, congr, congrArg, HMod.hMod, HDiv.hDiv, HAdd.hAdd, HMul.hMul, HPow.hPow, List.length, congrFun', Nat.digits_zero, pow_zero, mul_one, add_zero, Nat.digits_of_two_le_of_pos and 25 more

    33 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  23. lemma ZerosOnesAndTwos.prepend_two_all_one_or_two line 188 source

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

    Statement uses: Nat, ZerosOnesAndTwos.all_one_or_two, Nat.digits, OfNat.ofNat, ZerosOnesAndTwos.prepend_two

    Proof uses: Eq.mpr, HAppend.hAppend, List, List.cons, List.nil, id, Eq, congrArg, ZerosOnesAndTwos.prepend_two_eq_append, Membership.mem, Or, ZerosOnesAndTwos.all_one_or_two.eq_1, Eq.mp, propext, List.mem_append, Or.inr, List.mem_singleton

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  24. lemma ZerosOnesAndTwos.factor_ten_pow line 199 source

    standard axioms: propext what this means

    Statement uses: Nat, Eq, HPow.hPow, OfNat.ofNat, HMul.hMul

    Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, pow_zero, mul_one, eq_self, Eq.mpr, HAdd.hAdd, id, pow_succ, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 17 more

    35 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  25. lemma ZerosOnesAndTwos.even_5_pow_plus_one line 204 source

    standard axioms: propext what this means

    Statement uses: Nat, Dvd.dvd, OfNat.ofNat, HAdd.hAdd, HPow.hPow

    Proof uses: Nat.dvd_of_mod_eq_zero, Eq.mpr, Eq, HMod.hMod, id, congrArg, Nat.add_mod, Nat.pow_mod, of_eq_true, Eq.trans, True, congrFun', congr, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_natMod, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, one_pow, Nat.mod_succ, Nat.mod_self and 3 more

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  26. lemma ZerosOnesAndTwos.ones_and_twos_aux line 209 source

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

    Statement uses: Nat, Exists, PNat, And, Eq, List.length, Nat.digits, OfNat.ofNat, HMul.hMul, HPow.hPow, Nat.succ, ZerosOnesAndTwos.all_one_or_two

    Proof uses: Nat.recAux, Exists.intro, of_eq_true, Eq.trans, True, congr, congrArg, List.cons, List.nil, List, HMod.hMod, HDiv.hDiv, congrFun', Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_pow, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.isNat_natSucc, Mathlib.Meta.NormNum.natPow_one, mul_one and 92 more

    75 instances, coercions and auxiliary constants left out.

    Tactic trace: 62 steps

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

  27. problem ZerosOnesAndTwos.ones_and_twos line 276 source

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

    Statement uses: Nat, Exists, PNat, Membership.mem, List, Nat.digits, OfNat.ofNat, HMul.hMul, HPow.hPow, Or, Eq

    Proof uses: Nat.casesAuxOn, Exists.intro, of_eq_true, Eq.trans, True, forall_congr, implies_congr, List.nil, List.cons, congrFun', congrArg, HMod.hMod, HDiv.hDiv, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_pow, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.natPow_zero, mul_one, Nat.digits_of_two_le_of_pos and 24 more

    39 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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