Compfiles/Poland1998P4.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Polish Mathematical Olympiad 1998, Problem 4

Prove that the sequence {a_n} defined by a_1 = 1 and

a_n = a_{n - 1} + a_{⌊n/2⌋} n = 2,3,4,...

contains infinitely many integers divisible by 7.

Imports (4)
Imported by 1 file
  1. def Poland1998P4.a line 32 source

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

    Statement uses: Nat

    Proof uses: WellFounded.Nat.fix, InvImage, LT.lt, Poland1998P4.a.match_1, Unit, OfNat.ofNat, Nat.succ, HDiv.hDiv, HAdd.hAdd

    9 instances, coercions and auxiliary constants left out.

  2. lemma Poland1998P4.a_recurrence line 41 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Poland1998P4.a, HAdd.hAdd, HSub.hSub, HDiv.hDiv

    Proof uses: Exists, Exists.intro, Eq.mpr, Nat.succ, id, congrFun', congrArg, Poland1998P4.a.eq_3, False.elim, False, noConfusion_of_Nat, Nat.ctorIdx, Nat.add, Eq.refl, Eq.symm

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  3. def Poland1998P4.a' line 46 source

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

    Statement uses: Nat, ZMod, OfNat.ofNat

    Proof uses: Poland1998P4.a

    8 instances, coercions and auxiliary constants left out.

  4. lemma Poland1998P4.a'_recurrence line 48 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Eq, ZMod, Poland1998P4.a', HAdd.hAdd, HSub.hSub, HDiv.hDiv

    Proof uses: of_eq_true, Poland1998P4.a, Eq.trans, True, congrFun', congrArg, Poland1998P4.a_recurrence, Nat.cast_add, eq_self

    33 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  5. lemma Poland1998P4.lemma3 line 51 source

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

    Statement uses: Nat, ZMod, OfNat.ofNat, Ne, LT.lt, Eq, Poland1998P4.a', HAdd.hAdd, HMul.hMul, Exists, And

    Proof uses: Fact, Nat.Prime, Fact.mk, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.minFacHelper_0, Bool.false, Exists.intro, ZMod.val, HDiv.hDiv, Neg.neg, And.intro, ZMod.val_lt, Eq.mpr, id and 75 more

    88 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  6. lemma Poland1998P4.can_get_a_later_one_zmod line 63 source

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

    Statement uses: Nat, Eq, ZMod, OfNat.ofNat, Poland1998P4.a', Exists, And, LT.lt

    Proof uses: LE.le, Or, lt_or_ge, Exists.intro, And.intro, of_eq_true, Eq.trans, True, congrFun', congrArg, Poland1998P4.a, Nat.succ, HAdd.hAdd, HDiv.hDiv, Poland1998P4.a.eq_3, False.elim, False, noConfusion_of_Nat, Nat.ctorIdx, congr and 45 more

    92 instances, coercions and auxiliary constants left out.

    Tactic trace: 40 steps

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

  7. lemma Poland1998P4.can_get_a_later_one line 109 source

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

    Statement uses: Nat, Dvd.dvd, OfNat.ofNat, Poland1998P4.a, Exists, And, LT.lt

    Proof uses: Eq, ZMod, Poland1998P4.a', Poland1998P4.can_get_a_later_one_zmod, Iff.mpr, ZMod.natCast_eq_zero_iff, Exists.intro, And.intro, Iff.mp

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  8. lemma Poland1998P4.strengthen line 115 source

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

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

    Proof uses: Nat.recAux, OfNat.ofNat, Exists.intro, And.intro, pos_of_gt, HAdd.hAdd

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  9. theorem Poland1998P4.poland1998_p4' line 129 source

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

    Statement uses: Nat, Exists, And, LT.lt, Dvd.dvd, OfNat.ofNat, Poland1998P4.a

    Proof uses: of_eq_true, Eq.trans, True, congrArg, Nat.succ, HAdd.hAdd, HDiv.hDiv, Poland1998P4.a.eq_3, Eq, False.elim, False, noConfusion_of_Nat, Nat.ctorIdx, congr, Poland1998P4.a.eq_2, Nat.div_self, LE.le, Poland1998P4.strengthen, Poland1998P4.can_get_a_later_one, Exists.intro

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  10. problem Poland1998P4.poland1998_p4 line 135 source

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

    Statement uses: Set.Infinite, Nat, Set.ofPred, Dvd.dvd, OfNat.ofNat, Poland1998P4.a

    Proof uses: Set.infinite_of_forall_exists_gt, And, LT.lt, Exists, Membership.mem, Set, Poland1998P4.poland1998_p4', Exists.intro, And.intro

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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