Compfiles/Imo2025P4.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2025, Problem 4

A proper divisor of a positive integer N is a positive divisor of N other than N itself. The infinite sequence a₁, a₂, ... consists of positive integers, each of which has at least three proper divisors. For each n ⩾ 1, the integer aₙ₊₁ is the sum of the three largest proper divisors of aₙ. Determine all possible values of a₁.

Imports (3)
Imported by 1 file
  1. determine Imo2025P4.answer line 35 source

    standard axioms: propext what this means

    Statement uses: Set, Nat

    Proof uses: Set.ofPred, Exists, And, Eq, HMul.hMul, HPow.hPow, OfNat.ofNat, Nat.Coprime

    7 instances, coercions and auxiliary constants left out.

  2. def Imo2025P4.ψ line 41 source

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

    Statement uses: Nat

    Proof uses: List.sum, List.take, OfNat.ofNat, List.reverse, Finset.sort, Nat.properDivisors, LE.le

    11 instances, coercions and auxiliary constants left out.

  3. def Imo2025P4.S line 43 source

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

    Statement uses: Set, Nat

    Proof uses: Set.ofPred, LE.le, OfNat.ofNat, Finset.card, Nat.properDivisors

    2 instances, coercions and auxiliary constants left out.

  4. def Imo2025P4.ValidSequence line 45 source

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

    Statement uses: Nat

    Proof uses: And, LT.lt, OfNat.ofNat, Membership.mem, Set, Imo2025P4.S, Eq, HAdd.hAdd, Imo2025P4.ψ

    5 instances, coercions and auxiliary constants left out.

  5. def Imo2025P4.smallDivisors line 47 source

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

    Statement uses: Nat, List

    Proof uses: Finset.sort, Finset.erase, Nat.divisors, OfNat.ofNat, LE.le

    9 instances, coercions and auxiliary constants left out.

  6. def Imo2025P4.threeSmallestDivisors line 49 source

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

    Statement uses: Nat, List

    Proof uses: List.take, OfNat.ofNat, Imo2025P4.smallDivisors

    1 instances, coercions and auxiliary constants left out.

  7. lemma Imo2025P4.take_smallDivisors_eq_threeSmallestDivisors line 51 source

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

    Statement uses: Nat, Eq, List, List.take, OfNat.ofNat, Imo2025P4.smallDivisors, Imo2025P4.threeSmallestDivisors

    Proof uses: rfl

    2 instances, coercions and auxiliary constants left out.

  8. lemma Imo2025P4.mem_divisors_erase_one line 54 source

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

    Statement uses: Nat, Iff, Membership.mem, Finset, Finset.erase, Nat.divisors, OfNat.ofNat, And, Ne, Dvd.dvd

    Proof uses: Eq.mpr, id, Eq, congrArg, propext, Finset.mem_erase, Nat.mem_divisors, Iff.rfl

    10 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  9. lemma Imo2025P4.dvd_of_mem_divisors_erase_one line 58 source

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

    Statement uses: Nat, Membership.mem, Finset, Finset.erase, Nat.divisors, OfNat.ofNat, Dvd.dvd

    Proof uses: And.left, Ne, And.right, And, Iff.mp, Imo2025P4.mem_divisors_erase_one

    10 instances, coercions and auxiliary constants left out.

  10. lemma Imo2025P4.pos_of_mem_divisors_erase_one line 61 source

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

    Statement uses: Nat, Membership.mem, Finset, Finset.erase, Nat.divisors, OfNat.ofNat, LT.lt

    Proof uses: Nat.pos_of_mem_divisors, Iff.mpr, And, Dvd.dvd, Ne, Nat.mem_divisors, And.right, Iff.mp, Imo2025P4.mem_divisors_erase_one

    10 instances, coercions and auxiliary constants left out.

  11. lemma Imo2025P4.mem_divisors_erase_one_of_dvd_ne_one line 64 source

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

    Statement uses: Nat, Dvd.dvd, Ne, OfNat.ofNat, Membership.mem, Finset, Finset.erase, Nat.divisors

    Proof uses: Iff.mpr, And, Imo2025P4.mem_divisors_erase_one, And.intro

    10 instances, coercions and auxiliary constants left out.

  12. lemma Imo2025P4.reverse_properDivisors_eq_div_divisors_erase_one line 68 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, Eq, List, List.reverse, Finset.sort, Nat.properDivisors, LE.le, List.map, HDiv.hDiv, Imo2025P4.smallDivisors

    Proof uses: Eq.mpr, id, congrArg, propext, List.reverse_eq_iff, List.SortedLT.eq_of_mem_iff, Finset.sortedLT_sort, List.SortedLT, List.Pairwise, LT.lt, List.sortedLT_iff_pairwise, List.pairwise_reverse, List.pairwise_map, List.Pairwise.imp, And, Membership.mem, Finset.erase, Nat.divisors, Nat.div_lt_div_left, Imo2025P4.dvd_of_mem_divisors_erase_one and 27 more

    46 instances, coercions and auxiliary constants left out.

    Tactic trace: 31 steps

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

  13. lemma Imo2025P4.psi_eq_of_threeSmallestDivisors_eq line 96 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, Eq, List, Imo2025P4.threeSmallestDivisors, List.cons, List.nil, Imo2025P4.ψ, HAdd.hAdd, HDiv.hDiv

    Proof uses: Eq.mpr, List.sum, List.take, List.reverse, Finset.sort, Nat.properDivisors, LE.le, id, congrArg, Imo2025P4.ψ.eq_1, List.map, Imo2025P4.smallDivisors, Imo2025P4.reverse_properDivisors_eq_div_divisors_erase_one, Eq.symm, List.map_take, Imo2025P4.take_smallDivisors_eq_threeSmallestDivisors, of_eq_true, Eq.trans, True, congr and 5 more

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  14. lemma Imo2025P4.answer_mem_S line 102 source

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

    Statement uses: Nat, Membership.mem, Set, Imo2025P4.answer, Imo2025P4.S

    Proof uses: Exists, And, Eq, HMul.hMul, HPow.hPow, OfNat.ofNat, Nat.Coprime, LT.lt, LE.le, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, HAdd.hAdd, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast and 79 more

    131 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

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

  15. lemma Imo2025P4.pos_of_mem_S line 117 source

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

    Statement uses: Nat, Membership.mem, Set, Imo2025P4.S, LT.lt, OfNat.ofNat

    Proof uses: Decidable.byContradiction, Not, Eq, Finset.card, Nat.properDivisors, Eq.mpr, id, congrArg, Eq.mp, Eq.trans, LE.le, EmptyCollection.emptyCollection, Finset, Nat.properDivisors_zero, Finset.card_empty, Eq.refl

    23 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  16. lemma Imo2025P4.answer_pos line 125 source

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

    Statement uses: Nat, Membership.mem, Set, Imo2025P4.answer, LT.lt, OfNat.ofNat

    Proof uses: Imo2025P4.pos_of_mem_S, Imo2025P4.answer_mem_S

    4 instances, coercions and auxiliary constants left out.

  17. lemma Imo2025P4.sort_take_three_eq_of_first_three line 127 source

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

    Statement uses: Finset, Nat, Membership.mem, Finset.erase, LE.le, Eq, List, List.take, OfNat.ofNat, Finset.sort, List.cons, List.nil

    16 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  18. lemma Imo2025P4.divisors_erase_one_sort_take_three_eq_two_three_six line 133 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, Dvd.dvd, Not, Eq, List, Imo2025P4.threeSmallestDivisors, List.cons, List.nil

    Proof uses: Imo2025P4.sort_take_three_eq_of_first_three, Finset.erase, Nat.divisors, Membership.mem, Finset, LT.lt, Nat.pos_of_mem_divisors, Iff.mpr, And, Nat.mem_divisors, id, And.intro, dvd_refl, Eq.mp, Eq.trans, congrArg, Aesop.BuiltinRules.not_intro, False, False.elim, eq_false and 29 more

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  19. lemma Imo2025P4.divisors_erase_one_sort_take_three_eq_two_three_four line 145 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, Dvd.dvd, Eq, List, Imo2025P4.threeSmallestDivisors, List.cons, List.nil

    Proof uses: Imo2025P4.sort_take_three_eq_of_first_three, Finset.erase, Nat.divisors, Membership.mem, Finset, LT.lt, Nat.pos_of_mem_divisors, Iff.mpr, And, Nat.mem_divisors, id, And.intro, Not, dvd_refl, Eq.mp, Eq.trans, congrArg, Aesop.BuiltinRules.not_intro, False, False.elim and 2 more

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  20. lemma Imo2025P4.divisors_erase_one_sort_take_three_eq_two_three_five line 154 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, Dvd.dvd, Not, Eq, List, Imo2025P4.threeSmallestDivisors, List.cons, List.nil

    Proof uses: Imo2025P4.sort_take_three_eq_of_first_three, Finset.erase, Nat.divisors, Membership.mem, Finset, LT.lt, Nat.pos_of_mem_divisors, Iff.mpr, And, Nat.mem_divisors, id, And.intro, dvd_refl, Eq.mp, Eq.trans, congrArg, Aesop.BuiltinRules.not_intro, False, False.elim, eq_false and 29 more

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  21. lemma Imo2025P4.psi_answer_mem_S' line 166 source

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

    Statement uses: Nat, Membership.mem, Set, Imo2025P4.answer, Imo2025P4.ψ

    Proof uses: Ne, OfNat.ofNat, Exists, And, Eq, HMul.hMul, HPow.hPow, Nat.Coprime, dite, Exists.intro, And.intro, Not, Dvd.dvd, Iff.mp, Nat.Prime.coprime_iff_not_dvd, Nat.prime_two, Nat.Coprime.of_dvd_left, Nat.Coprime.symm, Nat.prime_five, List and 64 more

    83 instances, coercions and auxiliary constants left out.

    Tactic trace: 44 steps

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

  22. lemma Imo2025P4.psi_answer_mem_S line 197 source

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

    Statement uses: Nat, Membership.mem, Set, Imo2025P4.answer, Nat.iterate, Imo2025P4.ψ

    Proof uses: Nat.recAux, Eq.mpr, OfNat.ofNat, id, Eq, congrArg, Function.iterate_zero, id_eq, HAdd.hAdd, Exists, And, HMul.hMul, HPow.hPow, Nat.Coprime, Function.iterate_succ_apply', Imo2025P4.psi_answer_mem_S'

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  23. lemma Imo2025P4.answer_sufficient line 203 source

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

    Statement uses: Nat, Membership.mem, Set, Imo2025P4.answer, Exists, And, Eq, OfNat.ofNat, Imo2025P4.ValidSequence

    Proof uses: Nat.iterate, Imo2025P4.ψ, Exists.intro, And.intro, rfl, Imo2025P4.psi_answer_mem_S, LT.lt, Imo2025P4.S, HAdd.hAdd, Imo2025P4.answer_pos, Imo2025P4.answer_mem_S, Function.iterate_succ_apply'

    7 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  24. lemma Imo2025P4.odd_sum_iff_length_of_forall_odd line 211 source

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

    Statement uses: List, Nat, Membership.mem, Odd, Iff, List.sum, List.length

    Proof uses: List.rec, List.nil, of_eq_true, Eq.trans, False, True, congr, congrArg, iff_self, List.cons, Or, Eq, eq_true, or_true, Eq.mpr, HAdd.hAdd, id, List.sum_cons, OfNat.ofNat, List.length_cons and 11 more

    16 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  25. lemma Imo2025P4.odd_of_sum_odd line 219 source

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

    Statement uses: List, Nat, Odd, LE.le, List.length, Membership.mem, List.sum, List.take

    Proof uses: Eq.mpr, id, Eq, congrArg, Eq.trans, Min.min, List.length_take, min_eq_left, Iff.mpr, Imo2025P4.odd_sum_iff_length_of_forall_odd, List.mem_of_mem_take

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  26. lemma Imo2025P4.two_dvd_of_two_dvd_psi line 224 source

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

    Statement uses: Nat, Membership.mem, Set, Imo2025P4.S, Dvd.dvd, OfNat.ofNat, Imo2025P4.ψ

    Proof uses: Decidable.byContradiction, Not, Finset, Nat.properDivisors, Odd, Odd.of_dvd_nat, Iff.mp, Even, Nat.not_even_iff_odd, Eq.mpr, id, Eq, congrArg, propext, even_iff_two_dvd, And.left, LT.lt, And, Nat.mem_properDivisors, List and 19 more

    37 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

  27. lemma Imo2025P4.psi_le_of_three_smallest_ge line 239 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, Exists, And, Eq, List, Imo2025P4.threeSmallestDivisors, List.cons, List.nil, LE.le, Imo2025P4.ψ, HAdd.hAdd, HDiv.hDiv

    Proof uses: Eq.mpr, id, congrArg, Imo2025P4.psi_eq_of_threeSmallestDivisors_eq, Nat.div_le_div, le_refl, ne_of_gt, lt_of_le_of_ne', zero_le

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  28. lemma Imo2025P4.min_divisors_of_mem_S line 250 source

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

    Statement uses: Nat, Membership.mem, Set, Imo2025P4.S, And, Ne, OfNat.ofNat, Exists, Eq, List, Imo2025P4.threeSmallestDivisors, List.cons, List.nil, Finset, Finset.erase, Nat.divisors, LE.le, LT.lt

    Proof uses: Nat.ne_zero_of_lt, Imo2025P4.pos_of_mem_S, Finset.card, Nat.properDivisors, List.length, List.reverse, Finset.sort, List.map, HDiv.hDiv, Imo2025P4.smallDivisors, congrArg, Imo2025P4.reverse_properDivisors_eq_div_divisors_erase_one, Eq.mp, congr, Eq.trans, List.length_reverse, Finset.length_sort, List.length_map, Eq.mpr, id and 42 more

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 30 steps

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

  29. lemma Imo2025P4.mem_of_threeSmallestDivisors_eq line 279 source

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

    Statement uses: Nat, Eq, List, Imo2025P4.threeSmallestDivisors, List.cons, List.nil, And, Membership.mem, Finset, Finset.erase, Nat.divisors, OfNat.ofNat

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, eq_true, Iff.mp, Finset.sort, LE.le, Finset.mem_sort, Eq.mpr, Not, Dvd.dvd, id, Ne, Eq.mp, Imo2025P4.smallDivisors, List.mem_of_mem_take, And.intro, Or and 6 more

    22 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  30. lemma Imo2025P4.dvd_of_threeSmallestDivisors_eq line 286 source

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

    Statement uses: Nat, Eq, List, Imo2025P4.threeSmallestDivisors, List.cons, List.nil, And, Dvd.dvd

    Proof uses: Membership.mem, Finset, Finset.erase, Nat.divisors, OfNat.ofNat, Imo2025P4.mem_of_threeSmallestDivisors_eq, And.intro, Imo2025P4.dvd_of_mem_divisors_erase_one

    7 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  31. structure Imo2025P4.ThreeMinDivisors line 292 source

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

    Statement uses: Nat

  32. lemma Imo2025P4.ThreeMinDivisors.mems line 300 source

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

    Statement uses: Nat, Imo2025P4.ThreeMinDivisors, And, Membership.mem, Finset, Finset.erase, Nat.divisors, OfNat.ofNat

    Proof uses: Imo2025P4.mem_of_threeSmallestDivisors_eq, Imo2025P4.ThreeMinDivisors.hdiv

    4 instances, coercions and auxiliary constants left out.

  33. lemma Imo2025P4.ThreeMinDivisors.dvds line 304 source

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

    Statement uses: Nat, Imo2025P4.ThreeMinDivisors, And, Dvd.dvd

    Proof uses: Imo2025P4.dvd_of_threeSmallestDivisors_eq, Imo2025P4.ThreeMinDivisors.hdiv

    1 instances, coercions and auxiliary constants left out.

  34. lemma Imo2025P4.ThreeMinDivisors.psi_eq line 306 source

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

    Statement uses: Nat, Imo2025P4.ThreeMinDivisors, Ne, OfNat.ofNat, Eq, Imo2025P4.ψ, HAdd.hAdd, HDiv.hDiv

    Proof uses: Imo2025P4.psi_eq_of_threeSmallestDivisors_eq, Imo2025P4.ThreeMinDivisors.hdiv

    6 instances, coercions and auxiliary constants left out.

  35. lemma Imo2025P4.threeMinDivisors_of_mem_S line 311 source

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

    Statement uses: Nat, Membership.mem, Set, Imo2025P4.S, And, Ne, OfNat.ofNat, Exists, Imo2025P4.ThreeMinDivisors

    Proof uses: Eq, List, Imo2025P4.threeSmallestDivisors, List.cons, List.nil, Finset, Finset.erase, Nat.divisors, LE.le, LT.lt, Imo2025P4.min_divisors_of_mem_S, And.intro, Exists.intro, Imo2025P4.ThreeMinDivisors.mk

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  36. lemma Imo2025P4.mem_take_or_gt_of_divisor line 316 source

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

    Statement uses: Nat, Membership.mem, Set, Imo2025P4.S, Finset, Finset.erase, Nat.divisors, OfNat.ofNat, Eq, List, Imo2025P4.threeSmallestDivisors, List.cons, List.nil, Or, LT.lt

    Proof uses: dite, Or.inl, Not, Eq.mpr, id, Eq.trans, False, congrFun', congrArg, eq_false, false_or, Decidable.byContradiction, Finset.sort, LE.le, Iff.mpr, Finset.mem_sort, HAppend.hAppend, List.drop, Eq.symm, List.take and 14 more

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 19 steps

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

  37. lemma Imo2025P4.mem_of_dvd_mem_threeSmallest line 335 source

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

    Statement uses: Nat, Imo2025P4.ThreeMinDivisors, Membership.mem, Set, Imo2025P4.S, Ne, OfNat.ofNat, Dvd.dvd, List, List.cons, List.nil, LE.le

    Proof uses: And, Imo2025P4.ThreeMinDivisors.dvds, dite, LT.lt, Decidable.byContradiction, Not, Eq, Or, False, Eq.mp, Eq.trans, congrArg, or_false, Imo2025P4.ThreeMinDivisors.hd₁ge, Imo2025P4.ThreeMinDivisors.hd₁₂, Imo2025P4.ThreeMinDivisors.hd₂₃, Finset, Finset.erase, Nat.divisors, Imo2025P4.mem_divisors_erase_one_of_dvd_ne_one and 4 more

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  38. lemma Imo2025P4.first_min_divisor_eq_two_of_two_dvd line 347 source

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

    Statement uses: Nat, Membership.mem, Set, Imo2025P4.S, Dvd.dvd, OfNat.ofNat, Imo2025P4.ThreeMinDivisors, Eq

    Proof uses: Ne, Nat.ne_zero_of_lt, Imo2025P4.pos_of_mem_S, Finset, Finset.erase, Nat.divisors, Imo2025P4.mem_divisors_erase_one_of_dvd_ne_one, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Or, List, List.cons, List.nil, LT.lt, Imo2025P4.mem_take_or_gt_of_divisor, Imo2025P4.ThreeMinDivisors.hdiv, Imo2025P4.ThreeMinDivisors.hd₁ge and 2 more

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  39. lemma Imo2025P4.second_min_divisor_eq_four_of_four_dvd line 355 source

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

    Statement uses: Nat, Membership.mem, Set, Imo2025P4.S, Ne, OfNat.ofNat, Not, Dvd.dvd, Imo2025P4.ThreeMinDivisors, Eq

    Proof uses: Finset, Finset.erase, Nat.divisors, Imo2025P4.mem_divisors_erase_one_of_dvd_ne_one, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Or, List, List.cons, List.nil, LT.lt, Imo2025P4.mem_take_or_gt_of_divisor, Imo2025P4.ThreeMinDivisors.hdiv, And, Imo2025P4.ThreeMinDivisors.dvds, Imo2025P4.ThreeMinDivisors.hd₁₂, Imo2025P4.ThreeMinDivisors.hd₂₃

    15 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  40. lemma Imo2025P4.not_three_dvd_psi_of_second_min_divisor_four line 363 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, Not, Dvd.dvd, Imo2025P4.ThreeMinDivisors, Eq, Imo2025P4.ψ

    Proof uses: HAdd.hAdd, HDiv.hDiv, HMul.hMul, Eq.mpr, id, congrArg, Imo2025P4.ThreeMinDivisors.psi_eq, Eq.trans, congrFun', congr, eq_of_heq, Dvd, HEq, Eq.refl, HEq.refl, Eq.symm, Nat.mul_div_cancel', And.right, And, Imo2025P4.ThreeMinDivisors.dvds and 1 more

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  41. lemma Imo2025P4.second_min_divisor_prime_of_not_four_dvd line 374 source

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

    Statement uses: Nat, Membership.mem, Set, Imo2025P4.S, Ne, OfNat.ofNat, Imo2025P4.ThreeMinDivisors, Eq, Not, Dvd.dvd, Nat.Prime

    Proof uses: And, Imo2025P4.ThreeMinDivisors.dvds, GT.gt, Finset, Finset.erase, Nat.divisors, Imo2025P4.mem_divisors_erase_one_of_dvd_ne_one, dvd_trans, Or, List, List.cons, List.nil, LT.lt, Imo2025P4.mem_take_or_gt_of_divisor, Imo2025P4.ThreeMinDivisors.hdiv, LE.le, Nat.le_of_dvd, Imo2025P4.ThreeMinDivisors.hd₁₂, Eq.mp, Eq.trans and 88 more

    123 instances, coercions and auxiliary constants left out.

    Tactic trace: 31 steps

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

  42. lemma Imo2025P4.third_min_divisor_prime_of_not_double_second line 397 source

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

    Statement uses: Nat, Membership.mem, Set, Imo2025P4.S, Ne, OfNat.ofNat, Dvd.dvd, Not, Imo2025P4.ThreeMinDivisors, Eq, Nat.Prime, HMul.hMul

    Proof uses: And, Imo2025P4.ThreeMinDivisors.dvds, Finset, Finset.erase, Nat.divisors, Imo2025P4.ThreeMinDivisors.mems, Decidable.byContradiction, LE.le, LT.lt, Exists, False, Iff.mp, Nat.not_prime_iff_exists_dvd_lt, Imo2025P4.ThreeMinDivisors.hd₁₂, Imo2025P4.ThreeMinDivisors.hd₂₃, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, HAdd.hAdd and 98 more

    130 instances, coercions and auxiliary constants left out.

    Tactic trace: 43 steps

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

  43. lemma Imo2025P4.psi_mod_two_eq_one_of_min_divisors_prime line 426 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, Dvd.dvd, Not, Imo2025P4.ThreeMinDivisors, Eq, Nat.Prime, HMod.hMod, Imo2025P4.ψ

    Proof uses: And, Imo2025P4.ThreeMinDivisors.dvds, LT.lt, HDiv.hDiv, HMul.hMul, Eq.mp, congrArg, Eq.mpr, HAdd.hAdd, id, congrFun', Eq.trans, Imo2025P4.ThreeMinDivisors.psi_eq

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  44. lemma Imo2025P4.not_six_dvd_psi_of_not_four_dvd line 439 source

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

    Statement uses: Nat, Membership.mem, Set, Imo2025P4.S, Ne, OfNat.ofNat, Dvd.dvd, Not, Imo2025P4.ThreeMinDivisors, Eq, Imo2025P4.ψ

    Proof uses: Nat.Prime, Imo2025P4.second_min_divisor_prime_of_not_four_dvd, dite, HMul.hMul, HAdd.hAdd, HDiv.hDiv, of_eq_true, Eq.trans, True, congrFun', congrArg, Imo2025P4.ThreeMinDivisors.psi_eq, congr, eq_self, Eq.mp, And.right, And, Imo2025P4.ThreeMinDivisors.dvds, Trans.trans, mul_div_cancel_left₀ and 11 more

    47 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

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

  45. lemma Imo2025P4.six_dvd_of_six_dvd_psi line 458 source

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

    Statement uses: Nat, Membership.mem, Set, Imo2025P4.S, Dvd.dvd, OfNat.ofNat, Imo2025P4.ψ

    Proof uses: Decidable.byContradiction, Not, Imo2025P4.two_dvd_of_two_dvd_psi, Ne, Exists, Imo2025P4.ThreeMinDivisors, And, False, Imo2025P4.threeMinDivisors_of_mem_S, Eq, Imo2025P4.first_min_divisor_eq_two_of_two_dvd, dite, Imo2025P4.second_min_divisor_eq_four_of_four_dvd, Imo2025P4.not_three_dvd_psi_of_second_min_divisor_four, dvd_trans, Mathlib.Meta.NormNum.isNat_dvd_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Imo2025P4.not_six_dvd_psi_of_not_four_dvd

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

  46. lemma Imo2025P4.psi_lt_of_not_two_dvd line 471 source

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

    Statement uses: Nat, Membership.mem, Set, Imo2025P4.S, Not, Dvd.dvd, OfNat.ofNat, LT.lt, Imo2025P4.ψ

    Proof uses: Ne, Exists, And, Eq, List, Imo2025P4.threeSmallestDivisors, List.cons, List.nil, Finset, Finset.erase, Nat.divisors, LE.le, Imo2025P4.min_divisors_of_mem_S, dvd_trans, And.left, Iff.mp, Nat.mem_divisors, HAdd.hAdd, HDiv.hDiv, Imo2025P4.psi_le_of_three_smallest_ge and 8 more

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

  47. lemma Imo2025P4.psi_lt_of_two_dvd_not_three_dvd line 481 source

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

    Statement uses: Nat, Membership.mem, Set, Imo2025P4.S, Dvd.dvd, OfNat.ofNat, Not, LT.lt, Imo2025P4.ψ

    Proof uses: Ne, Exists, And, Eq, List, Imo2025P4.threeSmallestDivisors, List.cons, List.nil, Finset, Finset.erase, Nat.divisors, LE.le, Imo2025P4.min_divisors_of_mem_S, HAdd.hAdd, HDiv.hDiv, Imo2025P4.psi_le_of_three_smallest_ge, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool and 3 more

    23 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

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

  48. lemma Imo2025P4.descending_contra line 491 source

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

    Statement uses: Nat, OfNat.ofNat, HAdd.hAdd, LT.lt, False

    Proof uses: And, LE.le, Nat.recAux

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  49. lemma Imo2025P4.dvd_of_ValidSequence line 501 source

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

    Statement uses: Nat, Imo2025P4.ValidSequence, Membership.mem, Set, Imo2025P4.S, Not, Dvd.dvd, LT.lt, Imo2025P4.ψ

    Proof uses: Classical.byContradiction, Exists, False, Eq.mp, congrArg, propext, Classical.not_forall, HAdd.hAdd, OfNat.ofNat, And.left, Eq, And.right, And, Eq.mpr, id, Imo2025P4.descending_contra

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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

  50. lemma Imo2025P4.two_dvd_of_ValidSequence line 519 source

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

    Statement uses: Nat, Imo2025P4.ValidSequence, Dvd.dvd, OfNat.ofNat

    Proof uses: Imo2025P4.dvd_of_ValidSequence, Imo2025P4.psi_lt_of_not_two_dvd, Imo2025P4.two_dvd_of_two_dvd_psi

    3 instances, coercions and auxiliary constants left out.

  51. lemma Imo2025P4.three_dvd_of_ValidSequence line 522 source

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

    Statement uses: Nat, Imo2025P4.ValidSequence, Dvd.dvd, OfNat.ofNat

    Proof uses: Membership.mem, Set, Imo2025P4.S, Not, LT.lt, Imo2025P4.ψ, Imo2025P4.psi_lt_of_two_dvd_not_three_dvd, Imo2025P4.two_dvd_of_ValidSequence, HAdd.hAdd, Eq.mp, congrArg, And.right, Eq, And, Imo2025P4.six_dvd_of_six_dvd_psi, Imo2025P4.dvd_of_ValidSequence

    10 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  52. lemma Imo2025P4.six_dvd_of_ValidSequence line 533 source

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

    Statement uses: Nat, Imo2025P4.ValidSequence, Dvd.dvd, OfNat.ofNat

    3 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  53. lemma Imo2025P4.psi_of_six_dvd line 537 source

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

    Statement uses: Nat, Membership.mem, Set, Imo2025P4.S, Dvd.dvd, OfNat.ofNat, Eq, Imo2025P4.ψ, ite, HDiv.hDiv, HMul.hMul

    Proof uses: Ne, Nat.ne_zero_of_lt, Imo2025P4.pos_of_mem_S, dite, Not

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  54. lemma Imo2025P4.odd_of_five_branch line 550 source

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

    Statement uses: Nat, Dvd.dvd, OfNat.ofNat, Not, HDiv.hDiv, HMul.hMul

    9 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  55. lemma Imo2025P4.not_five_branch_of_ValidSequence line 552 source

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

    Statement uses: Nat, Imo2025P4.ValidSequence, Not, And, Dvd.dvd, OfNat.ofNat

    Proof uses: Eq.mpr, id, Eq, Imo2025P4.ψ, ite, HDiv.hDiv, HMul.hMul, Imo2025P4.psi_of_six_dvd, And.left, Membership.mem, Set, Imo2025P4.S, HAdd.hAdd, And.right, LT.lt, Imo2025P4.six_dvd_of_ValidSequence, congrArg, Eq.mp, congr, Eq.symm and 7 more

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  56. lemma Imo2025P4.padicValNat_step_thirteen_twelfths line 564 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, padicValNat

    Proof uses: congrArg, Eq.mp, congr, Eq.trans, padicValNat.mul, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, of_eq_true, Not, True, False, eq_false, not_false, not_false_eq_true, eq_true, True.intro, congrFun' and 4 more

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  57. lemma Imo2025P4.padicValNat_descends_thirteen_twelfths line 572 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, padicValNat

    Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrFun', congrArg, MulZeroClass.mul_zero, add_zero, eq_self

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  58. lemma Imo2025P4.not_forever_thirteen_twelfths line 579 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, False

    Proof uses: padicValNat, Imo2025P4.padicValNat_descends_thirteen_twelfths

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  59. lemma Imo2025P4.exists_fixed_branch_of_ValidSequence line 584 source

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

    Statement uses: Nat, Imo2025P4.ValidSequence, Exists, And, Not, Dvd.dvd, OfNat.ofNat

    Proof uses: Classical.byContradiction, dite, False, Classical.propDecidable, Imo2025P4.not_five_branch_of_ValidSequence, And.intro, Eq.mp, Eq.trans, forall_congr, implies_congr, Eq.refl, Eq, HMul.hMul, HAdd.hAdd, Imo2025P4.ψ, ite, HDiv.hDiv, Imo2025P4.psi_of_six_dvd, And.left, Membership.mem and 11 more

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  60. lemma Imo2025P4.exists_first_fixed_branch_of_ValidSequence line 600 source

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

    Statement uses: Nat, Imo2025P4.ValidSequence, Exists, And, LT.lt, Dvd.dvd, OfNat.ofNat, Not

    Proof uses: Imo2025P4.exists_fixed_branch_of_ValidSequence, Exists.intro, Nat.find, Nat.find_spec, Decidable.byContradiction, Nat.find_min, Imo2025P4.not_five_branch_of_ValidSequence, And.intro

    10 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

  61. lemma Imo2025P4.step_of_first_fixed_branch line 615 source

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

    Statement uses: Nat, Imo2025P4.ValidSequence, Dvd.dvd, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd

    Proof uses: Imo2025P4.six_dvd_of_ValidSequence, Imo2025P4.ψ, ite, HDiv.hDiv, Imo2025P4.psi_of_six_dvd, And.left, Membership.mem, Set, Imo2025P4.S, And.right, LT.lt, And

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  62. lemma Imo2025P4.twelve_pow_mul_of_first_fixed_branch line 621 source

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

    Statement uses: Nat, Imo2025P4.ValidSequence, LT.lt, Dvd.dvd, OfNat.ofNat, Eq, HMul.hMul, HPow.hPow

    Proof uses: LE.le, Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', pow_zero, one_mul, eq_self, HAdd.hAdd, Nat.lt_of_succ_le, Imo2025P4.step_of_first_fixed_branch, Nat.le_refl

    27 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  63. lemma Imo2025P4.start_eq_pow_mul_of_first_fixed_branch line 634 source

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

    Statement uses: Nat, Imo2025P4.ValidSequence, LT.lt, Dvd.dvd, OfNat.ofNat, Exists, And, Eq, HMul.hMul, HPow.hPow

    Proof uses: HDiv.hDiv, Imo2025P4.twelve_pow_mul_of_first_fixed_branch, Nat.Coprime, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Nat.Coprime.pow_right, Nat.Coprime.pow_left, Dvd.intro, Eq.symm, Nat.Coprime.dvd_of_dvd_mul_left, Nat.Coprime.symm, Nat.mul_div_cancel', of_eq_true, Eq.trans, True, congrArg and 11 more

    37 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

  64. lemma Imo2025P4.coprime_ten line 647 source

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

    Statement uses: Nat, Eq, HMul.hMul, OfNat.ofNat, Not, Dvd.dvd, Nat.Coprime

    Proof uses: Iff.mpr, Nat.coprime_comm, Nat.Prime.coprime_iff_not_dvd, Nat.prime_two, Nat.prime_five, Eq.mpr, id, congrArg, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.isNat_mul, And, propext, Nat.coprime_mul_iff_right, And.intro

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  65. lemma Imo2025P4.start_eq_pow_of_first_fixed_branch line 655 source

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

    Statement uses: Nat, Imo2025P4.ValidSequence, LT.lt, Dvd.dvd, OfNat.ofNat, Not, Exists, And, Eq, HMul.hMul, HPow.hPow, Nat.Coprime

    Proof uses: Imo2025P4.start_eq_pow_mul_of_first_fixed_branch, Imo2025P4.six_dvd_of_ValidSequence, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Nat.Coprime.dvd_of_dvd_mul_left, Nat.Coprime.pow_right, Eq.mp, congrArg, Exists.intro, And.intro, Eq.trans, Imo2025P4.coprime_ten

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  66. lemma Imo2025P4.answer_necessary line 672 source

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

    Statement uses: Nat, Membership.mem, Set, Set.ofPred, Exists, And, Eq, OfNat.ofNat, Imo2025P4.ValidSequence, Imo2025P4.answer

    Proof uses: LT.lt, Dvd.dvd, Not, Imo2025P4.exists_first_fixed_branch_of_ValidSequence, HMul.hMul, HPow.hPow, Nat.Coprime, Imo2025P4.start_eq_pow_of_first_fixed_branch, Exists.intro, Eq.mp, congrFun', congrArg

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  67. problem Imo2025P4.imo2025_p4 line 681 source

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

    Statement uses: Eq, Set, Nat, Set.ofPred, Exists, And, OfNat.ofNat, LT.lt, LE.le, Finset.card, Nat.properDivisors, HAdd.hAdd, List.sum, List.take, List.reverse, Finset.sort, Imo2025P4.answer

    Proof uses: Set.ext, Iff.intro, Membership.mem, Imo2025P4.answer_necessary, Imo2025P4.answer_sufficient

    27 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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